(*
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
*)
(* # 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). *)