(* This OCaml script was exported from a Jupyter notebook using an open-source software (under the MIT License) written by @Naereen from https://github.com/Naereen/Jupyter-Notebook-OCaml This software is still in development, please notify me of a bug at https://github.com/Naereen/Jupyter-Notebook-OCaml/issues/new if you find one *) (* # Table of Contents

1  TP 6 - Programmation pour la préparation à l'agrégation maths option info
2  Représentation des 𝜆-termes en OCaml
2.1  Grammaire
2.2  Ex1. Ecrire un type Caml représentant les 𝜆-termes
2.3  Ex2. Ecrire une fonction qui affiche un 𝜆-terme en une chaîne de caractère
2.4  Ex3. Bonus : Ecrire une fonction qui transforme un 𝜆-terme en une chaîne représentant une fonction "anonyme" exécutable par Python. Rappel : lambda x: ... correspond à 𝜆𝑥.<...>
3  Calculs ?
4  Quelques termes utiles ?
4.1  Une valeur "nulle"
4.2  Composition
4.3  Conditionnelles
4.4  Nombres entiers en codage de Chuch
4.5  Successeur
4.6  Addition
4.7  Multiplication
4.8  Paires
4.9  Bonus : prédecesseur
4.10  Listes
4.11  Récursion 𝑈
4.12  Point fixe 𝑌
4.13  Bonus : la factorielle en 𝜆-calcul
5  Conclusion
*) (* # TP 6 - Programmation pour la préparation à l'agrégation maths option info TP 6 : Lambda calcul, représentations, calculs et quelques termes pratiques. - Référence en théorie : [ce poly en français de Jean Goubault-Larrecqu (ENS Cachan)](http://www.lsv.fr/%7Egoubault/Lambda/lambda.pdf) ou le livre "Logique réduction résolution", par René Lalement. - Pour la pratique : [ce post de blog en anglais](http://matt.might.net/articles/python-church-y-combinator/) - Pour plus, [cette page wikipédia](https://fr.wikipedia.org/wiki/Lambda-calcul). *) (* - En OCaml. *) (* In[1]: *) let print = Printf.printf;; Sys.command "ocaml -version";; (* ---- # Représentation des $\lambda$-termes en OCaml ## Grammaire Avec une [grammaire BNF](https://fr.wikipedia.org/wiki/Forme_de_Backus-Naur), si `` désigne un nom d'expression valide (on se limitera à des noms en miniscules consistitués des 26 lettres a,b,..,z) : ::= | () | fun -> | () *) (* ## Ex1. Ecrire un type Caml représentant les $\lambda$-termes *) (* In[6]: *) type variable = string;; type terme = | V of variable | A of terme * terme | F of variable * terme ;; (* Par exemple, l'identité est le terme $\lambda x. x$. *) (* In[7]: *) let identite = F("x", V("x"));; (* In[8]: *) let identite_2 = F("y", V("y"));; (* Les deux termes sont différents mais égaux à $\alpha$-renomage près. *) (* Un autre exemple est le terme $\Omega = (\lambda x. xx)(\lambda x. xx)$ (qui est le plus petit terme dont l'exécution par $\beta$-réduction ne termine pas - cf [ce poly p7](http://www.lsv.fr/%7Egoubault/Lambda/lambda.pdf) si besoin). *) (* In[9]: *) let omega = A(F("x", A(V("x"), V("x"))), F("x", A(V("x"), V("x"))));; (* In[10]: *) let u = F("x", A(V("x"), V("x")));; let omega = A(u, u);;; (* ## Ex2. Ecrire une fonction qui affiche un $\lambda$-terme en une chaîne de caractère C'est très rapide. *) (* In[13]: *) let sprintf = Format.sprintf;; let rec string_of_terme = function | V(s) -> s | A(u, v) -> sprintf "(%s)(%s)" (string_of_terme u) (string_of_terme v) (* "(" ^ (string_of_terme u) ^ ")" ^ "(" ^ (string_of_terme v) ^ ")" *) | F(s, u) -> sprintf "λ %s. (%s)" s (string_of_terme u) (* "lambda " ^ s ^ ".(" ^ (string_of_terme u) *) ;; (* In[ ]: *) print_endline (string_of_terme identite);; print_endline (string_of_terme identite_2);; print_endline (string_of_terme omega);; (* ## Ex3. Bonus : Ecrire une fonction qui transforme un $\lambda$-terme en une chaîne représentant une fonction "anonyme" exécutable par Python. Rappel : `lambda x: ...` correspond à $\lambda x. <...>$ *) (* In[13]: *) let sprintf = Format.sprintf;; let rec python_of_terme = function | V(s) -> s | A(u, v) -> sprintf "(%s)(%s)" (python_of_terme u) (python_of_terme v) | F(s, u) -> sprintf "lambda %s: (%s)" s (python_of_terme u) ;; (* In[15]: *) print_endline (python_of_terme identite);; print_endline (python_of_terme identite_2);; print_endline (python_of_terme omega);; (* On peut ensuite simplement appeler Python sur un terme et vérifier s'il s'exécute ou non. *) (* In[35]: *) let execute_python_string (s : string) : int = Sys.command (sprintf "python -c 'print(%s)'" s) ;; (* In[36]: *) execute_python_string (python_of_terme identite);; (* On peut vérifier avec Python que ce terme $\Omega$ ne termine pas : *) (* In[34]: *) execute_python_string (python_of_terme omega);; (* ---- # Calculs ? *) (* ---- # Quelques termes utiles ? On peut définir des $\lambda$-termes utiles avec notre représentation, et on vérifiera ensuite en les exécutant via Python qu'ils sont corrects. *) (* ## Une valeur "nulle" *) (* In[37]: *) let none = F("x", V("x"));; (* ## Composition *) (* In[54]: *) let compose u v = A(u, v);; (* ## Conditionnelles Ce n'est qu'un des encodages possibles. *) (* In[38]: *) let si = F("cond", F("v", F("f", A(A(V("cond"), V("v")), V("f")))));; (* In[39]: *) print_endline (string_of_terme si);; (* In[40]: *) let vrai = F("v", F("f", V("v")));; let faux = F("v", F("f", V("f")));; (* In[41]: *) print_endline (string_of_terme vrai);; print_endline (string_of_terme faux);; (* ## Nombres entiers en codage de Chuch On rappelle que pour $n \in \mathbb{N}$, $[n] = \lambda f. \lambda x. f^n(x)$ est son codage dit codage de Church dans les $\lambda$-termes. *) (* In[45]: *) let zero = F("f", F("x", V("x")));; let un = F("f", F("x", A(V("f"), V("x"))));; (* In[50]: *) let terme_of_int (n : int) : terme = let rec aux = function | 0 -> V("x") | n -> A(V("f"), aux (n-1)) in F("f", F("x", (aux n))) ;; (* In[51]: *) let deux = terme_of_int 2;; (* In[53]: *) print_endline (string_of_terme deux);; execute_python_string (python_of_terme deux);; (* On peut faire l'opération inverse, interpréter un entier de Church en Python. *) (* In[55]: *) let entier_natif_python = "lambda c: c(lambda x: x+1)(0)";; (* In[56]: *) execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme deux));; (* > On est obligé de passer par une astuce, parce que $\lambda x. x + 1$ et $0$ ne sont pas des $\lambda$-termes. *) (* In[58]: *) execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (terme_of_int 10)));; (* Bien sûr, tout ça est très limité ! *) (* In[66]: *) execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (terme_of_int 100)));; (* ## Successeur *) (* Le successeur s'écrit $\mathrm{succ} = \lambda n. \lambda f. \lambda z. f(n(f)(z))$. *) (* In[72]: *) let successeur = F("n", F("f", F("z", A(V("f"), A(A(V("n"), V("f")), V("z"))))));; (* In[92]: *) print_endline (string_of_terme successeur);; (* In[70]: *) let dix = terme_of_int 10;; let onze = A(successeur, dix);; (* A noter que ce terme `onze` ne sera pas le même que celui (plus court) obtenu par `terme_of_int 11` : *) (* In[73]: *) let onze2 = terme_of_int 11;; (* Mais ils s'exécutent de la même façon : *) (* In[74]: *) execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme dix));; execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme onze));; execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme onze2));; (* ## Addition *) (* La somme s'écrit $\mathrm{somme} = \lambda n. \lambda m. \lambda f. \lambda z. n(f)(m(f)(z))$. *) (* In[90]: *) let somme = F("n", F("m", F("f", F("z", A((A(V("n"), V("f"))), A((A(V("m"), V("f"))), V("z")) )))));; (* In[91]: *) print_endline (string_of_terme somme);; (* In[87]: *) let trois = A(A(somme, un), deux);; (* Comme pour le successeur, ce terme est bien plus compliqué que l'encodage de Church, mais ils s'exécutent de la même manière. *) (* In[88]: *) let trois2 = terme_of_int 3;; (* In[89]: *) execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme trois));; execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme trois2));; (* ## Multiplication *) (* La multiplication est $\mathrm{mul} = \lambda n. \lambda m. \lambda f. \lambda z. m(n(f))(z)$. *) (* In[122]: *) let mul = F("n", F("m", F("f", F("z", A(A(V("m"), A(V("n"), V("f"))), V("z"))))));; (* In[123]: *) let trois = terme_of_int 3 ;; let six = A(A(mul, trois), deux);; let six2 = A(A(mul, deux), trois);; (* Comme pour le successeur, ce terme est bien plus compliqué que l'encodage de Church, mais ils s'exécutent de la même manière. *) (* In[124]: *) execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme six));; execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme six2));; execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (terme_of_int 6)));; (* ## Paires *) (* La représentation de la paire est simplement $\mathrm{pair} = \lambda a. \lambda b. \lambda f. f(a)(b)$. *) (* In[127]: *) let a = V("a") and b = V("b") and f = V("f");; let pair = F("a", F("b", F("f", A(A(f, a), b))));; (* Et ensuite les deux extracteurs sont immédiats : $\mathrm{gauche} = \lambda p. p(\lambda a. \lambda b. a)$ et $\mathrm{droite} = \lambda p. p(\lambda a. \lambda b. b)$. (on retrouve `vrai` et `faux`) *) (* In[130]: *) let gauche = F("f", A(f, vrai));; let droite = F("f", A(f, faux));; (* In[133]: *) let exemple_pair = A(A(pair, deux), trois);; (* On vérifie qu'on peut extraire `[2]` et `[3]` de cette paire `[(2, 3)]` : *) (* In[134]: *) execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (A(gauche, exemple_pair))));; execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (A(droite, exemple_pair))));; (* ## Bonus : prédecesseur *) (* > Avec les paires, c'est possible. > Idée de l'algorithme : en ayant `[n]`, on commence par la paire `[(0, 0)]` et on itère la fonction `fun (a,b) -> (a+1, a)` exactement `n` fois (et ça c'est facile par définition du codage `[n]`, ce qui donne la paire `[(n, n-1)]` et en récupérant la deuxième coordonnée on a `[n-1]`. > C'est corrigé en Exercice 12 du poly de Jean Goubault-Larrecqu. On va découper ça en morceau : *) (* In[137]: *) let constructeur_pair u v = A(A(pair, u), v);; let pi1 u = A(gauche, u);; let pi2 u = A(droite, u);; let constructeur_succ u = A(successeur, u);; let pair_00 = constructeur_pair zero zero;; (* In[139]: *) let p = V("p");; let succ_1 = F("p", constructeur_pair (constructeur_succ(pi1(p))) (pi1(p)));; (* In[140]: *) let n = V("n");; let predecesseur = F("n", pi2(A(A(n, succ_1), pair_00)));; (* In[142]: *) let cinq = A(predecesseur, (terme_of_int 6));; let cinq2 = terme_of_int 5;; (* Comme pour le successeur, ce terme est bien plus compliqué que l'encodage de Church, mais ils s'exécutent de la même manière. *) (* In[143]: *) execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme cinq));; execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme cinq2));; (* On vérifie que `pred 0 = 0` : *) (* In[146]: *) let zero2 = A(predecesseur, zero);; (* In[147]: *) execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme zero2));; execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme zero));; (* ## Listes *) (* ## Récursion $U$ *) (* ## Point fixe $Y$ *) (* ## Bonus : la factorielle en $\lambda$-calcul *) (* ---- # Conclusion Fin. À la séance prochaine. Le TP6 traitera de ?? (en février). *)