Ce notebook est inspiré de ce post de blog du Professeur Matt Might, qui implémente un mini langage de programmation en $\lambda$-calcul, en Python. Je vais faire la même chose en OCaml.
On rappelle que les expressions du 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} $$
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.
Avec une grammaire BNF, si <var> désigne un nom d'expression valide (on se limitera à des noms en miniscules consistitués des 26 lettres a,b,..,z) :
<exp> ::= <var>
| <exp>(<exp>)
| fun <var> -> <exp>
| (<exp>)let identite = fun x -> x ;;
let vide = fun x -> x ;;
La conditionnelle est si cond alors valeur_vraie sinon valeur_fausse.
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 == e2let vrai = fun valeur_vraie valeur_fausse -> valeur_vraie ;;
let faux = fun valeur_vraie valeur_fausse -> valeur_fausse ;;
La négation est facile !
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.
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 !
let paresseux = fun f -> fun () -> f ;;
La représentation de Church consiste a écrire $n$ comme $\lambda f. \lambda z. f^n z$.
type 'a nombres = ('a -> 'a) -> 'a -> 'a;; (* inutilisé *)
type entiers_church = (int -> int) -> int -> int;;
$0$ est trivialement $\lambda f. \lambda z. z$ :
let zero = fun (f : ('a -> 'a)) (z : 'a) -> z ;;
$1$ est $\lambda f. \lambda z. f z$ :
let un = fun (f : ('a -> 'a)) -> f ;;
Avec l'opérateur de composition, l'écriture des entiers suivants est facile.
let compose = fun f g x -> f (g x);;
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 :
let rec entierChurch (n : int) =
fun f z -> if n = 0 then z else f ((entierChurch (n-1)) f z)
;;
Par exemple :
(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) :
let entierNatif c : int =
c (fun x -> x + 1) 0
;;
Un petit test :
entierNatif (si vrai zero un);; (* 0 *)
entierNatif (si faux zero un);; (* 1 *)
entierNatif (entierChurch 100);; (* 100 *)
On a besoin de pouvoir tester si $n \leq 0$ (ou $n = 0$) en fait.
(* prend un lambda f lambda z. ... est donne vrai ssi n = 0 ou faux sinon *)
let estnul = fun n -> n (fun z -> faux) (vrai);;
(* 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 :
let estnonnul2 = fun n -> non (estnul n);;
entierNatif (si (estnul zero) zero un);; (* 0 *)
entierNatif (si (estnul un) zero un);; (* 1 *)
entierNatif (si (estnul deux) zero un);; (* 1 *)
entierNatif (si (estnonnul zero) zero un);; (* 0 *)
entierNatif (si (estnonnul un) zero un);; (* 1 *)
entierNatif (si (estnonnul deux) zero un);; (* 1 *)
entierNatif (si (non (estnul zero)) zero un);; (* 0 *)
entierNatif (si (non (estnul un)) zero un);; (* 1 *)
entierNatif (si (non (estnul deux)) zero un);; (* 1 *)
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))$.
let succ = fun n f z -> f ((n f) z) ;;
entierNatif (succ un);; (* 2 *)
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 :
let succ_de_un = succ un;;
(succ_de_un) (fun x -> x + 1);;
(succ_de_un) (fun x -> x ^ "0");;
(succ un) (fun x -> x ^ "0");;
(* une valeur fraîchement calculée, sans contrainte *)
Vue la représentation de Church, $\lambda n. n-1$ n'existe pas... mais on peut tricher.
let pred = fun n ->
if (entierNatif n) > 0 then entierChurch ((entierNatif n) - 1)
else zero
;;
entierNatif (pred deux);; (* 1 *)
entierNatif (pred trois);; (* 2 *)
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))$.
let somme = fun n m f z -> n(f)( m(f)(z));;
let cinq = somme deux trois ;;
entierNatif cinq;;
let sept = somme cinq deux ;;
entierNatif sept;;
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))...))$.
let produit = fun n m f z -> m(n(f))(z);;
On peut faire encore mieux avec l'opérateur de composition :
let produit = fun n m -> compose m n;;
let six = produit deux trois ;;
entierNatif six;;
let huit = produit deux quatre ;;
entierNatif huit;;
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) == blet paire = fun a b -> fun f -> f(a)(b);;
let gauche = fun p -> p(fun a b -> a);;
let droite = fun p -> p(fun a b -> b);;
entierNatif (gauche (paire zero un));;
entierNatif (droite (paire zero un));;
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é.
entierNatif (pred deux);; (* 1 *)
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.
let listevide = fun survide surpasvide -> survide;;
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.
let estvide = fun liste -> liste (vrai) (fun tt qu -> faux);;
Deux tests :
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.
let tete = fun liste -> liste (vide) (fun tt qu -> tt);;
let queue = fun liste -> liste (vide) (fun tt qu -> qu);;
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 :
cons un (cons un listevide);; (* 8 variables pour une liste de taille 2 *)
cons un (cons un (cons un (cons un listevide)));; (* 14 variables pour une liste de taille 4 *)
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 :
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 :
let pop liste =
si (estvide liste) (listevide) (queue liste)
;;
let ieme n liste =
tete (n pop liste)
;;
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é !
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 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.
let rec y = fun f -> f (y(f));;
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)$.
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 :
let fact = y(fun f n -> si (estnul n) (un) (produit n (f (pred n))));;
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.