(* Éléments de correction à propos des entiers de Church *) (* vus au premier TD *) Section EntiersDeChurchV1. (* Coq est fondé sur le calcul des constructions ; il *) (* contient donc en particulier la lambda-calcul simplement *) (* typé : il suffit de se restreindre au type Prop, et ne *) (* s'autoriser que le connecteur -> *) (* On définit le type de base, que nous notons X *) Variable X : Prop. Let N0 := X -> X. Let N1 := (X->X)->(X->X). Let N := N1. (* On code les entiers par le type N1. Un élément de N1 est *) (* une fonction qui prend en argument f:X->X et x:X et qui *) (* renvoie un élement de type X. *) (* Essentiellement, on peut renvoyer x, ou bien n'importe *) (* quelle itération de f sur x. Cela permet de coder *) (* naturellement les entiers : l'entier n est codé par *) (* l'itération de f n fois. *) Let O : N := (fun s z => z). Let S : N -> N := (fun n => (fun s z => s (n s z))). (* On se définit quelques entiers en composant S et O : *) Let I : N := S O. Let II : N := S I. Let III : N := S II. Let IV : N := S III. Let IV_2 : N := fun s z => s (s (s (s z))). (* Remarque : IV et IV_2 ne sont pas le même terme comme on *) (* peut s'en apercevoir en utilisant cbv delta : *) Eval cbv delta in IV. Eval cbv delta in IV_2. (* On peut utiliser la tactique compute pour demander à Coq *) (* de beta-réduire un terme. Cela nous permet de vérifier *) (* que 4 correspond bien à l'itération 4 fois. *) (* Les deux termes sont bien beta-équivalents. *) Eval compute in IV. Eval compute in IV_2. (* L'addition et la multiplication se font naturellement : *) Let add : N -> N -> N := fun n m => (fun s z => n s (m s z)). (* Vérifions que 2 + 3 = 5 *) Eval compute in add II III. Let mul : (N -> N -> N) := fun n m => (fun s => n (m s)). (* Vérifions que 2*3 = 6 *) Eval compute in mul II III. (* et 3*0 = 0... *) Eval compute in mul III O. (* Pour faire la puissance, on aurait envie d'écrire quelque chose *) (* comme ça : fun p n => n (mul p) I. *) (* Le problème est que si p est de type N1, *) (* (mul p) est de type N2 = N1->N1 et il faudrait donc *) (* que n soit de type N3 = (N1 -> N1) -> N1 -> N1 *) (* Le système F, en nous apportant le polymorphisme va nous *) (* permettre de résoudre ce problème. *) End EntiersDeChurchV1. Section EntiersDeChurchV2. (* Le système F correspond à Coq restreint au type Prop, avec les *) (* connecteurs forall et ->. Comme nous le verrons dans le deuxième *) (* TP, nous pouvons coder toute la logique sous forme imprédicative *) (* dand le système F. Pour l'instant, contentons-nous de coder les *) (* entiers, en prolongeant les idées de la première section. *) Let N := forall (X:Prop), (X->X)->X->X. Let O : N := (fun _ s z => z). Let S : N -> N := (fun n => (fun _ s z => s (n _ s z))). Let I : N := S O. Let II : N := S I. Let III : N := S II. Let IV : N := S III. Let add : N -> N -> N := fun n m => (fun _ s z => n _ s (m _ s z)). Let mul : (N -> N -> N) := fun n m => (fun _ s => n _ (m _ s)). Let pow : (N -> N -> N) := fun p n => n _ (mul p) (S O). Print pow. (* Vérifions que 3^2 = 9 *) Eval compute in pow III II. (* et 3^0 = 1 *) Eval compute in pow III O. (* et 2^1 = 2 *) Eval compute in pow II I. (* Allons un peu plus loin... Nous allons montrer que la classe des *) (* fonctions sur les entiers écrivables en Système F est assez grande. *) (* Pour commencer, montrons qu'on peut faire le prédecesseur. *) (* Pour faire le prédecesseur, il faut ruser. La solution proposée *) (* ici n'est pas la plus concise, mais elle illustre bien l'idée *) (* à mettre en oeuvre : *) (* imaginons que nous sachions coder des valeurs booléennes T et F *) (* de telle sorte que nous puissions écrire des If...Then...Else *) (* imaginons que nous puissions coder des couples de la forme *) (* (n,b) où n est entier et b un booléen. *) (* Soit alors la fonction définie pour tout n par : *) (* Phi(n,F) = (n,T) et Phi(n,T) = (n+1, T) *) (* Alors, on a (0,F) -> (0,T) -> (1,T) -> ... -> (n,T) *) (* et donc, en itérant n fois Phi, on obtient un couple dont la *) (* première composante est le prédecesseur de n. *) (* Il ne nous reste plus qu'à coder ! *) (* Comment coder les booléens ? Si b est un booléen, et si M et N *) (* sont deux termes de même type T, on veut pouvoir faire *) (* l'instruction "If b Then M Else N". Nous codons cette *) (* instruction dans b : autrement dit, *) (* bMN = M si b est vrai et bMN = N si b est faux *) (* Ceci conduit naturellement aux définitions suivantes : *) Let bool := forall X:Prop, X -> X -> X. Let T : bool := fun _ x y => x. Let F : bool := fun _ x y => y. (* De la même façon, un couple de type A x B est codé ainsi : *) Let couple := fun A B : Prop => forall X:Prop, (A -> B -> X) -> X. Let cons : forall A B:Prop, A -> B -> couple A B := fun A B a b => (fun _ f => f a b). (* Les projections *) Let P1 : forall A B:Prop, couple A B -> A := fun A B c => c A (fun a b => a). Let P2 : forall A B:Prop, couple A B -> B := fun A B c => c B (fun a b => b). (* Dans un premier temps, nous allons travailler avec des couples *) (* de type N x bool. *) (* Pour alléger les notations, on définit une notation infixe pour *) (* le constructeur des couples : *) (* le couple (n,b) sera noté (n/b) *) Let consNBool := cons N bool. Infix "/" := consNBool. Let Phi := fun (c : couple N bool) => let n := P1 _ _ c in let b := P2 _ _ c in (* c = (n,b) *) b _ ((S n) / T) (n / T). (* Si b Alors (n+1,T) Sinon (n,T) *) Let pred : N -> N := fun n => P1 _ _ (n _ Phi (O / F)). (* et voilà : *) Eval compute in pred (pow II III). Eval compute in (pred I). Eval compute in (pred O). (* En fait, on peut coder n'importe quelle fonction récursive *) (* primitive : *) (* de manière générale, le schéma de récurrence primitif peut être *) (* écrit de la façon suivante *) (* let rec f (n:N) = match n with *) (* | 0 -> g *) (* | n+1 -> h (f n) *) (* Ceci donne : *) (* Rec := fun (X :Prop) (g : X) (h : X -> X) *) (* => (f : N -> X) *) (* En dépliant la boucle de récurrence, on voit que *) (* f n = h (h (... (h g)...)) *) (* ce qui est une itération n fois de la fonction h *) Let Rec : forall (X : Prop) (g : X) (h : X->X), N->X := fun X g h => (fun n => n X h g). (* En guise d'application, fournissons la factorielle : *) (* pour la factorielle, on a le cas n+1 -> (n+1)*(factorielle n) *) (* on a donc besoin de n+1 qui n'est pas donné par notre schéma. *) (* Qu'à cela ne tienne : on va faire une fonction f qui renvoie un *) (* couple d'entiers : *) (* Nous allons donc prendre f n = (factorielle n, n) *) (* ce qui donne n+1 -> (P1 (f n)) * ((P2 (f n))+1) *) Let consNN := cons N N. Infix "/" := consNN. Let f : couple N N -> couple N N := fun c => let fact := P1 _ _ c in let n := P2 _ _ c in mul fact (S n) / (S n). Definition factorielle : N -> N := fun n => (* on a factorielle2 : N -> couple' *) (* factorielle2(n) = (n!, n) *) let factorielle2 := Rec _ (I/O) f in P1 _ _ (factorielle2 n). (* et ça marche... *) Eval compute in (factorielle III). End EntiersDeChurchV2.