{
"cells": [
{
"cell_type": "markdown",
"metadata": {
"toc": "true"
},
"source": [
"# Table of Contents\n",
" "
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Lambda-calcul implémenté en OCaml\n",
"\n",
"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.\n",
"Je vais faire la même chose en OCaml.\n",
"\n",
"## Expressions\n",
"On rappelle que les expressions du [Lambda calcul](https://fr.wikipedia.org/wiki/Lambda-calcul), ou $\\lambda$-calcul, sont les suivantes :\n",
"$$ \\begin{cases}\n",
"x, y, z & \\text{(des variables)} \\\\\n",
"u v & \\text{(application de deux termes}\\, u, v\\; \\text{)} \\\\\n",
"\\lambda x. v & \\text{(lambda-function prenant la variable}\\; x \\;\\text{et le terme}\\; v \\;\\text{)}\n",
"\\end{cases} $$\n",
"\n",
"## But ?\n",
"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.\n",
"\n",
"## Grammaire\n",
"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`) :\n",
"\n",
" ::= \n",
" | ()\n",
" | fun -> \n",
" | ()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"----\n",
"## L'identité"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val identite : 'a -> 'a = \n"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let identite = fun x -> x ;;"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val vide : 'a -> 'a = \n"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let vide = fun x -> x ;;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Conditionnelles\n",
"La conditionnelle est `si cond alors valeur_vraie sinon valeur_fausse`."
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val si : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = \n"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let si = fun cond valeur_vraie valeur_fausse -> cond valeur_vraie valeur_fausse ;;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"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 :\n",
"\n",
" si vrai e1 e2 == e1\n",
" si faux e1 e2 == e2"
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[14]\", line 1, characters 28-41:\n",
"Warning 27: unused variable valeur_fausse.\n"
]
},
{
"data": {
"text/plain": [
"val vrai : 'a -> 'b -> 'a = \n"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
},
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[14]\", line 2, characters 15-27:\n",
"Warning 27: unused variable valeur_vraie.\n"
]
},
{
"data": {
"text/plain": [
"val faux : 'a -> 'b -> 'b = \n"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let vrai = fun valeur_vraie valeur_fausse -> valeur_vraie ;;\n",
"let faux = fun valeur_vraie valeur_fausse -> valeur_fausse ;;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"La négation est facile !"
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val non : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c = \n"
]
},
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let non = fun v x y -> v y x;;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"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."
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[16]\", line 1, characters 38-51:\n",
"Warning 27: unused variable valeur_fausse.\n"
]
},
{
"data": {
"text/plain": [
"val vrai_paresseux : (unit -> 'a) -> 'b -> 'a = \n"
]
},
"execution_count": 16,
"metadata": {},
"output_type": "execute_result"
},
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[16]\", line 2, characters 25-37:\n",
"Warning 27: unused variable valeur_vraie.\n"
]
},
{
"data": {
"text/plain": [
"val faux_paresseux : 'a -> (unit -> 'b) -> 'b = \n"
]
},
"execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let vrai_paresseux = fun valeur_vraie valeur_fausse -> valeur_vraie () ;;\n",
"let faux_paresseux = fun valeur_vraie valeur_fausse -> valeur_fausse () ;;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Pour rendre paresseux un terme, rien de plus simple !"
]
},
{
"cell_type": "code",
"execution_count": 17,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val paresseux : 'a -> unit -> 'a = \n"
]
},
"execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let paresseux = fun f -> fun () -> f ;;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Nombres\n",
"La représentation de Church consiste a écrire $n$ comme $\\lambda f. \\lambda z. f^n z$."
]
},
{
"cell_type": "code",
"execution_count": 18,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"type 'a nombres = ('a -> 'a) -> 'a -> 'a\n"
]
},
"execution_count": 18,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"type entiers_church = (int -> int) -> int -> int\n"
]
},
"execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"type 'a nombres = ('a -> 'a) -> 'a -> 'a;; (* inutilisé *)\n",
"type entiers_church = (int -> int) -> int -> int;;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"$0$ est trivialement $\\lambda f. \\lambda z. z$ :"
]
},
{
"cell_type": "code",
"execution_count": 34,
"metadata": {
"scrolled": true
},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[34]\", line 1, characters 16-17:\n",
"Warning 27: unused variable f.\n"
]
},
{
"data": {
"text/plain": [
"val zero : ('a -> 'a) -> 'a -> 'a = \n"
]
},
"execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let zero = fun (f : ('a -> 'a)) (z : 'a) -> z ;;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"$1$ est $\\lambda f. \\lambda z. f z$ :"
]
},
{
"cell_type": "code",
"execution_count": 35,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val un : ('a -> 'a) -> 'a -> 'a = \n"
]
},
"execution_count": 35,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let un = fun (f : ('a -> 'a)) -> f ;;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Avec l'opérateur de composition, l'écriture des entiers suivants est facile."
]
},
{
"cell_type": "code",
"execution_count": 36,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b = \n"
]
},
"execution_count": 36,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let compose = fun f g x -> f (g x);;"
]
},
{
"cell_type": "code",
"execution_count": 37,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val deux : ('a -> 'a) -> 'a -> 'a = \n"
]
},
"execution_count": 37,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"val trois : ('a -> 'a) -> 'a -> 'a = \n"
]
},
"execution_count": 37,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"val quatre : ('a -> 'a) -> 'a -> 'a = \n"
]
},
"execution_count": 37,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let deux = fun f -> compose f f;; (* == compose f (un f) *)\n",
"let trois = fun f -> compose f (deux f) ;;\n",
"let quatre = fun f -> compose f (trois f) ;;\n",
"(* etc *)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On peut généraliser ça, avec une fonction qui transforme un entier (`int`) de Caml en un entier de Church :"
]
},
{
"cell_type": "code",
"execution_count": 38,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val entierChurch : int -> ('a -> 'a) -> 'a -> 'a = \n"
]
},
"execution_count": 38,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec entierChurch (n : int) =\n",
" fun f z -> if n = 0 then z else f ((entierChurch (n-1)) f z)\n",
";;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Par exemple :"
]
},
{
"cell_type": "code",
"execution_count": 39,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 0\n"
]
},
"execution_count": 39,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"- : int = 7\n"
]
},
"execution_count": 39,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"- : int = 8\n"
]
},
"execution_count": 39,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"(entierChurch 0) (fun x -> x + 1) 0;; (* 0 *)\n",
"(entierChurch 7) (fun x -> x + 1) 0;; (* 7 *)\n",
"(entierChurch 3) (fun x -> 2*x) 1;; (* 8 *)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Et une fonction qui fait l'inverse (note : cette fonction n'est *pas* un $\\lambda$-terme) :"
]
},
{
"cell_type": "code",
"execution_count": 40,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val entierNatif : ((int -> int) -> int -> int) -> int = \n"
]
},
"execution_count": 40,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let entierNatif c : int =\n",
" c (fun x -> x + 1) 0\n",
";;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Un petit test :"
]
},
{
"cell_type": "code",
"execution_count": 41,
"metadata": {
"scrolled": true
},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 0\n"
]
},
"execution_count": 41,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"- : int = 1\n"
]
},
"execution_count": 41,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif (si vrai zero un);; (* 0 *)\n",
"entierNatif (si faux zero un);; (* 1 *)"
]
},
{
"cell_type": "code",
"execution_count": 42,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 100\n"
]
},
"execution_count": 42,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif (entierChurch 100);; (* 100 *)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Test d'inégalité\n",
"On a besoin de pouvoir tester si $n \\leq 0$ (ou $n = 0$) en fait."
]
},
{
"cell_type": "code",
"execution_count": 43,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[43]\", line 2, characters 29-30:\n",
"Warning 27: unused variable z.\n"
]
},
{
"data": {
"text/plain": [
"val estnul : (('a -> 'b -> 'c -> 'c) -> ('d -> 'e -> 'd) -> 'f) -> 'f = \n"
]
},
"execution_count": 43,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"(* prend un lambda f lambda z. ... est donne vrai ssi n = 0 ou faux sinon *)\n",
"let estnul = fun n -> n (fun z -> faux) (vrai);;"
]
},
{
"cell_type": "code",
"execution_count": 44,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[44]\", line 2, characters 32-33:\n",
"Warning 27: unused variable z.\n"
]
},
{
"data": {
"text/plain": [
"val estnonnul : (('a -> 'b -> 'c -> 'b) -> ('d -> 'e -> 'e) -> 'f) -> 'f =\n",
" \n"
]
},
"execution_count": 44,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"(* prend un lambda f lambda z. ... est donne vrai ssi n > 0 ou faux sinon *)\n",
"let estnonnul = fun n -> n (fun z -> vrai) (faux);;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On peut proposer cette autre implémentation, qui \"fonctionne\" pareil (au sens calcul des $\\beta$-réductions) mais est plus compliquée :"
]
},
{
"cell_type": "code",
"execution_count": 45,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val estnonnul2 :\n",
" (('a -> 'b -> 'c -> 'c) -> ('d -> 'e -> 'd) -> 'f -> 'g -> 'h) ->\n",
" 'g -> 'f -> 'h = \n"
]
},
"execution_count": 45,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let estnonnul2 = fun n -> non (estnul n);;"
]
},
{
"cell_type": "code",
"execution_count": 46,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 0\n"
]
},
"execution_count": 46,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"- : int = 1\n"
]
},
"execution_count": 46,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"- : int = 1\n"
]
},
"execution_count": 46,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif (si (estnul zero) zero un);; (* 0 *)\n",
"entierNatif (si (estnul un) zero un);; (* 1 *)\n",
"entierNatif (si (estnul deux) zero un);; (* 1 *)"
]
},
{
"cell_type": "code",
"execution_count": 47,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 1\n"
]
},
"execution_count": 47,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"- : int = 0\n"
]
},
"execution_count": 47,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"- : int = 0\n"
]
},
"execution_count": 47,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif (si (estnonnul zero) zero un);; (* 0 *)\n",
"entierNatif (si (estnonnul un) zero un);; (* 1 *)\n",
"entierNatif (si (estnonnul deux) zero un);; (* 1 *)"
]
},
{
"cell_type": "code",
"execution_count": 48,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 1\n"
]
},
"execution_count": 48,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"- : int = 0\n"
]
},
"execution_count": 48,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"- : int = 0\n"
]
},
"execution_count": 48,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif (si (non (estnul zero)) zero un);; (* 0 *)\n",
"entierNatif (si (non (estnul un)) zero un);; (* 1 *)\n",
"entierNatif (si (non (estnul deux)) zero un);; (* 1 *)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Successeurs\n",
"Vue la représentation de Churc, $n+1$ consiste a appliquer l'argument $f$ une fois de plus :\n",
"$f^{n+1}(z) = f (f^n(z))$."
]
},
{
"cell_type": "code",
"execution_count": 49,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val succ : (('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b = \n"
]
},
"execution_count": 49,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let succ = fun n f z -> f ((n f) z) ;;"
]
},
{
"cell_type": "code",
"execution_count": 50,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 2\n"
]
},
"execution_count": 50,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif (succ un);; (* 2 *)"
]
},
{
"cell_type": "code",
"execution_count": 51,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : ('a -> 'a) -> 'a -> 'a = \n"
]
},
"execution_count": 51,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"- : ('_a -> '_a) -> '_a -> '_a = \n"
]
},
"execution_count": 51,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"deux;;\n",
"succ un;;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"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.\n",
"\n",
"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 !)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Si on appelle `succ un` à une fonction, le `'_a` va être contraint, et on ne pourra pas s'en reservir :"
]
},
{
"cell_type": "code",
"execution_count": 54,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val succ_de_un : ('_a -> '_a) -> '_a -> '_a = \n"
]
},
"execution_count": 54,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let succ_de_un = succ un;;"
]
},
{
"cell_type": "code",
"execution_count": 55,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int -> int = \n"
]
},
"execution_count": 55,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"(succ_de_un) (fun x -> x + 1);;"
]
},
{
"cell_type": "code",
"execution_count": 56,
"metadata": {},
"outputs": [
{
"ename": "error",
"evalue": "compile_error",
"output_type": "error",
"traceback": [
"\u001b[32mFile \"[56]\", line 1, characters 23-24:\n\u001b[31mError: This expression has type int but an expression was expected of type\n string\n\u001b[36m 1: \u001b[30m(succ_de_un) (fun x -> \u001b[4mx\u001b[0m\u001b[30m ^ \"0\");;\u001b[0m\n"
]
}
],
"source": [
"(succ_de_un) (fun x -> x ^ \"0\");;"
]
},
{
"cell_type": "code",
"execution_count": 57,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : string -> string = \n"
]
},
"execution_count": 57,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"(succ un) (fun x -> x ^ \"0\");;\n",
"(* une valeur fraîchement calculée, sans contrainte *)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Prédecesseurs\n",
"Vue la représentation de Church, $\\lambda n. n-1$ n'existe pas... mais on peut tricher."
]
},
{
"cell_type": "code",
"execution_count": 30,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val pred : ((int -> int) -> int -> int) -> ('a -> 'a) -> 'a -> 'a = \n"
]
},
"execution_count": 30,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let pred = fun n ->\n",
" if (entierNatif n) > 0 then entierChurch ((entierNatif n) - 1)\n",
" else zero\n",
";;"
]
},
{
"cell_type": "code",
"execution_count": 31,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 1\n"
]
},
"execution_count": 31,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif (pred deux);; (* 1 *)"
]
},
{
"cell_type": "code",
"execution_count": 32,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 2\n"
]
},
"execution_count": 32,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif (pred trois);; (* 2 *)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Addition\n",
"\n",
"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))$."
]
},
{
"cell_type": "code",
"execution_count": 33,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val somme : ('a -> 'b -> 'c) -> ('a -> 'd -> 'b) -> 'a -> 'd -> 'c = \n"
]
},
"execution_count": 33,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let somme = fun n m f z -> n(f)( m(f)(z));;"
]
},
{
"cell_type": "code",
"execution_count": 34,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val cinq : ('_a -> '_a) -> '_a -> '_a = \n"
]
},
"execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let cinq = somme deux trois ;;"
]
},
{
"cell_type": "code",
"execution_count": 35,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 5\n"
]
},
"execution_count": 35,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif cinq;;"
]
},
{
"cell_type": "code",
"execution_count": 36,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val sept : (int -> int) -> int -> int = \n"
]
},
"execution_count": 36,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let sept = somme cinq deux ;;"
]
},
{
"cell_type": "code",
"execution_count": 37,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 7\n"
]
},
"execution_count": 37,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif sept;;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Multiplication\n",
"\n",
"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))...))$."
]
},
{
"cell_type": "code",
"execution_count": 38,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val produit : ('a -> 'b) -> ('b -> 'c -> 'd) -> 'a -> 'c -> 'd = \n"
]
},
"execution_count": 38,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let produit = fun n m f z -> m(n(f))(z);;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On peut faire encore mieux avec l'opérateur de composition :"
]
},
{
"cell_type": "code",
"execution_count": 39,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val produit : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c = \n"
]
},
"execution_count": 39,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let produit = fun n m -> compose m n;;"
]
},
{
"cell_type": "code",
"execution_count": 40,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val six : ('_a -> '_a) -> '_a -> '_a = \n"
]
},
"execution_count": 40,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let six = produit deux trois ;;"
]
},
{
"cell_type": "code",
"execution_count": 41,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 6\n"
]
},
"execution_count": 41,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif six;;"
]
},
{
"cell_type": "code",
"execution_count": 42,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val huit : ('_a -> '_a) -> '_a -> '_a = \n"
]
},
"execution_count": 42,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let huit = produit deux quatre ;;"
]
},
{
"cell_type": "code",
"execution_count": 43,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 8\n"
]
},
"execution_count": 43,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif huit;;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Paires\n",
"\n",
"On va écrire un constructeur de paires, `paire a b` qui sera comme `(a, b)`, et deux destructeurs, `gauche` et `droite`, qui vérifient :\n",
"\n",
" gauche (paire a b) == a\n",
" droite (paire a b) == b"
]
},
{
"cell_type": "code",
"execution_count": 75,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val paire : 'a -> 'b -> ('a -> 'b -> 'c) -> 'c = \n"
]
},
"execution_count": 75,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let paire = fun a b -> fun f -> f(a)(b);;"
]
},
{
"cell_type": "code",
"execution_count": 76,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[76]\", line 1, characters 30-31:\n",
"Warning 27: unused variable b.\n"
]
},
{
"data": {
"text/plain": [
"val gauche : (('a -> 'b -> 'a) -> 'c) -> 'c = \n"
]
},
"execution_count": 76,
"metadata": {},
"output_type": "execute_result"
},
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[76]\", line 2, characters 28-29:\n",
"Warning 27: unused variable a.\n"
]
},
{
"data": {
"text/plain": [
"val droite : (('a -> 'b -> 'b) -> 'c) -> 'c = \n"
]
},
"execution_count": 76,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let gauche = fun p -> p(fun a b -> a);;\n",
"let droite = fun p -> p(fun a b -> b);;"
]
},
{
"cell_type": "code",
"execution_count": 77,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 0\n"
]
},
"execution_count": 77,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"- : int = 1\n"
]
},
"execution_count": 77,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif (gauche (paire zero un));;\n",
"entierNatif (droite (paire zero un));;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Prédécesseurs, deuxième essai\n",
"\n",
"Il y a une façon, longue et compliquée ([source](http://gregfjohnson.com/pred/)) d'y arriver, avec des paires."
]
},
{
"cell_type": "code",
"execution_count": 78,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val pred :\n",
" (((('a -> 'b -> 'a) -> 'c -> 'd) -> 'd) ->\n",
" ((('e -> 'e -> 'e) ->\n",
" ((('f -> 'g -> 'g) -> 'c -> 'h) -> 'h) ->\n",
" ((('i -> 'j -> 'j) -> 'k -> 'l) -> 'l) -> 'm) ->\n",
" 'm) ->\n",
" ('n -> 'o -> 'o) -> 'p) ->\n",
" ((((('f -> 'g -> 'g) -> 'c -> 'h) -> 'h) ->\n",
" ((('i -> 'j -> 'j) -> 'k -> 'l) -> 'l) -> 'm) ->\n",
" 'k) ->\n",
" 'c -> 'p = \n"
]
},
"execution_count": 78,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let pred n suivant premier =\n",
" let pred_suivant = paire vrai premier in\n",
" let pred_premier = fun p ->\n",
" si (gauche p)\n",
" (paire faux premier)\n",
" (paire faux (suivant (droite p)))\n",
" in\n",
" let paire_finale = n pred_suivant pred_premier in\n",
" droite paire_finale\n",
";;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Malheureusement, ce n'est pas bien typé."
]
},
{
"cell_type": "code",
"execution_count": 79,
"metadata": {},
"outputs": [
{
"ename": "error",
"evalue": "compile_error",
"output_type": "error",
"traceback": [
"\u001b[32mFile \"[79]\", line 1, characters 18-22:\n\u001b[31mError: This expression has type\n ((('a -> 'b -> 'a) -> 'c -> 'd) -> ('a -> 'b -> 'a) -> 'c -> 'd) ->\n (('a -> 'b -> 'a) -> 'c -> 'd) -> ('a -> 'b -> 'a) -> 'c -> 'd\n but an expression was expected of type\n ((('a -> 'b -> 'a) -> 'c -> 'd) -> 'd) ->\n ((('e -> 'e -> 'e) ->\n ((('f -> 'g -> 'g) -> 'c -> 'h) -> 'h) ->\n ((('i -> 'j -> 'j) -> 'k -> 'l) -> 'l) -> 'm) ->\n 'm) ->\n ('n -> 'o -> 'o) -> 'p\n The type variable 'd occurs inside ('a -> 'b -> 'a) -> 'c -> 'd\n\u001b[36m 1: \u001b[30mentierNatif (pred \u001b[4mdeux\u001b[0m\u001b[30m);; (* 1 *)\u001b[0m\n"
]
}
],
"source": [
"entierNatif (pred deux);; (* 1 *)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Listes\n",
"\n",
"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) :\n",
"\n",
" estvide (listevide) == vrai\n",
" estvide (cons tt qu) == faux\n",
" \n",
" tete (cons tt qu) == tt\n",
" queue (cons tt qu) == qu\n",
"\n",
"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."
]
},
{
"cell_type": "code",
"execution_count": 58,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[58]\", line 1, characters 28-38:\n",
"Warning 27: unused variable surpasvide.\n"
]
},
{
"data": {
"text/plain": [
"val listevide : 'a -> 'b -> 'a = \n"
]
},
"execution_count": 58,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let listevide = fun survide surpasvide -> survide;;"
]
},
{
"cell_type": "code",
"execution_count": 59,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val cons : 'a -> 'b -> 'c -> ('a -> 'b -> 'd) -> 'd = \n"
]
},
"execution_count": 59,
"metadata": {},
"output_type": "execute_result"
},
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[59]\", line 1, characters 28-35:\n",
"Warning 27: unused variable survide.\n"
]
}
],
"source": [
"let cons = fun hd tl -> fun survide surpasvide -> surpasvide hd tl;;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Avec cette construction, `estvide` est assez simple : `survide` est `() -> vrai` et `surpasvide` est `tt qu -> faux`."
]
},
{
"cell_type": "code",
"execution_count": 60,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[60]\", line 1, characters 45-47:\n",
"Warning 27: unused variable tt.\n",
"File \"[60]\", line 1, characters 48-50:\n",
"Warning 27: unused variable qu.\n"
]
},
{
"data": {
"text/plain": [
"val estvide : (('a -> 'b -> 'a) -> ('c -> 'd -> 'e -> 'f -> 'f) -> 'g) -> 'g =\n",
" \n"
]
},
"execution_count": 60,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let estvide = fun liste -> liste (vrai) (fun tt qu -> faux);;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Deux tests :"
]
},
{
"cell_type": "code",
"execution_count": 61,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 1\n"
]
},
"execution_count": 61,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"- : int = 0\n"
]
},
"execution_count": 61,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif (si (estvide (listevide)) un zero);; (* estvide listevide == vrai *)\n",
"entierNatif (si (estvide (cons un listevide)) un zero);; (* estvide (cons un listevide) == faux *)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Et pour les deux extracteurs, c'est très facile avec cet encodage."
]
},
{
"cell_type": "code",
"execution_count": 62,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[62]\", line 1, characters 45-47:\n",
"Warning 27: unused variable qu.\n"
]
},
{
"data": {
"text/plain": [
"val tete : (('a -> 'a) -> ('b -> 'c -> 'b) -> 'd) -> 'd = \n"
]
},
"execution_count": 62,
"metadata": {},
"output_type": "execute_result"
},
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[62]\", line 2, characters 43-45:\n",
"Warning 27: unused variable tt.\n"
]
},
{
"data": {
"text/plain": [
"val queue : (('a -> 'a) -> ('b -> 'c -> 'c) -> 'd) -> 'd = \n"
]
},
"execution_count": 62,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let tete = fun liste -> liste (vide) (fun tt qu -> tt);;\n",
"let queue = fun liste -> liste (vide) (fun tt qu -> qu);;"
]
},
{
"cell_type": "code",
"execution_count": 69,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : int = 1\n"
]
},
"execution_count": 69,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"- : int = 1\n"
]
},
"execution_count": 69,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"- : int = 2\n"
]
},
"execution_count": 69,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entierNatif (tete (cons un listevide));;\n",
"entierNatif (tete (queue (cons deux (cons un listevide))));;\n",
"entierNatif (tete (queue (cons trois (cons deux (cons un listevide)))));;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Visualisons les types que Caml trouve a des listes de tailles croissantes :"
]
},
{
"cell_type": "code",
"execution_count": 70,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : '_a ->\n",
" ((('_b -> '_b) -> '_b -> '_b) ->\n",
" ('_c ->\n",
" ((('_d -> '_d) -> '_d -> '_d) -> ('_e -> '_f -> '_e) -> '_g) -> '_g) ->\n",
" '_h) ->\n",
" '_h\n",
"= \n"
]
},
"execution_count": 70,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"cons un (cons un listevide);; (* 8 variables pour une liste de taille 2 *)"
]
},
{
"cell_type": "code",
"execution_count": 71,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : '_a ->\n",
" ((('_b -> '_b) -> '_b -> '_b) ->\n",
" ('_c ->\n",
" ((('_d -> '_d) -> '_d -> '_d) ->\n",
" ('_e ->\n",
" ((('_f -> '_f) -> '_f -> '_f) ->\n",
" ('_g ->\n",
" ((('_h -> '_h) -> '_h -> '_h) -> ('_i -> '_j -> '_i) -> '_k) -> '_k) ->\n",
" '_l) ->\n",
" '_l) ->\n",
" '_m) ->\n",
" '_m) ->\n",
" '_n) ->\n",
" '_n\n",
"= \n"
]
},
"execution_count": 71,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"cons un (cons un (cons un (cons un listevide)));; (* 14 variables pour une liste de taille 4 *)"
]
},
{
"cell_type": "code",
"execution_count": 72,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"- : '_a ->\n",
" ((('_b -> '_b) -> '_b -> '_b) ->\n",
" ('_c ->\n",
" ((('_d -> '_d) -> '_d -> '_d) ->\n",
" ('_e ->\n",
" ((('_f -> '_f) -> '_f -> '_f) ->\n",
" ('_g ->\n",
" ((('_h -> '_h) -> '_h -> '_h) ->\n",
" ('_i ->\n",
" ((('_j -> '_j) -> '_j -> '_j) ->\n",
" ('_k ->\n",
" ((('_l -> '_l) -> '_l -> '_l) ->\n",
" ('_m ->\n",
" ((('_n -> '_n) -> '_n -> '_n) ->\n",
" ('_o ->\n",
" ((('_p -> '_p) -> '_p -> '_p) -> ('_q -> '_r -> '_q) -> '_s) ->\n",
" '_s) ->\n",
" '_t) ->\n",
" '_t) ->\n",
" '_u) ->\n",
" '_u) ->\n",
" '_v) ->\n",
" '_v) ->\n",
" '_w) ->\n",
" '_w) ->\n",
" '_x) ->\n",
" '_x) ->\n",
" '_y) ->\n",
" '_y) ->\n",
" '_z) ->\n",
" '_z\n",
"= \n"
]
},
"execution_count": 72,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"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 *)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"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$ !\n",
"\n",
"Aucun espoir donc (avec cet encodage) d'avoir un type générique pour les listes représentés en Caml.\n",
"\n",
"Et donc nous ne sommes pas surpris de voir cet essai échouer :"
]
},
{
"cell_type": "code",
"execution_count": 68,
"metadata": {},
"outputs": [
{
"ename": "error",
"evalue": "compile_error",
"output_type": "error",
"traceback": [
"\u001b[32mFile \"[68]\", line 2, characters 44-45:\n\u001b[31mError: This expression has type 'a but an expression was expected of type\n (('b -> 'b) -> 'b -> 'b) -> ('c -> 'a -> 'd) -> 'e\n The type variable 'a occurs inside\n (('b -> 'b) -> 'b -> 'b) -> ('c -> 'a -> 'd) -> 'e\n\u001b[36m 1: \u001b[30mlet rec longueur liste =\n\u001b[36m 2: \u001b[30m liste (zero) (fun t q -> succ (longueur \u001b[4mq\u001b[0m\u001b[30m))\n\u001b[36m 3: \u001b[30m;;\u001b[0m\n"
]
}
],
"source": [
"let rec longueur liste =\n",
" liste (zero) (fun t q -> succ (longueur q))\n",
";;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"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`..."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On peut essayer de faire une fonction `ieme`.\n",
"On veut que `ieme zero liste = tete` et `ieme n liste = ieme (pred n) (queue liste)`.\n",
"\n",
"En écrivant en haut niveau, on aimerait pouvoir faire :"
]
},
{
"cell_type": "code",
"execution_count": 87,
"metadata": {},
"outputs": [
{
"ename": "error",
"evalue": "compile_error",
"output_type": "error",
"traceback": [
"\u001b[32mFile \"[87]\", line 2, characters 42-47:\n\u001b[31mError: This expression has type\n ('a -> 'b -> 'a) ->\n ('c -> 'd -> 'e -> 'f -> 'f) -> ('g -> 'h -> 'g) -> 'i -> 'j\n but an expression was expected of type\n ('a -> 'a) -> ('k -> 'l -> 'l) -> 'm\n The type variable 'a occurs inside 'b -> 'a\n\u001b[36m 1: \u001b[30mlet pop liste =\n\u001b[36m 2: \u001b[30m si (estvide liste) (listevide) (queue \u001b[4mliste\u001b[0m\u001b[30m)\n\u001b[36m 3: \u001b[30m;;\u001b[0m\n"
]
}
],
"source": [
"let pop liste =\n",
" si (estvide liste) (listevide) (queue liste)\n",
";;"
]
},
{
"cell_type": "code",
"execution_count": 86,
"metadata": {},
"outputs": [
{
"ename": "error",
"evalue": "compile_error",
"output_type": "error",
"traceback": [
"\u001b[32mFile \"[86]\", line 2, characters 12-15:\n\u001b[31mError: Unbound value pop\n\u001b[36m 1: \u001b[30mlet ieme n liste =\n\u001b[36m 2: \u001b[30m tete (n \u001b[4mpop\u001b[0m\u001b[30m liste)\n\u001b[36m 3: \u001b[30m;;\u001b[0m\n"
]
}
],
"source": [
"let ieme n liste =\n",
" tete (n pop liste)\n",
";;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## La fonction U\n",
"\n",
"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.\n",
"\n",
"Mais ce sera la faiblesse de l'utilisation de Caml : ce terme ne peut être correctement typé !"
]
},
{
"cell_type": "code",
"execution_count": 55,
"metadata": {},
"outputs": [
{
"ename": "error",
"evalue": "compile_error",
"output_type": "error",
"traceback": [
"\u001b[32mFile \"[55]\", line 1, characters 19-22:\n\u001b[31mError: This expression has type 'a -> 'b\n but an expression was expected of type 'a\n The type variable 'a occurs inside 'a -> 'b\n\u001b[36m 1: \u001b[30mlet u = fun f -> f \u001b[4m(f)\u001b[0m\u001b[30m;;\u001b[0m\n"
]
}
],
"source": [
"let u = fun f -> f (f);;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"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."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## La récursion via la fonction Y\n",
"\n",
"La fonction $Y$ trouve le point fixe d'une autre fonction.\n",
"C'est très utile pour définir des fonctions par récurrence.\n",
"\n",
"Par exemple, la factorielle est le point fixe de la fonction suivante :\n",
"\"$\\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).\n",
"\n",
"$Y$ satisfait ces contraintes : $Y(F) = f$ et $f = F(f)$.\n",
"Donc $Y(F) = F(Y(F))$ et donc $Y = \\lambda F. F(Y(F))$. Mais ce premier essai ne marche pas."
]
},
{
"cell_type": "code",
"execution_count": 56,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val y : ('a -> 'a) -> 'a = \n"
]
},
"execution_count": 56,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec y = fun f -> f (y(f));;"
]
},
{
"cell_type": "code",
"execution_count": 57,
"metadata": {},
"outputs": [
{
"ename": "error",
"evalue": "compile_error",
"output_type": "error",
"traceback": [
"\u001b[32mFile \"[57]\", line 1, characters 63-64:\n\u001b[31mError: This expression has type\n ((('a -> 'b -> 'a) -> 'c -> 'd -> 'e -> 'e) -> 'd -> 'e -> 'e) ->\n ((('f -> 'f -> 'f) ->\n ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n) ->\n 'o ->\n ('f -> 'f -> 'f) ->\n ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n) ->\n (('p -> 'p) -> 'p -> 'p) -> 'q -> 'r\n but an expression was expected of type\n ((('a -> 'b -> 'a) -> 'c -> 'd -> 'e -> 'e) -> 'd -> 'e -> 'e) ->\n ((('f -> 'f -> 'f) ->\n ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n) ->\n 'n) ->\n ('s -> 't -> 't) -> 'u\n The type variable 'n occurs inside\n 'o ->\n ('f -> 'f -> 'f) ->\n ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n\n\u001b[36m 1: \u001b[30mlet fact = y(fun f n -> si (estnul n) (un) (produit n (f (pred \u001b[4mn\u001b[0m\u001b[30m))));;\u001b[0m\n"
]
}
],
"source": [
"let fact = y(fun f n -> si (estnul n) (un) (produit n (f (pred n))));;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On utilise la $\\eta$-expansion : si $e$ termine, $e$ est équivalent (ie tout calcul donne le même terme) à $\\lambda x. e(x)$."
]
},
{
"cell_type": "code",
"execution_count": 58,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val y : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = \n"
]
},
"execution_count": 58,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec y = fun f -> f (fun x -> y(f)(x));;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Par contre, le typage n'arrive toujours pas à trouver que l'expression suivante devrait être bien définie :"
]
},
{
"cell_type": "code",
"execution_count": 59,
"metadata": {},
"outputs": [
{
"ename": "error",
"evalue": "compile_error",
"output_type": "error",
"traceback": [
"\u001b[32mFile \"[59]\", line 1, characters 63-64:\n\u001b[31mError: This expression has type\n ((('a -> 'b -> 'a) -> 'c -> 'd -> 'e -> 'e) -> 'd -> 'e -> 'e) ->\n ((('f -> 'f -> 'f) ->\n ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n) ->\n 'o ->\n ('f -> 'f -> 'f) ->\n ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n) ->\n (('p -> 'p) -> 'p -> 'p) -> 'q -> 'r\n but an expression was expected of type\n ((('a -> 'b -> 'a) -> 'c -> 'd -> 'e -> 'e) -> 'd -> 'e -> 'e) ->\n ((('f -> 'f -> 'f) ->\n ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n) ->\n 'n) ->\n ('s -> 't -> 't) -> 'u\n The type variable 'n occurs inside\n 'o ->\n ('f -> 'f -> 'f) ->\n ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n\n\u001b[36m 1: \u001b[30mlet fact = y(fun f n -> si (estnul n) (un) (produit n (f (pred \u001b[4mn\u001b[0m\u001b[30m))));;\u001b[0m\n"
]
}
],
"source": [
"let fact = y(fun f n -> si (estnul n) (un) (produit n (f (pred n))));;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Conclusion\n",
"\n",
"Je n'ai pas réussi à traduire intégralement la prouesse initiale, écrite en Python, par Matt Might.\n",
"Dommage, le typage de Caml est trop strict pour cet exercice."
]
}
],
"metadata": {
"kernelspec": {
"display_name": "OCaml 4.04.2",
"language": "OCaml",
"name": "ocaml-jupyter"
},
"language_info": {
"codemirror_mode": "text/x-ocaml",
"file_extension": ".ml",
"mimetype": "text/x-ocaml",
"name": "OCaml",
"nbconverter_exporter": null,
"pygments_lexer": "OCaml",
"version": "4.04.2"
},
"toc": {
"colors": {
"hover_highlight": "#DAA520",
"running_highlight": "#FF0000",
"selected_highlight": "#FFD700"
},
"moveMenuLeft": true,
"nav_menu": {
"height": "364px",
"width": "251px"
},
"navigate_menu": true,
"number_sections": true,
"sideBar": true,
"threshold": 4,
"toc_cell": true,
"toc_section_display": "block",
"toc_window_display": false
},
"varInspector": {
"cols": {
"lenName": 16,
"lenType": 16,
"lenVar": 40
},
"kernels_config": {
"python": {
"delete_cmd_postfix": "",
"delete_cmd_prefix": "del ",
"library": "var_list.py",
"varRefreshCmd": "print(var_dic_list())"
},
"r": {
"delete_cmd_postfix": ") ",
"delete_cmd_prefix": "rm(",
"library": "var_list.r",
"varRefreshCmd": "cat(var_dic_list()) "
}
},
"types_to_exclude": [
"module",
"function",
"builtin_function_or_method",
"instance",
"_Feature"
],
"window_display": false
}
},
"nbformat": 4,
"nbformat_minor": 2
}