(* 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  Lambda-calcul implémenté en OCaml
1.1  Expressions
1.2  But ?
1.3  Grammaire
1.4  L'identité
1.5  Conditionnelles
1.6  Nombres
1.7  Test d'inégalité
1.8  Successeurs
1.9  Prédecesseurs
1.10  Addition
1.11  Multiplication
1.12  Paires
1.13  Prédécesseurs, deuxième essai
1.14  Listes
1.15  La fonction U
1.16  La récursion via la fonction Y
1.17  Conclusion
*) (* # 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. *)