(*
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
*)
(* # Lambda-calcul implémenté en OCaml
Ce notebook est inspiré de [ce post de blog du Professeur Matt Might](http://matt.might.net/articles/python-church-y-combinator/), qui implémente un mini langage de programmation en $\lambda$-calcul, en Python.
Je vais faire la même chose en OCaml.
## Expressions
On rappelle que les expressions du [Lambda calcul](https://fr.wikipedia.org/wiki/Lambda-calcul), ou $\lambda$-calcul, sont les suivantes :
$$ \begin{cases}
x, y, z & \text{(des variables)} \\
u v & \text{(application de deux termes}\, u, v\; \text{)} \\
\lambda x. v & \text{(lambda-function prenant la variable}\; x \;\text{et le terme}\; v \;\text{)}
\end{cases} $$
## But ?
Le but ne va pas être de les représenter comme ça avec des types formels en Caml, mais plutôt d'utiliser les constructions de Caml, respectivement `u(v)` et `fun x -> v` pour l'application et les fonctions anonymes, et encoder des fonctionnalités de plus haut niveau dans ce langage réduit.
## Grammaire
Avec une grammaire BNF, si `` désigne un nom d'expression valide (on se limitera à des noms en miniscules consistitués des 26 lettres `a,b,..,z`) :
::=
| ()
| fun ->
| () *)
(* ----
## L'identité *)
(* In[3]: *)
let identite = fun x -> x ;;
(* In[4]: *)
let vide = fun x -> x ;;
(* ## Conditionnelles
La conditionnelle est `si cond alors valeur_vraie sinon valeur_fausse`. *)
(* In[13]: *)
let si = fun cond valeur_vraie valeur_fausse -> cond valeur_vraie valeur_fausse ;;
(* C'est très simple, du moment qu'on s'assure que `cond` est soit `vrai` soit `faux` tels que définis par leur comportement :
si vrai e1 e2 == e1
si faux e1 e2 == e2 *)
(* In[14]: *)
let vrai = fun valeur_vraie valeur_fausse -> valeur_vraie ;;
let faux = fun valeur_vraie valeur_fausse -> valeur_fausse ;;
(* La négation est facile ! *)
(* In[15]: *)
let non = fun v x y -> v y x;;
(* En fait, on va forcer une évaluation paresseuse, comme ça si l'une des deux expressions ne terminent pas, l'évaluation fonctionne quand même. *)
(* In[16]: *)
let vrai_paresseux = fun valeur_vraie valeur_fausse -> valeur_vraie () ;;
let faux_paresseux = fun valeur_vraie valeur_fausse -> valeur_fausse () ;;
(* Pour rendre paresseux un terme, rien de plus simple ! *)
(* In[17]: *)
let paresseux = fun f -> fun () -> f ;;
(* ## Nombres
La représentation de Church consiste a écrire $n$ comme $\lambda f. \lambda z. f^n z$. *)
(* In[18]: *)
type 'a nombres = ('a -> 'a) -> 'a -> 'a;; (* inutilisé *)
type entiers_church = (int -> int) -> int -> int;;
(* $0$ est trivialement $\lambda f. \lambda z. z$ : *)
(* In[34]: *)
let zero = fun (f : ('a -> 'a)) (z : 'a) -> z ;;
(* $1$ est $\lambda f. \lambda z. f z$ : *)
(* In[35]: *)
let un = fun (f : ('a -> 'a)) -> f ;;
(* Avec l'opérateur de composition, l'écriture des entiers suivants est facile. *)
(* In[36]: *)
let compose = fun f g x -> f (g x);;
(* In[37]: *)
let deux = fun f -> compose f f;; (* == compose f (un f) *)
let trois = fun f -> compose f (deux f) ;;
let quatre = fun f -> compose f (trois f) ;;
(* etc *);;
(* On peut généraliser ça, avec une fonction qui transforme un entier (`int`) de Caml en un entier de Church : *)
(* In[38]: *)
let rec entierChurch (n : int) =
fun f z -> if n = 0 then z else f ((entierChurch (n-1)) f z)
;;
(* Par exemple : *)
(* In[39]: *)
(entierChurch 0) (fun x -> x + 1) 0;; (* 0 *)
(entierChurch 7) (fun x -> x + 1) 0;; (* 7 *)
(entierChurch 3) (fun x -> 2*x) 1;; (* 8 *);;
(* Et une fonction qui fait l'inverse (note : cette fonction n'est *pas* un $\lambda$-terme) : *)
(* In[40]: *)
let entierNatif c : int =
c (fun x -> x + 1) 0
;;
(* Un petit test : *)
(* In[41]: *)
entierNatif (si vrai zero un);; (* 0 *)
entierNatif (si faux zero un);; (* 1 *);;
(* In[42]: *)
entierNatif (entierChurch 100);; (* 100 *);;
(* ## Test d'inégalité
On a besoin de pouvoir tester si $n \leq 0$ (ou $n = 0$) en fait. *)
(* In[43]: *)
(* prend un lambda f lambda z. ... est donne vrai ssi n = 0 ou faux sinon *)
let estnul = fun n -> n (fun z -> faux) (vrai);;
(* In[44]: *)
(* prend un lambda f lambda z. ... est donne vrai ssi n > 0 ou faux sinon *)
let estnonnul = fun n -> n (fun z -> vrai) (faux);;
(* On peut proposer cette autre implémentation, qui "fonctionne" pareil (au sens calcul des $\beta$-réductions) mais est plus compliquée : *)
(* In[45]: *)
let estnonnul2 = fun n -> non (estnul n);;
(* In[46]: *)
entierNatif (si (estnul zero) zero un);; (* 0 *)
entierNatif (si (estnul un) zero un);; (* 1 *)
entierNatif (si (estnul deux) zero un);; (* 1 *);;
(* In[47]: *)
entierNatif (si (estnonnul zero) zero un);; (* 0 *)
entierNatif (si (estnonnul un) zero un);; (* 1 *)
entierNatif (si (estnonnul deux) zero un);; (* 1 *);;
(* In[48]: *)
entierNatif (si (non (estnul zero)) zero un);; (* 0 *)
entierNatif (si (non (estnul un)) zero un);; (* 1 *)
entierNatif (si (non (estnul deux)) zero un);; (* 1 *);;
(* ## Successeurs
Vue la représentation de Churc, $n+1$ consiste a appliquer l'argument $f$ une fois de plus :
$f^{n+1}(z) = f (f^n(z))$. *)
(* In[49]: *)
let succ = fun n f z -> f ((n f) z) ;;
(* In[50]: *)
entierNatif (succ un);; (* 2 *);;
(* In[51]: *)
deux;;
succ un;;
(* On remarque qu'ils ont le même typage, mais OCaml indique qu'il a moins d'informations à propos du deuxième : ce `'_a` signifie que le type est *contraint*, il sera fixé dès la première utilisation de cette fonction.
C'est assez mystérieux, mais il faut retenir le point suivant : `deux` était écrit manuellement, donc le système a vu le terme en entier, il le connaît et saît que `deux = fun f -> fun x -> f (f x))`, pas de surprise. Par contre, `succ un` est le résultat d'une évaluation *partielle* et vaut `fun f z -> f ((deux f) z)`. Sauf que le système ne calcule pas tout et laisse l'évaluation partielle ! (heureusement !) *)
(* Si on appelle `succ un` à une fonction, le `'_a` va être contraint, et on ne pourra pas s'en reservir : *)
(* In[54]: *)
let succ_de_un = succ un;;
(* In[55]: *)
(succ_de_un) (fun x -> x + 1);;
(* In[56]: *)
(succ_de_un) (fun x -> x ^ "0");;
(* In[57]: *)
(succ un) (fun x -> x ^ "0");;
(* une valeur fraîchement calculée, sans contrainte *);;
(* ## Prédecesseurs
Vue la représentation de Church, $\lambda n. n-1$ n'existe pas... mais on peut tricher. *)
(* In[30]: *)
let pred = fun n ->
if (entierNatif n) > 0 then entierChurch ((entierNatif n) - 1)
else zero
;;
(* In[31]: *)
entierNatif (pred deux);; (* 1 *);;
(* In[32]: *)
entierNatif (pred trois);; (* 2 *);;
(* ## Addition
Pour ajouter $n$ et $m$, il faut appliquer une fonction $f$ $n$ fois puis $m$ fois : $f^{n+m}(z) = f^n(f^m(z))$. *)
(* In[33]: *)
let somme = fun n m f z -> n(f)( m(f)(z));;
(* In[34]: *)
let cinq = somme deux trois ;;
(* In[35]: *)
entierNatif cinq;;
(* In[36]: *)
let sept = somme cinq deux ;;
(* In[37]: *)
entierNatif sept;;
(* ## Multiplication
Pour multiplier $n$ et $m$, il faut appliquer le codage de $n$ exactement $m$ fois : $f^{nm}(z) = (f^n(f^n(...(f^n(z))...))$. *)
(* In[38]: *)
let produit = fun n m f z -> m(n(f))(z);;
(* On peut faire encore mieux avec l'opérateur de composition : *)
(* In[39]: *)
let produit = fun n m -> compose m n;;
(* In[40]: *)
let six = produit deux trois ;;
(* In[41]: *)
entierNatif six;;
(* In[42]: *)
let huit = produit deux quatre ;;
(* In[43]: *)
entierNatif huit;;
(* ## Paires
On va écrire un constructeur de paires, `paire a b` qui sera comme `(a, b)`, et deux destructeurs, `gauche` et `droite`, qui vérifient :
gauche (paire a b) == a
droite (paire a b) == b *)
(* In[75]: *)
let paire = fun a b -> fun f -> f(a)(b);;
(* In[76]: *)
let gauche = fun p -> p(fun a b -> a);;
let droite = fun p -> p(fun a b -> b);;
(* In[77]: *)
entierNatif (gauche (paire zero un));;
entierNatif (droite (paire zero un));;
(* ## Prédécesseurs, deuxième essai
Il y a une façon, longue et compliquée ([source](http://gregfjohnson.com/pred/)) d'y arriver, avec des paires. *)
(* In[78]: *)
let pred n suivant premier =
let pred_suivant = paire vrai premier in
let pred_premier = fun p ->
si (gauche p)
(paire faux premier)
(paire faux (suivant (droite p)))
in
let paire_finale = n pred_suivant pred_premier in
droite paire_finale
;;
(* Malheureusement, ce n'est pas bien typé. *)
(* In[79]: *)
entierNatif (pred deux);; (* 1 *);;
(* ## Listes
Pour construire des listes (simplement chaînées), on a besoin d'une valeur pour la liste vide, `listevide`, d'un constructeur pour une liste `cons`, un prédicat pour la liste vide `estvide`, un accesseur `tete` et `queue`, et avec les contraintes suivantes (avec `vrai`, `faux` définis comme plus haut) :
estvide (listevide) == vrai
estvide (cons tt qu) == faux
tete (cons tt qu) == tt
queue (cons tt qu) == qu
On va stocker tout ça avec des fonctions qui attendront deux arguments (deux fonctions - rappel tout est fonction en $\lambda$-calcul), l'une appellée si la liste est vide, l'autre si la liste n'est pas vide. *)
(* In[58]: *)
let listevide = fun survide surpasvide -> survide;;
(* In[59]: *)
let cons = fun hd tl -> fun survide surpasvide -> surpasvide hd tl;;
(* Avec cette construction, `estvide` est assez simple : `survide` est `() -> vrai` et `surpasvide` est `tt qu -> faux`. *)
(* In[60]: *)
let estvide = fun liste -> liste (vrai) (fun tt qu -> faux);;
(* Deux tests : *)
(* In[61]: *)
entierNatif (si (estvide (listevide)) un zero);; (* estvide listevide == vrai *)
entierNatif (si (estvide (cons un listevide)) un zero);; (* estvide (cons un listevide) == faux *);;
(* Et pour les deux extracteurs, c'est très facile avec cet encodage. *)
(* In[62]: *)
let tete = fun liste -> liste (vide) (fun tt qu -> tt);;
let queue = fun liste -> liste (vide) (fun tt qu -> qu);;
(* In[69]: *)
entierNatif (tete (cons un listevide));;
entierNatif (tete (queue (cons deux (cons un listevide))));;
entierNatif (tete (queue (cons trois (cons deux (cons un listevide)))));;
(* Visualisons les types que Caml trouve a des listes de tailles croissantes : *)
(* In[70]: *)
cons un (cons un listevide);; (* 8 variables pour une liste de taille 2 *);;
(* In[71]: *)
cons un (cons un (cons un (cons un listevide)));; (* 14 variables pour une liste de taille 4 *);;
(* In[72]: *)
cons un (cons un (cons un (cons un (cons un (cons un (cons un (cons un listevide)))))));; (* 26 variables pour une liste de taille 7 *);;
(* Pour ces raisons là, on se rend compte que le type donné par Caml à une liste de taille $k$ croît linéairement *en taille* en fonction de $k$ !
Aucun espoir donc (avec cet encodage) d'avoir un type générique pour les listes représentés en Caml.
Et donc nous ne sommes pas surpris de voir cet essai échouer : *)
(* In[68]: *)
let rec longueur liste =
liste (zero) (fun t q -> succ (longueur q))
;;
(* En effet, `longueur` devrait être bien typée et `liste` et `q` devraient avoir le même type, or le type de `liste` est strictement plus grand que celui de `q`... *)
(* On peut essayer de faire une fonction `ieme`.
On veut que `ieme zero liste = tete` et `ieme n liste = ieme (pred n) (queue liste)`.
En écrivant en haut niveau, on aimerait pouvoir faire : *)
(* In[87]: *)
let pop liste =
si (estvide liste) (listevide) (queue liste)
;;
(* In[86]: *)
let ieme n liste =
tete (n pop liste)
;;
(* ## La fonction U
C'est le premier indice que le $\lambda$-calcul peut être utilisé comme modèle de calcul : le terme $U : f \to f(f)$ ne termine pas si on l'applique à lui-même.
Mais ce sera la faiblesse de l'utilisation de Caml : ce terme ne peut être correctement typé ! *)
(* In[55]: *)
let u = fun f -> f (f);;
(* A noter que même dans un langage non typé (par exemple Python), on peut définir $U$ mais son exécution échouera, soit à caude d'un dépassement de pile, soit parce qu'elle ne termine pas. *)
(* ## La récursion via la fonction Y
La fonction $Y$ trouve le point fixe d'une autre fonction.
C'est très utile pour définir des fonctions par récurrence.
Par exemple, la factorielle est le point fixe de la fonction suivante :
"$\lambda f. \lambda n. 1$ si $n \leq 0$ sinon $n * f(n-1)$" (écrite dans un langage plus haut niveau, pas en $\lambda$-calcul).
$Y$ satisfait ces contraintes : $Y(F) = f$ et $f = F(f)$.
Donc $Y(F) = F(Y(F))$ et donc $Y = \lambda F. F(Y(F))$. Mais ce premier essai ne marche pas. *)
(* In[56]: *)
let rec y = fun f -> f (y(f));;
(* In[57]: *)
let fact = y(fun f n -> si (estnul n) (un) (produit n (f (pred n))));;
(* On utilise la $\eta$-expansion : si $e$ termine, $e$ est équivalent (ie tout calcul donne le même terme) à $\lambda x. e(x)$. *)
(* In[58]: *)
let rec y = fun f -> f (fun x -> y(f)(x));;
(* Par contre, le typage n'arrive toujours pas à trouver que l'expression suivante devrait être bien définie : *)
(* In[59]: *)
let fact = y(fun f n -> si (estnul n) (un) (produit n (f (pred n))));;
(* ## Conclusion
Je n'ai pas réussi à traduire intégralement la prouesse initiale, écrite en Python, par Matt Might.
Dommage, le typage de Caml est trop strict pour cet exercice. *)