ericw
/
Lambda_Calcul
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Lambda_Calcul/lambda_calcul.ipynb

6466 lines
215 KiB
Plaintext
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Ce calepin est composé de deux parties :\n",
"\n",
"1. la première partie est une rapide présentation du $\\lambda$-calcul illustrée par l'utilisation d'un module permettant de définir et transformer des $\\lambda$-termes. \n",
" \n",
"2. la deuxième partie reprend la partie « pouvoir d'expression du $\\lambda$-calcul » en l'illustrant avec les lambda-expressions du langage Python. (CETTE PARTIE RESTE ENCORE A REDIGER)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# $\\lambda$-calcul"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le [$\\lambda$-calcul](https://fr.wikipedia.org/wiki/Lambda-calcul) a été introduit dans les années 1930, principalement par [Alonzo Church](https://fr.wikipedia.org/wiki/Alonzo_Church) pour des questions de fondements mathématiques, semblables à celles qui ont conduit, à la même époque, [Alan Turing](https://fr.wikipedia.org/wiki/Alan_Turing) à concevoir les [machines](https://fr.wikipedia.org/wiki/Machine_de_Turing) qui portent son nom maintenant.\n",
"\n",
"Avec les machines de Turing, le $\\lambda$-calcul est l'un des principaux outils permettant d'étudier l'informatique théorique. Il est en particulier le fondement de la programmation fonctionnelle, et des langages de programmation comme [Lisp](https://fr.wikipedia.org/wiki/Lisp), [Scheme](https://fr.wikipedia.org/wiki/Scheme), [ML](https://fr.wikipedia.org/wiki/ML_(langage)), [Haskell](https://fr.wikipedia.org/wiki/Haskell) lui doivent beaucoup."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Les $\\lambda$-termes"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Sommaire de cette partie :\n",
"\n",
"* définition des $\\lambda$-termes\n",
"* variables libres, liées. Sous-termes\n",
"\n",
"Le tout illustré avec une classe Python pour représenter et manipuler des $\\lambda$-termes."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Définition des $\\lambda$-termes"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"En principe, les $\\lambda$-termes sont des mots sur lesquels certaines opérations sont possibles. Ces mots ont vocation à pouvoir exprimer des fonctions, ainsi que leur application à un argument. "
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"En $\\lambda$-calcul tout est fonction !\n",
"\n",
"Si $f$ est un $\\lambda$-terme, on doit pouvoir l'appliquer à un autre terme $x$, mais au lieu d'écrire $f(x)$ comme c'est l'usage en mathématiques, on écrit plutôt $(f\\ x)$ et cela forme un nouveau terme nommé *application*.\n",
"\n",
"Il n'y a pas de fonctions à plusieurs variables : toutes les fonctions ont une et une seule variable. Donc si on a en tête de vouloir représenter une fonction à deux variables $f(x,y)$, elle le sera par une fonction à une variable telle que $f(x)$ soit elle aussi une fonction à une variable, et au lieu d'écrire $f(x,y)$ ou même $f(x)(y)$, on écrira $((f\\ x)\\ y)$.\n",
"\n",
"Enfin si $x$ est une variable et $M$ un terme dépendant éventuellement de $x$, on doit pouvoir définir la fonction $x\\mapsto M$. Cette construction est nommée *abstraction* en $\\lambda$-calcul et elle est notée $\\lambda x.M$."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Formellement, l'alphabet $\\Sigma$ utilisé pour les $\\lambda$-termes est constitué :\n",
"\n",
"* d'un ensemble infini dénombrable de variables $V=\\{x, y, z, t, ...\\}$ ;\n",
"* et d'un ensemble de cinq symboles $\\mathcal{S}=\\{\\lambda, ., (, ), ESP\\}$, $ESP$ désignant l'espace.\n",
"Ainsi $\\Sigma = V\\cup \\mathcal{S}$.\n",
"\n",
"Les $\\lambda$-termes sont construits inductivement à l'aide des trois règles\n",
"\n",
"1. toute variable est un $\\lambda$-terme ;\n",
"2. si $T$ est un $\\lambda$-terme et $x$ une variable, alors $\\lambda x.T$ est un $\\lambda$-terme, que l'on appelle *abstraction* de $T$ par $x$ ;\n",
"3. si $T$ et $S$ sont deux $\\lambda$-termes, alors $(T\\ S)$ est un $\\lambda$-terme, que l'on appelle *application* de $T$ à $S$.\n",
"\n",
"L'ensemble $\\Lambda$ des $\\lambda$-termes est donc le plus petit sous-ensemble de $\\Sigma^*$ contenant $V$ et stable par abstraction et application."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Une classe pour les $\\lambda$-termes"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le module `lambda_calcul` définit une classe `Lambda_terme` permettant de construire et manipuler des objets représentant des $\\lambda$-termes."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Remarque :** ce module fait appel au module`sly` qui permet de définir des analyseurs lexicaux et syntaxiques. Ce module doit donc être préalablement installé (`pip install sly`)."
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"from lambda_calcul import Lambda_terme"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Construction de $\\lambda$-termes"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"L'une des façons les plus simples de construire des $\\lambda$-termes est d'invoquer le constructeur `Lambda_terme` avec une chaîne de caractères les représentant. "
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [],
"source": [
"T1 = Lambda_terme(\"x\")\n",
"T2 = Lambda_terme(\"(x x)\")\n",
"T3 = Lambda_terme(\"!x.x\")\n",
"T4 = Lambda_terme('!x.(x y)')\n",
"T5 = Lambda_terme('(!x.(x y) x)')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Les objets de la classe `Lambda_terme` peuvent être convertis en chaînes de caractères et imprimés."
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"x\n",
"(x x)\n",
"λx.x\n",
"λx.(x y)\n",
"(λx.(x y) x)\n"
]
}
],
"source": [
"termes = (T1, T2, T3, T4, T5)\n",
"for t in termes:\n",
" print(t)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"La syntaxe autorisée pour les $\\lambda$-termes est\n",
"\n",
"1. pour les variables : n'importe quelles chaîne de caractères ne contenant que des lettres (latins) non accentuées majuscules ou minuscules, ainsi que des chiffres. Autrement dit n'importe quelle chaîne correspondant à l'expression régulière `[A-Za-z][A-Za-z0-9]*`.\n",
"2. pour les abstractions : n'importe quelle chaîne débutant par `!` ou $\\lambda$ suivie d'une variable, suivie d'un point `.` suivi d'une chaîne décrivant un $\\lambda$-terme. Autrement dit n'importe quelle chaîne satisfaisant `(!|λ)VAR.LAMBDA-TERME`.\n",
"3. pour les applications : n'importe quelle chaîne débutant par une parenthèse ouvrante `(` et terminant par une parenthèse fermante `)` et comprenant entre les deux la description de deux $\\lambda$-termes séparés par un ou plusieurs espaces. Autrement dit n'importe quelle chaîne satisfaisant `(LAMBDA-TERME ESPACES LAMBDA-TERME)`.\n",
"\n",
"**Remarque :** le parenthésage des applications est obligatoire, contrairement à la convention d'associativité à gauche qui permet usuellement d'écrire $M\\ N\\ P$ au lieu de $((M\\ N)\\ P)$.\n",
"De même deux abstractions successives doivent être explicitement écrites : il n'est pas possible d'écrire $\\lambda xy.(x\\ y)$, il faut écrire $\\lambda x.\\lambda y.(x\\ y)$."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Les passages à la ligne sont autorisés dans la chaîne transmise au constructeur."
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(james bond007)\n"
]
}
],
"source": [
"print(Lambda_terme('''(james\n",
" bond007)'''))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"L'exception `LambdaSyntaxError` est déclenchée en cas de présence de caractères non autorisés ou de malformation syntaxique."
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [],
"source": [
"# Lambda_terme('bond 007')"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [],
"source": [
"# Lambda_terme('(james bond007 !)')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Autres constructions"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Deux méthodes permettent de construire de nouveaux $\\lambda$-termes à partir de $\\lambda$-termes existant."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"La méthode `abstrait` permet de construire une abstraction."
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λx.x\n",
"λy.(x x)\n"
]
}
],
"source": [
"print(T1.abstrait('x'))\n",
"print(T2.abstrait('y'))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"La méthode `applique` construit une application d'un terme sur un autre."
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((x x) λx.x)\n",
"(λx.x (x x))\n"
]
}
],
"source": [
"print(T2.applique(T3))\n",
"print(T3.applique(T2))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Quelques prédicats"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Trois prédicats `est_variable`, `est_abstraction` et `est_application` permettent de reconnaître la nature d'un $\\lambda$-terme."
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"x\n",
"(x x)\n",
"λx.x\n",
"λx.(x y)\n",
"(λx.(x y) x)\n"
]
}
],
"source": [
"# pour rappel des termes définis\n",
"for t in termes:\n",
" print(t)"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, False, False, False, False)"
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(t.est_variable() for t in termes)"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(False, False, True, True, False)"
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(t.est_abstraction() for t in termes)"
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(False, True, False, False, True)"
]
},
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(t.est_application() for t in termes)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Variables libres, variables liées"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Parmi les variables figurant dans un $\\lambda$-terme, certaines sont dites *libres*, et d'autres *liées*."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Les variables libres sont celles qui ne sont pas sous la portée d'une abstraction. L'ensemble $FV(T)$ des variables libres d'un $\\lambda$-terme $T$ est défini inductivement par les trois règles :\n",
"\n",
"1. $FV(x) = \\{x\\}$.\n",
"2. $FV(\\lambda x.T) = FV(T)\\setminus\\{x\\}$.\n",
"3. $FV((T_1\\ T_2)) = FV(T_1)\\cup FV(T_2)$.\n",
"\n",
"Les variables liées sont celles qui sont sous la portée d'une abstraction. L'ensemble $BV(T)$ des variables liées d'un $\\lambda$-terme $T$ est défini inductivement par les trois règles :\n",
"\n",
"1. $BV(x) = \\emptyset$.\n",
"2. $BV(\\lambda x.T) = BV(T)\\cup \\{x\\}$ si $x\\in FV(T)$, sinon\n",
" $BV(\\lambda x.T) = BV(T)$.\n",
"3. $BV((T_1\\ T_2)) = BV(T_1)\\cup BV(T_2)$."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"La méthode `variables` donne sous un couple constitué de l'ensemble des variables libres et de l'ensemble des variables liées du $\\lambda$-terme."
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(({'x'}, set()),\n",
" ({'x'}, set()),\n",
" (set(), {'x'}),\n",
" ({'y'}, {'x'}),\n",
" ({'x', 'y'}, {'x'}))"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(t.variables() for t in termes)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Remarque :** Dans un $\\lambda$-terme, une variable peut être à la fois libre et liée comme le montre l'exemple du terme `T5` qui contient deux occurrences de la variable $x$, la première étant liée et la seconde libre. Pour être plus précis, on devrait plutôt parler d'*occurrence libre* ou *liée* d'une variable."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Un $\\lambda$-terme sans variable libre est appelé *terme clos*, ou encore *combinateur*."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Sous-termes"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Hormis les variables, les $\\lambda$-termes sont construits à partir d'autres $\\lambda$-termes qui eux-mêmes peuvent être construits à l'aide d'autres $\\lambda$-termes encore. \n",
"\n",
"Un $\\lambda$-terme contient donc des *sous-termes*."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Voici comment l'ensemble $ST$ des sous-termes d'un $\\lambda$-terme est défini inductivement selon la structure de ce terme.\n",
"\n",
"1. Les variables n'ont qu'un seul sous-terme : elles-mêmes. $ST(x) = \\{x\\}$.\n",
"2. Les sous-termes d'une abstraction sont, outre l'abstration elle-même, les sous-termes de son corps. $ST(\\lambda x.T) = \\{\\lambda x.T\\}\\cup ST(T)$.\n",
"3. Les sous-termes d'une application sont, outre l'application elle-même, les sous-termes des deux termes la composant. $ST((T_1\\ T_2)) = \\{(T_1\\ T_2)\\}\\cup ST(T_1)\\cup ST(T_2)$."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"La méthode `sous_termes` donne la liste des sous-termes d'un $\\lambda$-terme. L'ordre dans lequel figurent les sous-termes dans cette liste est l'ordre d'apparition de ces sous-termes dans une lecture de gauche à droite (autrement dit, un ordre préfixe)."
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λx.(x y) x)\n",
"λx.(x y)\n",
"(x y)\n",
"x\n",
"y\n",
"x\n"
]
}
],
"source": [
"for t in T5.sous_termes():\n",
" print(t)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## $\\beta$-réduction ou calculer avec des $\\lambda$-termes"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Substitution"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Étant donnés deux $\\lambda$-termes $T$ et $R$, et une variable $x$, on note $T[x:= R]$ le $\\lambda$-terme obtenu en substituant le terme $R$ à toutes les occurrences libres de la variable $x$ dans le terme $T$."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"1. Si $T$ est une variable, $T[x:=R] = R$ si $T=x$ et $T[x := R] = T$ si $T\\neq x$.\n",
"2. Si $T=(T_1\\ T_2)$ est une application, $T[x:=R] = (T_1[x:=R]\\ T_2[x := R])$.\n",
"3. Si $T=\\lambda y.S$ est une abstraction, alors il faut distinguer deux cas pour définir $T[x:=R]$\n",
" \n",
" * si $y\\not\\in FV(R)$, alors $T[x:=R] = \\lambda y.S[x:= R]$.\n",
" * si $y\\in FV(R)$, alors $T[x:=R] = \\lambda z.S[y:=z][x:=R]$, la variable $z$ étant une nouvelle variable n'apparaissant pas dans $S$ ni dans $R$. On procède à un renommage de la variable d'abstraction ($y$) pour éviter que les occurrences libres de $y$ de $R$ n'entrent sous la portée de l'abstraction.\n",
"\n",
"\n",
"La méthode `subs` renvoie le terme obtenu en substituant un $\\lambda$-terme à toutes les occurrences libres d'une variable."
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"T1 = x\n",
"T1[y:=(y x)] = x\n",
"T1[x:=(y x)] = (y x)\n"
]
}
],
"source": [
"# substitution dans une variable\n",
"print('T1 = {:s}'.format(str(T1)))\n",
"x = 'y'; R = Lambda_terme('(y x)')\n",
"print('T1[{:s}:={:s}] = {:s}'.format(x, str(R), str(T1.subs(x, R))))\n",
"x = 'x'\n",
"print('T1[{:s}:={:s}] = {:s}'.format(x, str(R), str(T1.subs(x, R))))"
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"T2 = (x x)\n",
"T2[y:=(y x)] = (x x)\n",
"T2[x:=(y x)] = ((y x) (y x))\n"
]
}
],
"source": [
"# substitution dans une application\n",
"print('T2 = {:s}'.format(str(T2)))\n",
"x = 'y'; R = Lambda_terme('(y x)')\n",
"print('T2[{:s}:={:s}] = {:s}'.format(x, str(R), str(T2.subs(x, R))))\n",
"x = 'x'\n",
"print('T2[{:s}:={:s}] = {:s}'.format(x, str(R), str(T2.subs(x, R))))"
]
},
{
"cell_type": "code",
"execution_count": 17,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"T4 = λx.(x y)\n",
"T4[x:=(y z)] = λx.(x y)\n",
"T4[y:=(y z)] = λx.(x (y z))\n",
"T4[y:=(y x)] = λx0.(x0 (y x))\n"
]
}
],
"source": [
"# substitution dans une abstraction\n",
"print('T4 = {:s}'.format(str(T4)))\n",
"x = 'x'; R = Lambda_terme('(y z)')\n",
"print('T4[{:s}:={:s}] = {:s}'.format(x, str(R), str(T4.subs(x, R))))\n",
"x = 'y'; R = Lambda_terme('(y z)')\n",
"print('T4[{:s}:={:s}] = {:s}'.format(x, str(R), str(T4.subs(x, R))))\n",
"x = 'y'; R = Lambda_terme('(y x)')\n",
"print('T4[{:s}:={:s}] = {:s}'.format(x, str(R), str(T4.subs(x, R))))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Remarque :** on peut utiliser la substitution pour construire des $\\lambda$-termes à partir d'autres existants. "
]
},
{
"cell_type": "code",
"execution_count": 18,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λz.((x x) λx.x) λx.(x y))\n"
]
}
],
"source": [
"print(Lambda_terme('(!z.(T2 T3) T4)').subs('T2', T2).subs('T3', T3).subs('T4', T4))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Réduire un terme"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"L'idée principale qui motive la notion de réduction est qu'une abstraction $\\lambda x.T$ représente une fonction $x \\mapsto T$, et qu'une application d'une abstraction à un terme $R$, $(\\lambda x.T\\ R)$ représente l'application de la fonction au terme $R$.\n",
"\n",
"De la même façon que l'application la fonction $x\\mapsto x^2+2x -1$ à un nombre $y$ se ramène au calcul de l'expression $y^2+2y-1$ obtenue en substituant $y$ à $x$, l'application $(\\lambda x.T\\ R)$ doit se réduire au terme $T[x:=R]$."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Un terme de la forme $(\\lambda x.T\\ R)$, autrement dit une application d'une abstraction à un terme, est appelé *redex*.\n",
"\n",
"La *réduction d'un redex* est une relation, notée $\\rightarrow_\\beta$, est définie par\n",
"\n",
"$$ (\\lambda x.T\\ R) \\rightarrow_\\beta T[x:=R].$$ \n",
"\n",
"On peut étendre cette notion de réduction à tout $\\lambda$-terme dont l'un au moins de ses sous-termes est un redex. Le terme réduit correspondant étant celui obtenu en remplaçant un sous-terme redex par son réduit.\n",
"\n",
"Selon cette définition, seuls les $\\lambda$-termes ayant au moins un redex parmi leurs sous-termes peuvent être réduits. Les $\\lambda$-termes ne contenant aucun redex sont dit *irréductibles* ou encore sont des *formes normales*."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"La méthode `est_redex` permet de distinguer les $\\lambda$-termes qui sont des redex."
]
},
{
"cell_type": "code",
"execution_count": 19,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"x False\n",
"(x x) False\n",
"λx.x False\n",
"λx.(x y) False\n",
"(λx.(x y) x) True\n"
]
}
],
"source": [
"for t in termes:\n",
" print(t, t.est_redex())"
]
},
{
"cell_type": "code",
"execution_count": 20,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λx.(x y) (λx.(x y) x)) True\n",
"λx.(x y) False\n",
"(x y) False\n",
"x False\n",
"y False\n",
"(λx.(x y) x) True\n",
"λx.(x y) False\n",
"(x y) False\n",
"x False\n",
"y False\n",
"x False\n"
]
}
],
"source": [
"T6 = T4.applique(T5)\n",
"for t in T6.sous_termes():\n",
" print(t, t.est_redex())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"La méthode `reduit` réduit les redex. La valeur de l'expression `T.reduit()` est un couple (Lambda_terme, bool) dont la valeur dépend du $\\lambda$-terme `T` :\n",
"\n",
"* si `T` contient un redex, alors le booléen a la valeur `True` et la première composante du couple est le $\\lambda$-terme obtenu en remplaçant le redex le plus à gauche dans `T` par le terme obtenu par une étape de réduction.\n",
"* si `T` ne contient aucun redex, alors le couple est `(T, False)`."
]
},
{
"cell_type": "code",
"execution_count": 21,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(x x)\n",
"False\n",
"(x x)\n"
]
}
],
"source": [
"t, reduit = T2.reduit()\n",
"print(T2)\n",
"print(reduit)\n",
"print(t)"
]
},
{
"cell_type": "code",
"execution_count": 22,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λx.(x y) (λx.(x y) x))\n",
"True\n",
"((λx.(x y) x) y)\n"
]
}
],
"source": [
"T7, reduit = T6.reduit()\n",
"print(T6)\n",
"print(reduit)\n",
"print(T7)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le terme `T6` contient deux redex. Comme il a été signalé la méthode `reduit` réduit le redex le plus à gauche, et dans le cas de `T6` le redex le plus à gauche est `T6` lui-même. Et cela donne le terme `T7`.\n",
"\n",
"Mais comme `T6 = (T4 T5)`, et que `T5` est un redex, considérons le terme `(T4 T5')` dans lequel `T5'` est le terme obtenu en réduisant le redex `T5`."
]
},
{
"cell_type": "code",
"execution_count": 23,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λx.(x y) x)\n",
"(λx.(x y) (x y))\n"
]
}
],
"source": [
"T5bis, reduit = T5.reduit()\n",
"T7bis = T4.applique(T5bis)\n",
"print(T5)\n",
"print\n",
"print(T7bis)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Nous voyons donc qu'un $\\lambda$-terme peut se réduire de plusieurs façons (en fait d'autant de façon que le terme contient de sous-termes qui sont des redex).\n",
"\n",
"En particulier nous avons\n",
"\n",
"* `T6` $\\rightarrow_\\beta$ `T7` et\n",
"* `T6` $\\rightarrow_\\beta$ `T7bis`.\n",
"\n",
"Si nous envisageons les $\\beta$ reductions comme des étapes de calcul, nous avons donc deux voies distinctes pour « calculer » `T6`. \n",
"\n",
"Poursuivons le calcul pour chacun des deux termes `T7` et `T7bis` qui ne sont pas des formes normales."
]
},
{
"cell_type": "code",
"execution_count": 24,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((x y) y) = ((x y) y) : True\n"
]
}
],
"source": [
"T8, _ = T7.reduit()\n",
"T8bis, _ = T7bis.reduit()\n",
"print('{} = {} : {}'.format(str(T8), str(T8bis), T8==T8bis))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Après une nouvelle étape de réduction nous obtenons le même terme $((x\\ y)\\ y)$ qui est irréductible.\n",
"On peut dire que par deux calculs différents `T6` se calcule, ou se *normalise*, en $((x\\ y)\\ y)$.\n",
"On écrit\n",
"\n",
"$$ \\mathtt{T6} \\twoheadrightarrow_{\\beta} ((x\\ y)\\ y),$$\n",
"la notation $T\\twoheadrightarrow_{\\beta} R$ signifiant qu'il y a un nombre quelconque (y compris nul) d'étapes de $\\beta$-réduction pour arriver au terme $R$ en partant de $T$ (dit en terme plus savant, la relation $\\twoheadrightarrow_\\beta$ est la clôture réflexive et transitive de la relation $\\rightarrow_\\beta$)."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Formes normales, normalisation"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On dit d'un $\\lambda$-terme $T$ qu'il est *normalisable* s'il existe un $\\lambda$-terme $R$ irréductible tel que\n",
"\n",
"$$ T\\twoheadrightarrow_{\\beta} R.$$\n",
"Dans ce cas, on dit que $R$ est une *forme normale* de $T$.\n",
"\n",
"Par exemple, `T6` est normalisable et admet $((x\\ y)\\ y)$ pour forme normale."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Deux questions se posent naturellement :\n",
"\n",
"1. est-ce que tout $\\lambda$-terme est normalisable ?\n",
"2. un $\\lambda$-terme normalisable peut-il avoir plusieurs formes normales ?"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"La réponse à la première question est négative. Il suffit pour s'en convaincre de considérer le terme\n",
"\n",
"$$\\Omega = (\\lambda x.(x\\ x)\\ \\lambda x.(x\\ x)),$$\n",
"qui est un redex et est donc réductible."
]
},
{
"cell_type": "code",
"execution_count": 25,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λx.(x x) λx.(x x))\n",
"True\n",
"(λx.(x x) λx.(x x)) -> (λx.(x x) λx.(x x))\n",
"True\n"
]
}
],
"source": [
"OMEGA = Lambda_terme('(!x.(x x) !x.(x x))')\n",
"print(OMEGA)\n",
"t, reduit = OMEGA.reduit()\n",
"print(reduit)\n",
"print('{} -> {}'.format(str(OMEGA), str(t)))\n",
"print(t==OMEGA)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le terme $\\Omega$ n'a qu'un seul redex. Il n'y a donc qu'une seule façon de le réduire et cette réduction donne le terme $\\Omega$ lui-même. Quelque soit le nombre d'étapes de réduction qu'on effectue on garde toujours le même terme : $\\Omega$ n'est donc pas normalisable. \n",
"\n",
"Il existe donc des termes non normalisables, et $\\Omega$ en est un exemple les plus simples."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Venons-en maintenant à la deuxième question : un terme normalisable peut-il avoir plusieurs formes normales ?\n",
"\n",
"Cette question est naturelle puisque lorsqu'un $\\lambda$-terme possède plusieurs redex, il y a plusieurs façons de le réduire, et il se pourrait bien que ces voies différentes mènent à des formes normales différentes.\n",
"\n",
"Cela n'a pas été le cas pour le terme `T6`. Et il se trouve que cet exemple particulier reflète la situation générale, car la relation de $\\beta$-réduction satisfait une propriété qu'on appelle propriété du diamant."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Propriété du diamant** Soit $T$ un $\\lambda$-terme qui peut se réduire en un nombre fini d'étapes en deux termes différents $R_1$ et $R_2$. Alors il existe un terme $R$ en lequel chacun des deux termes $R_1$ et $R_2$ se réduit en un nombre quelconque (y compris nul) d'étapes.\n",
"\n",
"Cette propriété doit son nom à la figure qui l'illustre. Cette propriété est aussi connue sous le nom de *confluence* de la $\\beta$-réduction.\n",
"\n",
"![illustration de la propriété du diamant](tikz_diamant.png)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Conséquence de la propriété du diamant :** Un $\\lambda$-terme normalisable ne peut avoir qu'une seule forme normale."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Maintenant que nous avons répondu aux deux questions que nous nous sommes posées, il en vient une troisième.\n",
"\n",
"Étant donné que certains $\\lambda$-termes sont normalisables et d'autres non, y a-t-il un moyen de les reconnaître ?\n",
"\n",
"Si par *moyen* nous entendons un algorithme général prenant un $\\lambda$-terme en entrée, et répondant OUI si ce terme est normalisable et NON dans le cas contraire, alors la réponse est non. Aucun algorithme ne permet de distinguer les termes normalisables de ceux qui ne le sont pas. Le problème de la reconnaissance des termes normalisables est *indécidable*.\n",
"\n",
"Dit en d'autres termes, l'ensemble des termes normalisables n'est pas récursif. En revanche il est récursivement énumérable. En effet, si un terme est normalisable, pour s'en rendre compte il suffit de suivre tous les chemins de réduction. L'un d'eux mène à un terme irréductible et on le trouvera en un nombre fini d'étapes."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"La méthode `forme_normale` calcule la forme normale d'un terme normalisable si ce terme l'est, et ne renvoie rien dans le cas contraire. "
]
},
{
"cell_type": "code",
"execution_count": 26,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((x y) y)\n"
]
}
],
"source": [
"print(T6.forme_normale())"
]
},
{
"cell_type": "code",
"execution_count": 27,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"None\n"
]
}
],
"source": [
"print(OMEGA.forme_normale())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Hmmmm ... Comment est-ce possible puisque nous venons de voir qu'aucun algorithme ne permet de décider si un terme est normalisable ?\n",
"\n",
"En fait le nombre d'étapes de réduction dans le calcul d'une forme normale est limité (par défaut à 100 étapes maximum). On peut visualiser chaque étape de calcul avec le paramètre optionnel `verbose` auquel il faut attribuer la valeur `True`."
]
},
{
"cell_type": "code",
"execution_count": 28,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λx.(x y) (λx.(x y) x))\n",
" 1: ---> ((λx.(x y) x) y)\n",
" 2: ---> ((x y) y)\n",
"Forme normale calculée : ((x y) y)\n"
]
},
{
"data": {
"text/plain": [
"<lambda_calcul.Lambda_terme at 0x7f71cc35f3c8>"
]
},
"execution_count": 28,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"T6.forme_normale(verbose=True)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On voit que la forme normale du terme `T6` est calculé en trois étapes."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Pour un terme non normalisable les calculs peuvent (en principe) être infinis. Voici la tentative de détermination d'une forme normale pour le terme $\\Omega$ limité à dix étapes à l'aide du paramètre optionnel `nb_etapes_max`. "
]
},
{
"cell_type": "code",
"execution_count": 29,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λx.(x x) λx.(x x))\n",
" 1: ---> (λx.(x x) λx.(x x))\n",
" 2: ---> (λx.(x x) λx.(x x))\n",
" 3: ---> (λx.(x x) λx.(x x))\n",
" 4: ---> (λx.(x x) λx.(x x))\n",
" 5: ---> (λx.(x x) λx.(x x))\n",
" 6: ---> (λx.(x x) λx.(x x))\n",
" 7: ---> (λx.(x x) λx.(x x))\n",
" 8: ---> (λx.(x x) λx.(x x))\n",
" 9: ---> (λx.(x x) λx.(x x))\n",
" 10: ---> (λx.(x x) λx.(x x))\n",
"Pas de forme normale atteinte après 10 étapes de réduction\n"
]
}
],
"source": [
"OMEGA.forme_normale(verbose=True, nb_etapes_max=10)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### $\\beta$-équivalence"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"La relation $\\twoheadrightarrow_\\beta$ n'est pas symétrique. En effet, en général, si $T\\twoheadrightarrow_\\beta R$, on n'a pas $R\\twoheadrightarrow_\\beta T$."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"En considèrant que la forme normale d'un terme normalisable représente sa « valeur », on peut définir une relation d'équivalence sur les $\\lambda$-termes normalisables. Cette relation d'équivalence est la clôture symétrique de la relation de réduction $\\twoheadrightarrow_\\beta$."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Deux $\\lambda$-termes $T$ et $S$ (normalisables ou non) sont dit $\\beta$-équivalents, et on note $T=_\\beta S$, s'il existe un terme $R$ tel que $T\\twoheadrightarrow_\\beta R$ et $S\\twoheadrightarrow_\\beta R$."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Ainsi deux termes normalisables ayant la même forme normale sont $\\beta$-équivalents."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Théorème du point fixe** Pour tout $\\lambda$-terme $T$, il existe un $\\lambda$-terme $X$ tel que\n",
"\n",
"$$ (T\\ X) =_\\beta X.$$"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"La démonstration de ce théorème se fait en considérant les $\\lambda$-termes\n",
"$$ W = \\lambda x.(T\\ (x\\ x)),$$\n",
"et\n",
"$$ X = (W\\ W).$$\n",
"Il est clair que\n",
"$$ X \\rightarrow_\\beta (T\\ (W\\ W)) = (T\\ X),$$\n",
"et donc que\n",
"$$ X =_\\beta (T\\ X).$$"
]
},
{
"cell_type": "code",
"execution_count": 30,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λx.(T (x x)) λx.(T (x x)))\n",
"(T (λx.(T (x x)) λx.(T (x x))))\n"
]
}
],
"source": [
"W = Lambda_terme('!x.(T (x x))')\n",
"X = W.applique(W)\n",
"print(X)\n",
"print(X.reduit()[0])"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Remarque** À noter que dans la démonstration du théorème du point fixe, pour établir que $(T\\ X) =_\\beta X$, on a montré que $X$ se réduit en $(T\\ X)$ et non le contraire."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Pouvoir d'expression du $\\lambda$-calcul"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Dans cette section, nous allons découvrir que le $\\lambda$-calcul permet \n",
"\n",
"* de représenter les nombres entiers et de définir les opérations arithmétiques de base\n",
"* de définir des couples, listes, structures à la base de nombreuses autres structures de données\n",
"* de définir des booléens, et de simuler des expressions conditionnelles\n",
"* d'itérer des fonctions,\n",
"* d'exprimer n'importe quelle fonction récursive.\n",
"\n",
"Bref, d'un certain point de vue le $\\lambda$-calcul est un langage de programmation ... certes assez peu efficace comme on pourra s'en rendre compte."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Booléens, opérateurs logiques et conditionnelles"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Les deux booléens VRAI et FAUX"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On peut représenter les deux booléens VRAI et FAUX par les $\\lambda$-termes\n",
"$$ \\mathtt{VRAI} = \\lambda x.\\lambda y.x,$$\n",
"et\n",
"$$ \\mathtt{FAUX} = \\lambda x.\\lambda y.y.$$"
]
},
{
"cell_type": "code",
"execution_count": 31,
"metadata": {},
"outputs": [],
"source": [
"VRAI = Lambda_terme('!x.!y.x')\n",
"FAUX = Lambda_terme('!x.!y.y')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Remarque** les deux termes $\\mathtt{VRAI}$ et $\\mathtt{FAUX}$ sont termes clos irréductibles."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Le terme IF"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Ce choix peut être justifiée a posteriori en considérant que l'expression conditionnelle fréquente en programmation\n",
"\n",
" IF c THEN a ELSE s\n",
"\n",
"peut être facilement simulée à l'aide d'abstractions des variables $c$, $a$ et $s$ par le $\\lambda$-terme\n",
"\n",
"$$ \\mathtt{IF} = \\lambda c.\\lambda a.\\lambda s.((c\\ a)\\ s).$$"
]
},
{
"cell_type": "code",
"execution_count": 32,
"metadata": {},
"outputs": [],
"source": [
"IF = Lambda_terme('!c.!a.!s.((c a) s)') "
]
},
{
"cell_type": "code",
"execution_count": 33,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(((λc.λa.λs.((c a) s) λx.λy.x) ALORS) SINON)\n",
" 1: ---> ((λa.λs.((λx.λy.x a) s) ALORS) SINON)\n",
" 2: ---> (λs.((λx.λy.x ALORS) s) SINON)\n",
" 3: ---> ((λx.λy.x ALORS) SINON)\n",
" 4: ---> (λy.ALORS SINON)\n",
" 5: ---> ALORS\n",
"Forme normale calculée : ALORS\n"
]
},
{
"data": {
"text/plain": [
"<lambda_calcul.Lambda_terme at 0x7f71cc39b320>"
]
},
"execution_count": 33,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"IF.applique(VRAI).applique(Lambda_terme('ALORS')).applique(Lambda_terme('SINON')).forme_normale(verbose=True)"
]
},
{
"cell_type": "code",
"execution_count": 34,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(((λc.λa.λs.((c a) s) λx.λy.y) ALORS) SINON)\n",
" 1: ---> ((λa.λs.((λx.λy.y a) s) ALORS) SINON)\n",
" 2: ---> (λs.((λx.λy.y ALORS) s) SINON)\n",
" 3: ---> ((λx.λy.y ALORS) SINON)\n",
" 4: ---> (λy.y SINON)\n",
" 5: ---> SINON\n",
"Forme normale calculée : SINON\n"
]
},
{
"data": {
"text/plain": [
"<lambda_calcul.Lambda_terme at 0x7f71cc39b978>"
]
},
"execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"IF.applique(FAUX).applique(Lambda_terme('ALORS')).applique(Lambda_terme('SINON')).forme_normale(verbose=True)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Remarque**\n",
"Le $\\lambda$-terme $\\mathtt{IF}$ permet d'exprimer des $\\lambda$-termes ayant une forme normale bien que l'une ou l'autre de ses sous-termes n'en aient pas, comme par exemple\n",
"\n",
"1. $(((\\mathtt{IF}\\, \\mathtt{VRAI})\\, \\mathtt{ALORS})\\, \\mathtt{OMEGA})$ qui se réduit en $\\mathtt{ALORS}$ (et a donc une forme normale si $\\mathtt{ALORS}$ en a une) bien que $\\mathtt{OMEGA}$ n'en ait pas ;\n",
"\n",
"2. ou $(((\\mathtt{IF}\\, \\mathtt{FAUX})\\, \\mathtt{OMEGA})\\, \\mathtt{SINON})$ qui se réduit en $\\mathtt{SINON}$.\n",
"\n",
"Cette propriété est bien utile en programmation, et servira pour la programmation de fonctions récursives."
]
},
{
"cell_type": "code",
"execution_count": 35,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(((λc.λa.λs.((c a) s) λx.λy.x) ALORS) (λx.(x x) λx.(x x)))\n",
" 1: ---> ((λa.λs.((λx.λy.x a) s) ALORS) (λx.(x x) λx.(x x)))\n",
" 2: ---> (λs.((λx.λy.x ALORS) s) (λx.(x x) λx.(x x)))\n",
" 3: ---> ((λx.λy.x ALORS) (λx.(x x) λx.(x x)))\n",
" 4: ---> (λy.ALORS (λx.(x x) λx.(x x)))\n",
" 5: ---> ALORS\n",
"Forme normale calculée : ALORS\n"
]
},
{
"data": {
"text/plain": [
"<lambda_calcul.Lambda_terme at 0x7f71cc39be10>"
]
},
"execution_count": 35,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"IF.applique(VRAI).applique(Lambda_terme('ALORS')).applique(OMEGA).forme_normale(verbose=True)"
]
},
{
"cell_type": "code",
"execution_count": 36,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(((λc.λa.λs.((c a) s) λx.λy.y) (λx.(x x) λx.(x x))) SINON)\n",
" 1: ---> ((λa.λs.((λx.λy.y a) s) (λx.(x x) λx.(x x))) SINON)\n",
" 2: ---> (λs.((λx.λy.y (λx.(x x) λx.(x x))) s) SINON)\n",
" 3: ---> ((λx.λy.y (λx.(x x) λx.(x x))) SINON)\n",
" 4: ---> (λy.y SINON)\n",
" 5: ---> SINON\n",
"Forme normale calculée : SINON\n"
]
},
{
"data": {
"text/plain": [
"<lambda_calcul.Lambda_terme at 0x7f71cc3a1470>"
]
},
"execution_count": 36,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"IF.applique(FAUX).applique(OMEGA).applique(Lambda_terme('SINON')).forme_normale(verbose=True)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le fait que le terme $\\mathtt{IF}$ se comporte bien comme on l'attend résulte du choix de la stratégie de réduction des redex les plus à gauche en priorité. Si la stratégie choisie avait été de réduire le redex le plus à droite, la réduction de chacun des deux termes précédents aurait conduit à la tentative de réduire le terme $\\Omega$ qui échoue puisque celui-ci n'est pas normalisable comme on l'a vu."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Il est facile de définir les opérateurs logiques de base : conjonction, disjonction et négation."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Opérateur ET"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"L'opérateur logique de conjonction peut être défini par\n",
"\n",
"$$ \\mathtt{ET} = \\lambda a.\\lambda b.(((\\mathtt{IF}\\ a)\\ b)\\ \\mathtt{FAUX}).$$"
]
},
{
"cell_type": "code",
"execution_count": 37,
"metadata": {},
"outputs": [],
"source": [
"ET = IF.applique(Lambda_terme('a')).applique(Lambda_terme('b')).applique(FAUX).abstrait('b').abstrait('a')"
]
},
{
"cell_type": "code",
"execution_count": 38,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y)\n"
]
}
],
"source": [
"print(ET)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Et on peut verifier que ce terme satisfait bien à la table de vérité de l'opérateur de conjonction."
]
},
{
"cell_type": "code",
"execution_count": 39,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.x) λx.λy.x)\n",
" 1: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.x) b) λx.λy.y) λx.λy.x)\n",
" 2: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) λx.λy.y)\n",
" 3: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.x) λx.λy.y)\n",
" 4: ---> (λs.((λx.λy.x λx.λy.x) s) λx.λy.y)\n",
" 5: ---> ((λx.λy.x λx.λy.x) λx.λy.y)\n",
" 6: ---> (λy.λx.λy.x λx.λy.y)\n",
" 7: ---> λx.λy.x\n",
"Forme normale calculée : λx.λy.x\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 39,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"ET.applique(VRAI).applique(VRAI).forme_normale(verbose=True) == VRAI"
]
},
{
"cell_type": "code",
"execution_count": 40,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.x) λx.λy.y)\n",
" 1: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.x) b) λx.λy.y) λx.λy.y)\n",
" 2: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.y) λx.λy.y)\n",
" 3: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.y) λx.λy.y)\n",
" 4: ---> (λs.((λx.λy.x λx.λy.y) s) λx.λy.y)\n",
" 5: ---> ((λx.λy.x λx.λy.y) λx.λy.y)\n",
" 6: ---> (λy.λx.λy.y λx.λy.y)\n",
" 7: ---> λx.λy.y\n",
"Forme normale calculée : λx.λy.y\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 40,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"ET.applique(VRAI).applique(FAUX).forme_normale(verbose=True) == FAUX"
]
},
{
"cell_type": "code",
"execution_count": 41,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.y) λx.λy.x)\n",
" 1: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.y) b) λx.λy.y) λx.λy.x)\n",
" 2: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) λx.λy.y)\n",
" 3: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.x) λx.λy.y)\n",
" 4: ---> (λs.((λx.λy.y λx.λy.x) s) λx.λy.y)\n",
" 5: ---> ((λx.λy.y λx.λy.x) λx.λy.y)\n",
" 6: ---> (λy.y λx.λy.y)\n",
" 7: ---> λx.λy.y\n",
"Forme normale calculée : λx.λy.y\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 41,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"ET.applique(FAUX).applique(VRAI).forme_normale(verbose=True) == FAUX"
]
},
{
"cell_type": "code",
"execution_count": 42,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.y) λx.λy.y)\n",
" 1: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.y) b) λx.λy.y) λx.λy.y)\n",
" 2: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.y) λx.λy.y)\n",
" 3: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.y) λx.λy.y)\n",
" 4: ---> (λs.((λx.λy.y λx.λy.y) s) λx.λy.y)\n",
" 5: ---> ((λx.λy.y λx.λy.y) λx.λy.y)\n",
" 6: ---> (λy.y λx.λy.y)\n",
" 7: ---> λx.λy.y\n",
"Forme normale calculée : λx.λy.y\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 42,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"ET.applique(FAUX).applique(FAUX).forme_normale(verbose=True) == FAUX"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Opérateur OU"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"L'opérateur logique de disjonction peut être défini par\n",
"\n",
"$$ \\mathtt{OU} = \\lambda a.\\lambda b.(((\\mathtt{IF}\\ a)\\ \\mathtt{VRAI})\\ b).$$"
]
},
{
"cell_type": "code",
"execution_count": 43,
"metadata": {},
"outputs": [],
"source": [
"OU = IF.applique(Lambda_terme('a')).applique(VRAI).applique(Lambda_terme('b')).abstrait('b').abstrait('a')"
]
},
{
"cell_type": "code",
"execution_count": 44,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b)\n"
]
}
],
"source": [
"print(OU)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Et on peut verifier que ce terme satisfait bien à la table de vérité de l'opérateur de disjonction."
]
},
{
"cell_type": "code",
"execution_count": 45,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.x) λx.λy.x)\n",
" 1: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) b) λx.λy.x)\n",
" 2: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) λx.λy.x)\n",
" 3: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.x) λx.λy.x)\n",
" 4: ---> (λs.((λx.λy.x λx.λy.x) s) λx.λy.x)\n",
" 5: ---> ((λx.λy.x λx.λy.x) λx.λy.x)\n",
" 6: ---> (λy.λx.λy.x λx.λy.x)\n",
" 7: ---> λx.λy.x\n",
"Forme normale calculée : λx.λy.x\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 45,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"OU.applique(VRAI).applique(VRAI).forme_normale(verbose=True) == VRAI"
]
},
{
"cell_type": "code",
"execution_count": 46,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.x) λx.λy.y)\n",
" 1: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) b) λx.λy.y)\n",
" 2: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) λx.λy.y)\n",
" 3: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.x) λx.λy.y)\n",
" 4: ---> (λs.((λx.λy.x λx.λy.x) s) λx.λy.y)\n",
" 5: ---> ((λx.λy.x λx.λy.x) λx.λy.y)\n",
" 6: ---> (λy.λx.λy.x λx.λy.y)\n",
" 7: ---> λx.λy.x\n",
"Forme normale calculée : λx.λy.x\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 46,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"OU.applique(VRAI).applique(FAUX).forme_normale(verbose=True) == VRAI"
]
},
{
"cell_type": "code",
"execution_count": 47,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.y) λx.λy.x)\n",
" 1: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) b) λx.λy.x)\n",
" 2: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) λx.λy.x)\n",
" 3: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.x) λx.λy.x)\n",
" 4: ---> (λs.((λx.λy.y λx.λy.x) s) λx.λy.x)\n",
" 5: ---> ((λx.λy.y λx.λy.x) λx.λy.x)\n",
" 6: ---> (λy.y λx.λy.x)\n",
" 7: ---> λx.λy.x\n",
"Forme normale calculée : λx.λy.x\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 47,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"OU.applique(FAUX).applique(VRAI).forme_normale(verbose=True) == VRAI"
]
},
{
"cell_type": "code",
"execution_count": 48,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.y) λx.λy.y)\n",
" 1: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) b) λx.λy.y)\n",
" 2: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) λx.λy.y)\n",
" 3: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.x) λx.λy.y)\n",
" 4: ---> (λs.((λx.λy.y λx.λy.x) s) λx.λy.y)\n",
" 5: ---> ((λx.λy.y λx.λy.x) λx.λy.y)\n",
" 6: ---> (λy.y λx.λy.y)\n",
" 7: ---> λx.λy.y\n",
"Forme normale calculée : λx.λy.y\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 48,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"OU.applique(FAUX).applique(FAUX).forme_normale(verbose=True) == FAUX"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Opérateur NON"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"L'opérateur de négation peut être défini par le terme\n",
"\n",
"$$ \\mathtt{NON} = \\lambda a.(((\\mathtt{IF}\\ a)\\ \\mathtt{FAUX})\\ \\mathtt{VRAI}).$$"
]
},
{
"cell_type": "code",
"execution_count": 49,
"metadata": {},
"outputs": [],
"source": [
"NON = IF.applique(Lambda_terme('a')).applique(FAUX).applique(VRAI).abstrait('a')"
]
},
{
"cell_type": "code",
"execution_count": 50,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λa.(((λc.λa.λs.((c a) s) a) λx.λy.y) λx.λy.x)\n"
]
}
],
"source": [
"print(NON)"
]
},
{
"cell_type": "code",
"execution_count": 51,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λa.(((λc.λa.λs.((c a) s) a) λx.λy.y) λx.λy.x) λx.λy.x)\n",
" 1: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.y) λx.λy.x)\n",
" 2: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.y) λx.λy.x)\n",
" 3: ---> (λs.((λx.λy.x λx.λy.y) s) λx.λy.x)\n",
" 4: ---> ((λx.λy.x λx.λy.y) λx.λy.x)\n",
" 5: ---> (λy.λx.λy.y λx.λy.x)\n",
" 6: ---> λx.λy.y\n",
"Forme normale calculée : λx.λy.y\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 51,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"NON.applique(VRAI).forme_normale(verbose=True) == FAUX"
]
},
{
"cell_type": "code",
"execution_count": 52,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λa.(((λc.λa.λs.((c a) s) a) λx.λy.y) λx.λy.x) λx.λy.y)\n",
" 1: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.y) λx.λy.x)\n",
" 2: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.y) λx.λy.x)\n",
" 3: ---> (λs.((λx.λy.y λx.λy.y) s) λx.λy.x)\n",
" 4: ---> ((λx.λy.y λx.λy.y) λx.λy.x)\n",
" 5: ---> (λy.y λx.λy.x)\n",
" 6: ---> λx.λy.x\n",
"Forme normale calculée : λx.λy.x\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 52,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"NON.applique(FAUX).forme_normale(verbose=True) == VRAI"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Entiers, successeurs, addition, multiplication et exponentiation"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Numéraux de Church"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Il existe plusieurs façons de représenter les entiers naturels par un $\\lambda$-terme. La représentation donnée ici est connue sous le nom de *numéraux de Church*."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Dans le système de Church, un entier $n\\in\\mathbb{N}$ est représenté par le $\\lambda$-terme\n",
"\n",
"$$ \\lceil n\\rceil = \\lambda f.\\lambda x. (f^n\\ x),$$\n",
"dans lequel le sous-terme $(f^n\\ x)$ est un raccourci pour signifier\n",
"$$ (f^n\\ x) = (f\\ (f\\ (\\ldots (f\\ x)\\ldots))),$$\n",
"terme dans lequel $f$ apparaît $n$ fois.\n",
"En quelque sorte le terme représentant l'entier $n$ est une représentation unaire de $n$.\n",
"\n",
"Ainsi on a\n",
"\n",
"\\begin{align*}\n",
" \\lceil 0\\rceil &= \\lambda f.\\lambda x.x\\\\\n",
" \\lceil 1\\rceil &= \\lambda f.\\lambda x.(f\\ x)\\\\\n",
" \\lceil 2\\rceil &= \\lambda f.\\lambda x.(f\\ (f\\ x))\\\\\n",
" \\lceil 3\\rceil &= \\lambda f.\\lambda x.(f\\ (f\\ (f\\ x))).\n",
"\\end{align*}\n",
"\n",
"Le $\\lambda$-terme $\\lceil n\\rceil$ est donc un terme capable d'appliquer $n$ fois une fonction $F$ sur une donnée $X$. En effet on a\n",
"$$ (\\lceil n\\rceil\\ F) \\twoheadrightarrow_\\beta \\lambda x.(F\\ldots(F\\ x)),$$\n",
"et\n",
"$$ ((\\lceil n\\rceil\\ F)\\ X) \\twoheadrightarrow_\\beta (F\\ldots(F\\ X)).$$\n"
]
},
{
"cell_type": "code",
"execution_count": 53,
"metadata": {},
"outputs": [],
"source": [
"ZERO = Lambda_terme('!f.!x.x')"
]
},
{
"cell_type": "code",
"execution_count": 54,
"metadata": {},
"outputs": [],
"source": [
"UN = Lambda_terme('!f.!x.(f x)')"
]
},
{
"cell_type": "code",
"execution_count": 55,
"metadata": {},
"outputs": [],
"source": [
"DEUX = Lambda_terme('!f.!x.(f (f x))')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le calcul ci-dessous vérifie bien qu'un numéral appliqué à un terme résulte en une fonction itération du terme."
]
},
{
"cell_type": "code",
"execution_count": 56,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λf.λx.(f (f x)) F)\n",
" 1: ---> λx.(F (F x))\n",
"Forme normale calculée : λx.(F (F x))\n"
]
},
{
"data": {
"text/plain": [
"<lambda_calcul.Lambda_terme at 0x7f71cc3b0fd0>"
]
},
"execution_count": 56,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"DEUX.applique(Lambda_terme('F')).forme_normale(verbose=True)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Remarque** les numéraux de Church sont des $\\lambda$-termes clos irréductibles."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Successeur"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Lorsqu'on a compris que pour tout numéral $\\lceil n\\rceil$ on a\n",
"\n",
"$$ ((\\lceil n\\rceil\\ F)\\ X) \\twoheadrightarrow_\\beta (F\\ldots(F\\ X)),$$\n",
"\n",
"alors il est facile de concevoir un $\\lambda$-terme $\\mathtt{SUC}$ tel que\n",
"\n",
"$$ (\\mathtt{SUC}\\ \\lceil n\\rceil) =_\\beta \\lceil n+1\\rceil.$$\n"
]
},
{
"cell_type": "code",
"execution_count": 57,
"metadata": {},
"outputs": [],
"source": [
"SUC = Lambda_terme('!n.!f.!x.(f ((n f) x))')"
]
},
{
"cell_type": "code",
"execution_count": 58,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λn.λf.λx.(f ((n f) x))\n"
]
}
],
"source": [
"print(SUC)"
]
},
{
"cell_type": "code",
"execution_count": 59,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x)))\n",
" 1: ---> λf.λx.(f ((λf.λx.(f (f x)) f) x))\n",
" 2: ---> λf.λx.(f (λx.(f (f x)) x))\n",
" 3: ---> λf.λx.(f (f (f x)))\n",
"Forme normale calculée : λf.λx.(f (f (f x)))\n"
]
}
],
"source": [
"TROIS = SUC.applique(DEUX).forme_normale(verbose=True)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"La fonction qui suit permet d'obtenir le numéral de Church correspondant à un entier naturel (de Python)."
]
},
{
"cell_type": "code",
"execution_count": 60,
"metadata": {},
"outputs": [],
"source": [
"def int_en_church(n):\n",
" if n == 0:\n",
" return ZERO\n",
" else:\n",
" return SUC.applique(int_en_church(n - 1)).forme_normale()"
]
},
{
"cell_type": "code",
"execution_count": 61,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"True\n",
"True\n",
"True\n",
"True\n"
]
}
],
"source": [
"for n, t in enumerate((ZERO, UN, DEUX, TROIS)):\n",
" print(int_en_church(n) == t)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Addition"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"En appliquant trois fois de suite le terme $\\mathtt{SUC}$ sur le terme $\\lceil 2\\rceil$ on obtient un terme dont la forme normale est le numéral $\\lceil 5\\rceil$."
]
},
{
"cell_type": "code",
"execution_count": 62,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λf.λx.(f (f (f x))) λn.λf.λx.(f ((n f) x))) λf.λx.(f (f x)))\n",
" 1: ---> (λx.(λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) x))) λf.λx.(f (f x)))\n",
" 2: ---> (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x)))))\n",
" 3: ---> λf.λx.(f (((λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x)))) f) x))\n",
" 4: ---> λf.λx.(f ((λf.λx.(f (((λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x))) f) x)) f) x))\n",
" 5: ---> λf.λx.(f (λx.(f (((λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x))) f) x)) x))\n",
" 6: ---> λf.λx.(f (f (((λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x))) f) x)))\n",
" 7: ---> λf.λx.(f (f ((λf.λx.(f ((λf.λx.(f (f x)) f) x)) f) x)))\n",
" 8: ---> λf.λx.(f (f (λx.(f ((λf.λx.(f (f x)) f) x)) x)))\n",
" 9: ---> λf.λx.(f (f (f ((λf.λx.(f (f x)) f) x))))\n",
" 10: ---> λf.λx.(f (f (f (λx.(f (f x)) x))))\n",
" 11: ---> λf.λx.(f (f (f (f (f x)))))\n",
"Forme normale calculée : λf.λx.(f (f (f (f (f x)))))\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 62,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"TROIS.applique(SUC).applique(DEUX).forme_normale(verbose=True) == int_en_church(5)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Ainsi on peut définir un $\\lambda$-terme $\\mathtt{ADD}$ qui appliqué à deux numéraux est $\\beta$-équivalent au numéral somme.\n",
"En définissant donc \n",
"$$ \\mathtt{ADD} = \\lambda n.\\lambda m.((n\\ \\mathtt{SUC})\\ m),$$\n",
"on a\n",
"$$ ((\\mathtt{ADD}\\ \\lceil n\\rceil)\\ \\lceil m\\rceil) =_\\beta \\lceil n+m\\rceil.$$"
]
},
{
"cell_type": "code",
"execution_count": 63,
"metadata": {},
"outputs": [],
"source": [
"M_ADD = Lambda_terme('!n.!m.((n SUC) m)')\n",
"ADD = M_ADD.subs('SUC', SUC)"
]
},
{
"cell_type": "code",
"execution_count": 64,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λn.λm.((n λn.λf.λx.(f ((n f) x))) m)\n"
]
}
],
"source": [
"print(ADD)"
]
},
{
"cell_type": "code",
"execution_count": 65,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f x)) λf.λx.(f (f (f x))))\n",
" 1: ---> (λm.((λf.λx.(f x) λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x))))\n",
" 2: ---> ((λf.λx.(f x) λn.λf.λx.(f ((n f) x))) λf.λx.(f (f (f x))))\n",
" 3: ---> (λx.(λn.λf.λx.(f ((n f) x)) x) λf.λx.(f (f (f x))))\n",
" 4: ---> (λn.λf.λx.(f ((n f) x)) λf.λx.(f (f (f x))))\n",
" 5: ---> λf.λx.(f ((λf.λx.(f (f (f x))) f) x))\n",
" 6: ---> λf.λx.(f (λx.(f (f (f x))) x))\n",
" 7: ---> λf.λx.(f (f (f (f x))))\n",
"Forme normale calculée : λf.λx.(f (f (f (f x))))\n"
]
}
],
"source": [
"QUATRE = ADD.applique(UN).applique(TROIS).forme_normale(verbose=True)"
]
},
{
"cell_type": "code",
"execution_count": 66,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) λf.λx.(f (f x)))\n",
" 1: ---> (λm.((λf.λx.(f (f (f x))) λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f x)))\n",
" 2: ---> ((λf.λx.(f (f (f x))) λn.λf.λx.(f ((n f) x))) λf.λx.(f (f x)))\n",
" 3: ---> (λx.(λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) x))) λf.λx.(f (f x)))\n",
" 4: ---> (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x)))))\n",
" 5: ---> λf.λx.(f (((λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x)))) f) x))\n",
" 6: ---> λf.λx.(f ((λf.λx.(f (((λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x))) f) x)) f) x))\n",
" 7: ---> λf.λx.(f (λx.(f (((λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x))) f) x)) x))\n",
" 8: ---> λf.λx.(f (f (((λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x))) f) x)))\n",
" 9: ---> λf.λx.(f (f ((λf.λx.(f ((λf.λx.(f (f x)) f) x)) f) x)))\n",
" 10: ---> λf.λx.(f (f (λx.(f ((λf.λx.(f (f x)) f) x)) x)))\n",
" 11: ---> λf.λx.(f (f (f ((λf.λx.(f (f x)) f) x))))\n",
" 12: ---> λf.λx.(f (f (f (λx.(f (f x)) x))))\n",
" 13: ---> λf.λx.(f (f (f (f (f x)))))\n",
"Forme normale calculée : λf.λx.(f (f (f (f (f x)))))\n"
]
}
],
"source": [
"CINQ = ADD.applique(TROIS).applique(DEUX).forme_normale(verbose=True)"
]
},
{
"cell_type": "code",
"execution_count": 67,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f (f x))))) λf.λx.(f (f (f x))))\n",
" 1: ---> (λm.((λf.λx.(f (f (f (f x)))) λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x))))\n",
" 2: ---> ((λf.λx.(f (f (f (f x)))) λn.λf.λx.(f ((n f) x))) λf.λx.(f (f (f x))))\n",
" 3: ---> (λx.(λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) x)))) λf.λx.(f (f (f x))))\n",
" 4: ---> (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.(f (f (f x)))))))\n",
" 5: ---> λf.λx.(f (((λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.(f (f (f x)))))) f) x))\n",
" 6: ---> λf.λx.(f ((λf.λx.(f (((λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.(f (f (f x))))) f) x)) f) x))\n",
" 7: ---> λf.λx.(f (λx.(f (((λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.(f (f (f x))))) f) x)) x))\n",
" 8: ---> λf.λx.(f (f (((λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.(f (f (f x))))) f) x)))\n",
" 9: ---> λf.λx.(f (f ((λf.λx.(f (((λn.λf.λx.(f ((n f) x)) λf.λx.(f (f (f x)))) f) x)) f) x)))\n",
" 10: ---> λf.λx.(f (f (λx.(f (((λn.λf.λx.(f ((n f) x)) λf.λx.(f (f (f x)))) f) x)) x)))\n",
" 11: ---> λf.λx.(f (f (f (((λn.λf.λx.(f ((n f) x)) λf.λx.(f (f (f x)))) f) x))))\n",
" 12: ---> λf.λx.(f (f (f ((λf.λx.(f ((λf.λx.(f (f (f x))) f) x)) f) x))))\n",
" 13: ---> λf.λx.(f (f (f (λx.(f ((λf.λx.(f (f (f x))) f) x)) x))))\n",
" 14: ---> λf.λx.(f (f (f (f ((λf.λx.(f (f (f x))) f) x)))))\n",
" 15: ---> λf.λx.(f (f (f (f (λx.(f (f (f x))) x)))))\n",
" 16: ---> λf.λx.(f (f (f (f (f (f (f x)))))))\n",
"Forme normale calculée : λf.λx.(f (f (f (f (f (f (f x)))))))\n"
]
}
],
"source": [
"SEPT = ADD.applique(QUATRE).applique(TROIS).forme_normale(verbose=True)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Multiplication"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On pourrait définir un terme pour la multiplication en considérant que multiplier $n$ par $m$ c'est répéter $n$ fois l'addition de $m$ à partir de 0."
]
},
{
"cell_type": "code",
"execution_count": 68,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λn.λm.((n (λn.λm.((n λn.λf.λx.(f ((n f) x))) m) m)) λf.λx.x)\n"
]
}
],
"source": [
"M_MUL = Lambda_terme('!n.!m.((n (ADD m)) ZERO)')\n",
"MUL = M_MUL.subs('ADD', ADD).subs('ZERO', ZERO)\n",
"print(MUL)"
]
},
{
"cell_type": "code",
"execution_count": 69,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λn.λm.((n (λn.λm.((n λn.λf.λx.(f ((n f) x))) m) m)) λf.λx.x) λf.λx.(f (f x))) λf.λx.(f (f (f x))))\n",
" 1: ---> (λm.((λf.λx.(f (f x)) (λn.λm.((n λn.λf.λx.(f ((n f) x))) m) m)) λf.λx.x) λf.λx.(f (f (f x))))\n",
" 2: ---> ((λf.λx.(f (f x)) (λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x))))) λf.λx.x)\n",
" 3: ---> (λx.((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) ((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) x)) λf.λx.x)\n",
" 4: ---> ((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) ((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) λf.λx.x))\n",
" 5: ---> (λm.((λf.λx.(f (f (f x))) λn.λf.λx.(f ((n f) x))) m) ((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) λf.λx.x))\n",
" 6: ---> ((λf.λx.(f (f (f x))) λn.λf.λx.(f ((n f) x))) ((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) λf.λx.x))\n",
" 7: ---> (λx.(λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) x))) ((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) λf.λx.x))\n",
" 8: ---> (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) ((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) λf.λx.x))))\n",
" 9: ---> λf.λx.(f (((λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) ((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) λf.λx.x))) f) x))\n",
" 10: ---> λf.λx.(f ((λf.λx.(f (((λn.λf.λx.(f ((n f) x)) ((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) λf.λx.x)) f) x)) f) x))\n",
" 11: ---> λf.λx.(f (λx.(f (((λn.λf.λx.(f ((n f) x)) ((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) λf.λx.x)) f) x)) x))\n",
" 12: ---> λf.λx.(f (f (((λn.λf.λx.(f ((n f) x)) ((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) λf.λx.x)) f) x)))\n",
" 13: ---> λf.λx.(f (f ((λf.λx.(f ((((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) λf.λx.x) f) x)) f) x)))\n",
" 14: ---> λf.λx.(f (f (λx.(f ((((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) λf.λx.x) f) x)) x)))\n",
" 15: ---> λf.λx.(f (f (f ((((λn.λm.((n λn.λf.λx.(f ((n f) x))) m) λf.λx.(f (f (f x)))) λf.λx.x) f) x))))\n",
" 16: ---> λf.λx.(f (f (f (((λm.((λf.λx.(f (f (f x))) λn.λf.λx.(f ((n f) x))) m) λf.λx.x) f) x))))\n",
" 17: ---> λf.λx.(f (f (f ((((λf.λx.(f (f (f x))) λn.λf.λx.(f ((n f) x))) λf.λx.x) f) x))))\n",
" 18: ---> λf.λx.(f (f (f (((λx.(λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) x))) λf.λx.x) f) x))))\n",
" 19: ---> λf.λx.(f (f (f (((λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.x))) f) x))))\n",
" 20: ---> λf.λx.(f (f (f ((λf.λx.(f (((λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.x)) f) x)) f) x))))\n",
" 21: ---> λf.λx.(f (f (f (λx.(f (((λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.x)) f) x)) x))))\n",
" 22: ---> λf.λx.(f (f (f (f (((λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.x)) f) x)))))\n",
" 23: ---> λf.λx.(f (f (f (f ((λf.λx.(f (((λn.λf.λx.(f ((n f) x)) λf.λx.x) f) x)) f) x)))))\n",
" 24: ---> λf.λx.(f (f (f (f (λx.(f (((λn.λf.λx.(f ((n f) x)) λf.λx.x) f) x)) x)))))\n",
" 25: ---> λf.λx.(f (f (f (f (f (((λn.λf.λx.(f ((n f) x)) λf.λx.x) f) x))))))\n",
" 26: ---> λf.λx.(f (f (f (f (f ((λf.λx.(f ((λf.λx.x f) x)) f) x))))))\n",
" 27: ---> λf.λx.(f (f (f (f (f (λx.(f ((λf.λx.x f) x)) x))))))\n",
" 28: ---> λf.λx.(f (f (f (f (f (f ((λf.λx.x f) x)))))))\n",
" 29: ---> λf.λx.(f (f (f (f (f (f (λx.x x)))))))\n",
" 30: ---> λf.λx.(f (f (f (f (f (f x))))))\n",
"Forme normale calculée : λf.λx.(f (f (f (f (f (f x))))))\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 69,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"MUL.applique(DEUX).applique(TROIS).forme_normale(verbose=True) == int_en_church(6)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Mais il s'avère plus simple (et plus efficace comme on pourra le constater) de définir le terme $\\mathtt{MUL}$ par\n",
"$$ \\mathtt{MUL} = \\lambda n.\\lambda m.\\lambda f.(n\\ (m\\ f)).$$\n",
"\n",
"En effet, il est clair que\n",
"$$ ((\\mathtt{MUL} \\lceil n\\rceil)\\ \\lceil m\\rceil) \\twoheadrightarrow_\\beta \\lambda f.(\\lceil n\\rceil\\ (\\lceil m\\rceil\\ f)),$$\n",
"et le terme obtenu est la répétition $m$ fois du terme $f$, répétition répétée elle-même $n$ fois. Au bilan le terme $f$ est répété $n\\times m$ fois.\n",
"\n",
"Et on a donc bien\n",
"$$ ((\\mathtt{MUL} \\lceil n\\rceil)\\ \\lceil m\\rceil) =_\\beta \\lceil n\\times m\\rceil.$$"
]
},
{
"cell_type": "code",
"execution_count": 70,
"metadata": {},
"outputs": [],
"source": [
"MUL = Lambda_terme('!n.!m.!f.(n (m f))')"
]
},
{
"cell_type": "code",
"execution_count": 71,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λn.λm.λf.(n (m f)) λf.λx.(f (f x))) λf.λx.(f (f (f x))))\n",
" 1: ---> (λm.λf.(λf.λx.(f (f x)) (m f)) λf.λx.(f (f (f x))))\n",
" 2: ---> λf.(λf.λx.(f (f x)) (λf.λx.(f (f (f x))) f))\n",
" 3: ---> λf.λx.((λf.λx.(f (f (f x))) f) ((λf.λx.(f (f (f x))) f) x))\n",
" 4: ---> λf.λx.(λx.(f (f (f x))) ((λf.λx.(f (f (f x))) f) x))\n",
" 5: ---> λf.λx.(f (f (f ((λf.λx.(f (f (f x))) f) x))))\n",
" 6: ---> λf.λx.(f (f (f (λx.(f (f (f x))) x))))\n",
" 7: ---> λf.λx.(f (f (f (f (f (f x))))))\n",
"Forme normale calculée : λf.λx.(f (f (f (f (f (f x))))))\n"
]
}
],
"source": [
"SIX = MUL.applique(DEUX).applique(TROIS).forme_normale(verbose=True)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le calcul de la forme normale de $((\\mathtt{MUL}\\ \\lceil 2\\rceil)\\ \\lceil 3\\rceil)$ avec cette version de $\\mathtt{MUL}$ est bien plus court que le calcul effectué avec la version précédente."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Exponentiation"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Comme pour la multiplication, on pourrait envisager de définir un terme pour l'exponentiation en considérant qu'il suffit de répéter $m$ fois le terme $\\mathtt{MUL}$ appliqué à $n$ pour obtenir un terme qui se réduirait au numéral représentant $n^m$.\n",
"\n",
"Mais il est possible de définir un terme beaucoup plus simple :\n",
"$$ \\mathtt{EXP} = \\lambda n.\\lambda m.(m\\ n).$"
]
},
{
"cell_type": "code",
"execution_count": 72,
"metadata": {},
"outputs": [],
"source": [
"EXP = Lambda_terme('!n.!m.(m n)')"
]
},
{
"cell_type": "code",
"execution_count": 73,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λn.λm.(m n) λf.λx.(f (f x))) λf.λx.(f (f (f x))))\n",
" 1: ---> (λm.(m λf.λx.(f (f x))) λf.λx.(f (f (f x))))\n",
" 2: ---> (λf.λx.(f (f (f x))) λf.λx.(f (f x)))\n",
" 3: ---> λx.(λf.λx.(f (f x)) (λf.λx.(f (f x)) (λf.λx.(f (f x)) x)))\n",
" 4: ---> λx.λx0.((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0))\n",
" 5: ---> λx.λx0.(λx0.((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) x) x0)) ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0))\n",
" 6: ---> λx.λx0.((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0)))\n",
" 7: ---> λx.λx0.(λx0.(x (x x0)) ((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0)))\n",
" 8: ---> λx.λx0.(x (x ((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0))))\n",
" 9: ---> λx.λx0.(x (x (λx0.(x (x x0)) ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0))))\n",
" 10: ---> λx.λx0.(x (x (x (x ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0)))))\n",
" 11: ---> λx.λx0.(x (x (x (x (λx0.((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) x) x0)) x0)))))\n",
" 12: ---> λx.λx0.(x (x (x (x ((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) x) x0))))))\n",
" 13: ---> λx.λx0.(x (x (x (x (λx0.(x (x x0)) ((λf.λx.(f (f x)) x) x0))))))\n",
" 14: ---> λx.λx0.(x (x (x (x (x (x ((λf.λx.(f (f x)) x) x0)))))))\n",
" 15: ---> λx.λx0.(x (x (x (x (x (x (λx0.(x (x x0)) x0)))))))\n",
" 16: ---> λx.λx0.(x (x (x (x (x (x (x (x x0))))))))\n",
"Forme normale calculée : λx.λx0.(x (x (x (x (x (x (x (x x0))))))))\n"
]
}
],
"source": [
"HUIT = EXP.applique(DEUX).applique(TROIS).forme_normale(verbose=True)"
]
},
{
"cell_type": "code",
"execution_count": 74,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 74,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"HUIT == int_en_church(8)"
]
},
{
"cell_type": "code",
"execution_count": 75,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λn.λm.(m n) λf.λx.(f (f (f x)))) λf.λx.(f (f x)))\n",
" 1: ---> (λm.(m λf.λx.(f (f (f x)))) λf.λx.(f (f x)))\n",
" 2: ---> (λf.λx.(f (f x)) λf.λx.(f (f (f x))))\n",
" 3: ---> λx.(λf.λx.(f (f (f x))) (λf.λx.(f (f (f x))) x))\n",
" 4: ---> λx.λx0.((λf.λx.(f (f (f x))) x) ((λf.λx.(f (f (f x))) x) ((λf.λx.(f (f (f x))) x) x0)))\n",
" 5: ---> λx.λx0.(λx0.(x (x (x x0))) ((λf.λx.(f (f (f x))) x) ((λf.λx.(f (f (f x))) x) x0)))\n",
" 6: ---> λx.λx0.(x (x (x ((λf.λx.(f (f (f x))) x) ((λf.λx.(f (f (f x))) x) x0)))))\n",
" 7: ---> λx.λx0.(x (x (x (λx0.(x (x (x x0))) ((λf.λx.(f (f (f x))) x) x0)))))\n",
" 8: ---> λx.λx0.(x (x (x (x (x (x ((λf.λx.(f (f (f x))) x) x0)))))))\n",
" 9: ---> λx.λx0.(x (x (x (x (x (x (λx0.(x (x (x x0))) x0)))))))\n",
" 10: ---> λx.λx0.(x (x (x (x (x (x (x (x (x x0)))))))))\n",
"Forme normale calculée : λx.λx0.(x (x (x (x (x (x (x (x (x x0)))))))))\n"
]
}
],
"source": [
"NEUF = EXP.applique(TROIS).applique(DEUX).forme_normale(verbose=True)"
]
},
{
"cell_type": "code",
"execution_count": 76,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 76,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"NEUF == int_en_church(9)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Nullité"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Considérons le terme $((\\lceil n\\rceil\\ \\lambda x.\\mathtt{FAUX})\\ \\mathtt{VRAI})$. Si $n=0$ on a \n",
"$$((\\lceil 0\\rceil\\ \\lambda x.\\mathtt{FAUX})\\ \\mathtt{VRAI}) \\twoheadrightarrow_\\beta (\\lambda x.x\\ \\mathtt{VRAI}) \\rightarrow_\\beta \\mathtt{VRAI}.$$\n",
"Et si $n\\neq 0$ on a\n",
"$$((\\lceil n\\rceil\\ \\lambda x.\\mathtt{FAUX})\\ \\mathtt{VRAI}) \\twoheadrightarrow_\\beta (\\lambda x.\\mathtt{FAUX}\\ \\mathtt{VRAI}) \\rightarrow_\\beta \\mathtt{FAUX}.$$\n",
"\n",
"Avec une abstraction, on obtient le $\\lambda$-terme \n",
"$$ \\mathtt{NUL} = \\lambda n.(),$$\n",
"tel que pour $n=0$\n",
"$$ (\\mathtt{NUL}\\ \\lceil 0\\rceil) =_\\beta \\mathtt{VRAI},$$\n",
"et pour $n\\neq 0$\n",
"$$ (\\mathtt{NUL}\\ \\lceil n\\rceil) =_\\beta \\mathtt{FAUX}.$$\n",
"\n",
"En d'autres termes, le $\\lambda$-terme $\\mathtt{NUL}$ correspond à un prédicat permettant de tester la nullité d'un entier."
]
},
{
"cell_type": "code",
"execution_count": 77,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λn.((n λx.FAUX) VRAI)\n",
"λn.((n λx.λx.λy.y) λx.λy.x)\n"
]
}
],
"source": [
"M_NUL = Lambda_terme('!n.((n !x.FAUX) VRAI)')\n",
"print(M_NUL)\n",
"NUL = M_NUL.subs('FAUX', FAUX).subs('VRAI', VRAI)\n",
"print(NUL)"
]
},
{
"cell_type": "code",
"execution_count": 78,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λn.((n λx.λx.λy.y) λx.λy.x) λf.λx.x)\n",
" 1: ---> ((λf.λx.x λx.λx.λy.y) λx.λy.x)\n",
" 2: ---> (λx.x λx.λy.x)\n",
" 3: ---> λx.λy.x\n",
"Forme normale calculée : λx.λy.x\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 78,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"NUL.applique(ZERO).forme_normale(verbose=True) == VRAI"
]
},
{
"cell_type": "code",
"execution_count": 79,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λn.((n λx.λx.λy.y) λx.λy.x) λf.λx.(f (f (f x))))\n",
" 1: ---> ((λf.λx.(f (f (f x))) λx.λx.λy.y) λx.λy.x)\n",
" 2: ---> (λx.(λx.λx.λy.y (λx.λx.λy.y (λx.λx.λy.y x))) λx.λy.x)\n",
" 3: ---> (λx.λx.λy.y (λx.λx.λy.y (λx.λx.λy.y λx.λy.x)))\n",
" 4: ---> λx.λy.y\n",
"Forme normale calculée : λx.λy.y\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 79,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"NUL.applique(TROIS).forme_normale(verbose=True) == FAUX"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Remarque** Arrivé à ce stade, il nous manque une opération arithmétique de base : la soustraction, et la possibilité de comparaison plus générale permettant de décider si un entier est inférieur à un autre. Ce manque sera comblé une fois que nous aurons vu une représentation des couples."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Couples et listes"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Constructeur et sélecteurs de couples"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Comment exprimer un couple de $\\lambda$-termes à l'aide d'un $\\lambda$-terme ? Une fois ce couple exprimé comment en extraire chacune des deux composantes ? "
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Soient $M$ et $N$ deux $\\lambda$-termes quelconques. Considérons les deux termes $((\\mathtt{VRAI}\\ M)\\ N)$ et $((\\mathtt{FAUX}\\ M)\\ N)$. Il est facile de vérifier que\n",
"$$ ((\\mathtt{VRAI}\\ M)\\ N) =_\\beta M,$$\n",
"et\n",
"$$ ((\\mathtt{FAUX}\\ M)\\ N) =_\\beta N.$$\n",
"\n",
"On déduit de ce constat que \n",
"$$[M, N] = \\lambda s.((s\\ M)\\ N)$$\n",
"est un $\\lambda$-terme pouvant représenter le couple $(M, N)$ et que la sélection de l'une ou l'autre des deux composantes peut se faire en appliquant le terme sur l'un ou l'autre des deux termes $\\mathtt{VRAI}$ ou $\\mathtt{FAUX}$ :\n",
"\n",
"$$ ([M, N]\\ \\mathtt{VRAI}) =_\\beta M,$$\n",
"et\n",
"$$ ([M, N]\\ \\mathtt{FAUX}) =_\\beta N.$$"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Ces considérations amènent à définir le terme constructeur de couple $\\mathtt{CONS}$\n",
"$$ \\mathtt{CONS} = \\lambda x.\\lambda y.\\lambda s.((s\\ x)\\ y),$$\n",
"ainsi que les deux sélecteurs $\\mathtt{CAR}$, pour accéder à la première composante, et $\\mathtt{CDR}$, pour accéder à la deuxième composante\n",
"$$\\mathtt{CAR} = \\lambda c.(c\\ \\mathtt{VRAI}),$$\n",
"et\n",
"$$\\mathtt{CDR} = \\lambda c.(c\\ \\mathtt{FAUX}).$$"
]
},
{
"cell_type": "code",
"execution_count": 80,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λx.λy.λs.((s x) y)\n"
]
}
],
"source": [
"CONS = Lambda_terme('!x.!y.!s.((s x) y)')\n",
"print(CONS)"
]
},
{
"cell_type": "code",
"execution_count": 81,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λx.λy.λs.((s x) y) λf.λx.(f x)) λf.λx.(f (f x)))\n",
" 1: ---> (λy.λs.((s λf.λx.(f x)) y) λf.λx.(f (f x)))\n",
" 2: ---> λs.((s λf.λx.(f x)) λf.λx.(f (f x)))\n",
"Forme normale calculée : λs.((s λf.λx.(f x)) λf.λx.(f (f x)))\n"
]
}
],
"source": [
"UN_DEUX = CONS.applique(UN).applique(DEUX).forme_normale(verbose=True)"
]
},
{
"cell_type": "code",
"execution_count": 82,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λc.(c VRAI)\n",
"λc.(c λx.λy.x)\n"
]
}
],
"source": [
"M_CAR = Lambda_terme('!c.(c VRAI)')\n",
"print(M_CAR)\n",
"CAR = M_CAR.subs('VRAI', VRAI)\n",
"print(CAR)"
]
},
{
"cell_type": "code",
"execution_count": 83,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λc.(c λx.λy.x) λs.((s λf.λx.(f x)) λf.λx.(f (f x))))\n",
" 1: ---> (λs.((s λf.λx.(f x)) λf.λx.(f (f x))) λx.λy.x)\n",
" 2: ---> ((λx.λy.x λf.λx.(f x)) λf.λx.(f (f x)))\n",
" 3: ---> (λy.λf.λx.(f x) λf.λx.(f (f x)))\n",
" 4: ---> λf.λx.(f x)\n",
"Forme normale calculée : λf.λx.(f x)\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 83,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"CAR.applique(UN_DEUX).forme_normale(verbose=True) == UN"
]
},
{
"cell_type": "code",
"execution_count": 84,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λc.(c FAUX)\n",
"λc.(c λx.λy.y)\n"
]
}
],
"source": [
"M_CDR = Lambda_terme('!c.(c FAUX)')\n",
"print(M_CDR)\n",
"CDR = M_CDR.subs('FAUX', FAUX)\n",
"print(CDR)"
]
},
{
"cell_type": "code",
"execution_count": 85,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λc.(c λx.λy.y) λs.((s λf.λx.(f x)) λf.λx.(f (f x))))\n",
" 1: ---> (λs.((s λf.λx.(f x)) λf.λx.(f (f x))) λx.λy.y)\n",
" 2: ---> ((λx.λy.y λf.λx.(f x)) λf.λx.(f (f x)))\n",
" 3: ---> (λy.y λf.λx.(f (f x)))\n",
" 4: ---> λf.λx.(f (f x))\n",
"Forme normale calculée : λf.λx.(f (f x))\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 85,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"CDR.applique(UN_DEUX).forme_normale(verbose=True) == DEUX"
]
},
{
"cell_type": "code",
"execution_count": 86,
"metadata": {},
"outputs": [],
"source": [
"M = Lambda_terme('M')\n",
"CPLE_M = CONS.applique(CAR.applique(M)).applique(CDR.applique(M))"
]
},
{
"cell_type": "code",
"execution_count": 87,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) (λc.(c λx.λy.x) M)) (λc.(c λx.λy.y) M)))\n",
" 1: ---> (((λx.λy.λs.((s x) y) (λc.(c λx.λy.x) M)) (λc.(c λx.λy.y) M)) λx.λy.y)\n",
" 2: ---> ((λy.λs.((s (λc.(c λx.λy.x) M)) y) (λc.(c λx.λy.y) M)) λx.λy.y)\n",
" 3: ---> (λs.((s (λc.(c λx.λy.x) M)) (λc.(c λx.λy.y) M)) λx.λy.y)\n",
" 4: ---> ((λx.λy.y (λc.(c λx.λy.x) M)) (λc.(c λx.λy.y) M))\n",
" 5: ---> (λy.y (λc.(c λx.λy.y) M))\n",
" 6: ---> (λc.(c λx.λy.y) M)\n",
" 7: ---> (M λx.λy.y)\n",
"Forme normale calculée : (M λx.λy.y)\n"
]
},
{
"data": {
"text/plain": [
"<lambda_calcul.Lambda_terme at 0x7f71cc300710>"
]
},
"execution_count": 87,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"CDR.applique(CPLE_M).forme_normale(verbose=True)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Remarques** \n",
"1. le terme $((\\mathtt{CONS}\\ M)\\ N)$ est clos si et seulement si $M$ et $N$ le sont, et il est normalisable si et seulement si $M$ et $N$ le sont.\n",
"\n",
"2. les noms donnés aux termes $\\mathtt{CONS}$, $\\mathtt{CAR}$ et $\\mathtt{CDR}$ font référence aux noms donnés aux constructeurs et sélecteurs de paires dans le langage de programmation LISP (et ses successeurs comme SCHEME)."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Prédécesseur d'un entier, soustraction"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Envisageons la fonction $F$ qui, à un couple $(m, n)$ d'entiers, associe le couple $(n, n+1)$. En partant du couple $(0,0)$ et en itérant $n$ fois cette fonction, on obtient le couple $(n-1, n)$. La première composante de ce couple est l'entier $n-1$, donc l'entier qui précède $n$.\n",
"\n",
"C'est l'idée de base pour définir un $\\lambda$-terme $\\mathtt{PRED}$ tel que pour tout entier $n\\geq 1$ on ait\n",
"$$ (\\mathtt{PRED}\\ \\lceil n\\rceil) =_\\beta \\lceil n-1\\rceil.$$"
]
},
{
"cell_type": "code",
"execution_count": 88,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λc.((CONS (CDR c)) (SUC (CDR c)))\n",
"λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))\n"
]
}
],
"source": [
"M_F = Lambda_terme('!c.((CONS (CDR c)) (SUC (CDR c)))')\n",
"print(M_F)\n",
"F = M_F.subs('CONS', CONS).subs('CDR', CDR).subs('SUC', SUC)\n",
"print(F)"
]
},
{
"cell_type": "code",
"execution_count": 89,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 89,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"QUATRE.applique(F).applique(CONS.applique(ZERO).applique(ZERO)).forme_normale() == CONS.applique(TROIS).applique(QUATRE).forme_normale()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le $\\lambda$-terme $\\mathtt{PRED}$ est défini par\n",
"\n",
"$$ \\mathtt{PRED} = \\lambda n.(\\mathtt{CAR} ((n \\lambda c.((\\mathtt{CONS}\\ (\\mathtt{CDR}\\ c))\\ (\\mathtt{SUC} (\\mathtt{CDR}\\ c)))) ((\\mathtt{CONS}\\ \\mathtt{ZERO})\\ \\mathtt{ZERO}))).$$"
]
},
{
"cell_type": "code",
"execution_count": 90,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λn.(CAR ((n λc.((CONS (CDR c)) (SUC (CDR c)))) ((CONS ZERO) ZERO)))\n",
"λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))\n"
]
}
],
"source": [
"M_PRED = Lambda_terme('!n.(CAR ((n !c.((CONS (CDR c)) (SUC (CDR c)))) ((CONS ZERO) ZERO)))')\n",
"print(M_PRED)\n",
"PRED = M_PRED.subs('CAR', CAR).subs('CONS', CONS).subs('CDR', CDR).subs('SUC', SUC).subs('ZERO', ZERO)\n",
"print(PRED)"
]
},
{
"cell_type": "code",
"execution_count": 91,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f (f (f (f (f x))))))\n",
" 1: ---> (λc.(c λx.λy.x) ((λf.λx.(f (f (f (f (f x))))) λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))\n",
" 2: ---> (((λf.λx.(f (f (f (f (f x))))) λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
" 3: ---> ((λx.(λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) x))))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
" 4: ---> ((λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))) λx.λy.x)\n",
" 5: ---> (((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))))) λx.λy.x)\n",
" 6: ---> ((λy.λs.((s (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))))) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))))) λx.λy.x)\n",
" 7: ---> (λs.((s (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))))) λx.λy.x)\n",
" 8: ---> ((λx.λy.x (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))))))\n",
" 9: ---> (λy.(λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))))))\n",
" 10: ---> (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))))\n",
" 11: ---> ((λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) λx.λy.y)\n",
" 12: ---> (((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))))) λx.λy.y)\n",
" 13: ---> ((λy.λs.((s (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))))) λx.λy.y)\n",
" 14: ---> (λs.((s (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))))) λx.λy.y)\n",
" 15: ---> ((λx.λy.y (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))))\n",
" 16: ---> (λy.y (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))))\n",
" 17: ---> (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))))\n",
" 18: ---> λf.λx.(f (((λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) f) x))\n",
" 19: ---> λf.λx.(f ((((λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) λx.λy.y) f) x))\n",
" 20: ---> λf.λx.(f (((((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))) λx.λy.y) f) x))\n",
" 21: ---> λf.λx.(f ((((λy.λs.((s (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))) λx.λy.y) f) x))\n",
" 22: ---> λf.λx.(f (((λs.((s (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))) λx.λy.y) f) x))\n",
" 23: ---> λf.λx.(f ((((λx.λy.y (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))) f) x))\n",
" 24: ---> λf.λx.(f (((λy.y (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))) f) x))\n",
" 25: ---> λf.λx.(f (((λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) f) x))\n",
" 26: ---> λf.λx.(f ((λf.λx.(f (((λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) f) x)) f) x))\n",
" 27: ---> λf.λx.(f (λx.(f (((λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) f) x)) x))\n",
" 28: ---> λf.λx.(f (f (((λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) f) x)))\n",
" 29: ---> λf.λx.(f (f ((((λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λx.λy.y) f) x)))\n",
" 30: ---> λf.λx.(f (f (((((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) λx.λy.y) f) x)))\n",
" 31: ---> λf.λx.(f (f ((((λy.λs.((s (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) λx.λy.y) f) x)))\n",
" 32: ---> λf.λx.(f (f (((λs.((s (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) λx.λy.y) f) x)))\n",
" 33: ---> λf.λx.(f (f ((((λx.λy.y (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) f) x)))\n",
" 34: ---> λf.λx.(f (f (((λy.y (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) f) x)))\n",
" 35: ---> λf.λx.(f (f (((λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) f) x)))\n",
" 36: ---> λf.λx.(f (f ((λf.λx.(f (((λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) f) x)) f) x)))\n",
" 37: ---> λf.λx.(f (f (λx.(f (((λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) f) x)) x)))\n",
" 38: ---> λf.λx.(f (f (f (((λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) f) x))))\n",
" 39: ---> λf.λx.(f (f (f ((((λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)) λx.λy.y) f) x))))\n",
" 40: ---> λf.λx.(f (f (f (((((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) λx.λy.y) f) x))))\n",
" 41: ---> λf.λx.(f (f (f ((((λy.λs.((s (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) λx.λy.y) f) x))))\n",
" 42: ---> λf.λx.(f (f (f (((λs.((s (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) λx.λy.y) f) x))))\n",
" 43: ---> λf.λx.(f (f (f ((((λx.λy.y (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) f) x))))\n",
" 44: ---> λf.λx.(f (f (f (((λy.y (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) f) x))))\n",
" 45: ---> λf.λx.(f (f (f (((λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) f) x))))\n",
" 46: ---> λf.λx.(f (f (f ((λf.λx.(f (((λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)) f) x)) f) x))))\n",
" 47: ---> λf.λx.(f (f (f (λx.(f (((λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)) f) x)) x))))\n",
" 48: ---> λf.λx.(f (f (f (f (((λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)) f) x)))))\n",
" 49: ---> λf.λx.(f (f (f (f (((((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x) λx.λy.y) f) x)))))\n",
" 50: ---> λf.λx.(f (f (f (f ((((λy.λs.((s λf.λx.x) y) λf.λx.x) λx.λy.y) f) x)))))\n",
" 51: ---> λf.λx.(f (f (f (f (((λs.((s λf.λx.x) λf.λx.x) λx.λy.y) f) x)))))\n",
" 52: ---> λf.λx.(f (f (f (f ((((λx.λy.y λf.λx.x) λf.λx.x) f) x)))))\n",
" 53: ---> λf.λx.(f (f (f (f (((λy.y λf.λx.x) f) x)))))\n",
" 54: ---> λf.λx.(f (f (f (f ((λf.λx.x f) x)))))\n",
" 55: ---> λf.λx.(f (f (f (f (λx.x x)))))\n",
" 56: ---> λf.λx.(f (f (f (f x))))\n",
"Forme normale calculée : λf.λx.(f (f (f (f x))))\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 91,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"PRED.applique(CINQ).forme_normale(verbose=True) == QUATRE"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Remarque** le terme $(\\mathtt{PRED}\\ \\mathtt{ZERO})$ est normalisable et sa forme normale est $\\mathtt{ZERO}$."
]
},
{
"cell_type": "code",
"execution_count": 92,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.x)\n",
" 1: ---> (λc.(c λx.λy.x) ((λf.λx.x λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))\n",
" 2: ---> (((λf.λx.x λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
" 3: ---> ((λx.x ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
" 4: ---> (((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x) λx.λy.x)\n",
" 5: ---> ((λy.λs.((s λf.λx.x) y) λf.λx.x) λx.λy.x)\n",
" 6: ---> (λs.((s λf.λx.x) λf.λx.x) λx.λy.x)\n",
" 7: ---> ((λx.λy.x λf.λx.x) λf.λx.x)\n",
" 8: ---> (λy.λf.λx.x λf.λx.x)\n",
" 9: ---> λf.λx.x\n",
"Forme normale calculée : λf.λx.x\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 92,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"PRED.applique(ZERO).forme_normale(verbose=True) == ZERO"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Une fois le prédesseur exprimé, il est facile de définir la soustraction comme une itération du prédécesseur."
]
},
{
"cell_type": "code",
"execution_count": 93,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λn.λm.((m PRED) n)\n",
"λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) n)\n"
]
}
],
"source": [
"M_SUB = Lambda_terme('!n.!m.((m PRED) n)')\n",
"print(M_SUB)\n",
"SUB = M_SUB.subs('PRED', PRED)\n",
"print(SUB)"
]
},
{
"cell_type": "code",
"execution_count": 94,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) n) λf.λx.(f (f (f x)))) λf.λx.(f x))\n",
" 1: ---> (λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) λf.λx.(f (f (f x)))) λf.λx.(f x))\n",
" 2: ---> ((λf.λx.(f x) λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) λf.λx.(f (f (f x))))\n",
" 3: ---> (λx.(λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) x) λf.λx.(f (f (f x))))\n",
" 4: ---> (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f (f (f x))))\n",
" 5: ---> (λc.(c λx.λy.x) ((λf.λx.(f (f (f x))) λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))\n",
" 6: ---> (((λf.λx.(f (f (f x))) λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
" 7: ---> ((λx.(λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) x))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
" 8: ---> ((λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) λx.λy.x)\n",
" 9: ---> (((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))) λx.λy.x)\n",
" 10: ---> ((λy.λs.((s (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))) λx.λy.x)\n",
" 11: ---> (λs.((s (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))) λx.λy.x)\n",
" 12: ---> ((λx.λy.x (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))))\n",
" 13: ---> (λy.(λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))))\n",
" 14: ---> (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))\n",
" 15: ---> ((λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λx.λy.y)\n",
" 16: ---> (((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) λx.λy.y)\n",
" 17: ---> ((λy.λs.((s (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) λx.λy.y)\n",
" 18: ---> (λs.((s (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))) λx.λy.y)\n",
" 19: ---> ((λx.λy.y (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))\n",
" 20: ---> (λy.y (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))))\n",
" 21: ---> (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))))\n",
" 22: ---> λf.λx.(f (((λc.(c λx.λy.y) (λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) f) x))\n",
" 23: ---> λf.λx.(f ((((λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)) λx.λy.y) f) x))\n",
" 24: ---> λf.λx.(f (((((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) λx.λy.y) f) x))\n",
" 25: ---> λf.λx.(f ((((λy.λs.((s (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) λx.λy.y) f) x))\n",
" 26: ---> λf.λx.(f (((λs.((s (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) λx.λy.y) f) x))\n",
" 27: ---> λf.λx.(f ((((λx.λy.y (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) f) x))\n",
" 28: ---> λf.λx.(f (((λy.y (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) f) x))\n",
" 29: ---> λf.λx.(f (((λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) f) x))\n",
" 30: ---> λf.λx.(f ((λf.λx.(f (((λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)) f) x)) f) x))\n",
" 31: ---> λf.λx.(f (λx.(f (((λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)) f) x)) x))\n",
" 32: ---> λf.λx.(f (f (((λc.(c λx.λy.y) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)) f) x)))\n",
" 33: ---> λf.λx.(f (f (((((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x) λx.λy.y) f) x)))\n",
" 34: ---> λf.λx.(f (f ((((λy.λs.((s λf.λx.x) y) λf.λx.x) λx.λy.y) f) x)))\n",
" 35: ---> λf.λx.(f (f (((λs.((s λf.λx.x) λf.λx.x) λx.λy.y) f) x)))\n",
" 36: ---> λf.λx.(f (f ((((λx.λy.y λf.λx.x) λf.λx.x) f) x)))\n",
" 37: ---> λf.λx.(f (f (((λy.y λf.λx.x) f) x)))\n",
" 38: ---> λf.λx.(f (f ((λf.λx.x f) x)))\n",
" 39: ---> λf.λx.(f (f (λx.x x)))\n",
" 40: ---> λf.λx.(f (f x))\n",
"Forme normale calculée : λf.λx.(f (f x))\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 94,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"SUB.applique(TROIS).applique(UN).forme_normale(verbose=True) == DEUX"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Infériorité, égalité"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Remarque** on a l'équivalence \n",
"$$ n <= m \\Longleftrightarrow ((\\mathtt{SUB}\\ \\lceil n\\rceil)\\ \\lceil m\\rceil) =_\\beta \\mathtt{ZERO}.$$"
]
},
{
"cell_type": "code",
"execution_count": 95,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 95,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"SUB.applique(TROIS).applique(QUATRE).forme_normale() == ZERO"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"De là vient l'idée de définir le $\\lambda$-terme\n",
"$$\\mathtt{INF} = \\lambda n.\\lambda m.(\\mathtt{NUL}\\ ((\\mathtt{SUB}\\ n)\\ m)),$$\n",
"qui est tel que pour tout couple d'entier $(n, m)$, on a\n",
"\n",
"* si $n \\leq m$\n",
" $$ ((\\mathtt{INF}\\ \\lceil n\\rceil)\\ \\lceil m\\rceil) =_\\beta \\mathtt{VRAI},$$\n",
"* et si $n > m$\n",
" $$ ((\\mathtt{INF}\\ \\lceil n\\rceil)\\ \\lceil m\\rceil) =_\\beta \\mathtt{FAUX}.$$"
]
},
{
"cell_type": "code",
"execution_count": 96,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λn.λm.(NUL ((SUB n) m))\n",
"λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) n) n) m))\n"
]
}
],
"source": [
"M_INF = Lambda_terme('!n.!m.(NUL ((SUB n) m))')\n",
"print(M_INF)\n",
"INF = M_INF.subs('NUL', NUL).subs('SUB', SUB)\n",
"print(INF)"
]
},
{
"cell_type": "code",
"execution_count": 97,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 97,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"INF.applique(TROIS).applique(UN).forme_normale() == FAUX"
]
},
{
"cell_type": "code",
"execution_count": 98,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 98,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"INF.applique(UN).applique(TROIS).forme_normale() == VRAI"
]
},
{
"cell_type": "code",
"execution_count": 99,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 99,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"INF.applique(UN).applique(UN).forme_normale() == VRAI"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Et à partir de $\\mathtt{INF}$ on peut définir le terme\n",
"$$ \\mathtt{EGAL} = \\lambda n.\\lambda m.((\\mathtt{ET}\\ ((\\mathtt{INF}\\ \\lceil n\\rceil)\\ \\lceil m\\rceil))\\ ((\\mathtt{INF}\\ \\lceil m\\rceil)\\ \\lceil n\\rceil)),$$\n",
"qui est tel que pour tout couple d'entier $(n, m)$, on a\n",
"\n",
"* si $n = m$\n",
" $$ ((\\mathtt{EGAL}\\ \\lceil n\\rceil)\\ \\lceil m\\rceil) =_\\beta \\mathtt{VRAI},$$\n",
"* et si $n \\neq m$\n",
" $$ ((\\mathtt{EGAL}\\ \\lceil n\\rceil)\\ \\lceil m\\rceil) =_\\beta \\mathtt{FAUX}.$$"
]
},
{
"cell_type": "code",
"execution_count": 100,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λn.λm.((ET ((INF n) m)) ((INF m) n))\n",
"λn.λm.((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) n) n) m)) n) m)) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n))\n"
]
}
],
"source": [
"M_EGAL = Lambda_terme('!n.!m.((ET ((INF n) m)) ((INF m) n))')\n",
"print(M_EGAL)\n",
"EGAL = M_EGAL.subs('ET', ET).subs('INF', INF)\n",
"print(EGAL)"
]
},
{
"cell_type": "code",
"execution_count": 101,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 101,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"EGAL.applique(UN).applique(UN).forme_normale() == VRAI"
]
},
{
"cell_type": "code",
"execution_count": 102,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 102,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"EGAL.applique(UN).applique(DEUX).forme_normale() == FAUX"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Listes de termes"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Classiquement, on peut considérer une liste de termes $ <M_1, M_2, \\ldots, M_n>$ comme un couple dont la première composante est l'élément en tête de la liste, et la seconde composante est la liste des éléments qui restent :\n",
"$$ <M_1, M_2, \\ldots, M_n> = [M_1, <M_2, \\ldots, M_n>].$$\n",
"Ainsi une liste de trois éléments est un emboîtement de trois couples :\n",
"\n",
"$$ <M_1, M_2, M_3> = [M_1, [M_2, [M3, <>]]],$$\n",
"la deuxième composante du couple le plus interne, $<>$ désignant la liste vide.\n",
"\n",
"On voit bien comment construire des listes ($\\mathtt{CONS}$), accéder à leur tête ($\\mathtt{CAR}$) et à leur reste ($\\mathtt{CDR}$).\n",
"\n",
"Il reste à trouver une représentation de la liste vide et un terme permettant de distinguer la liste vide de celles qui ne le sont pas. \n",
"\n",
"Et le problème de la vacuité d'une liste va imposer de mettre une couche d'abstraction supplémentaire sur notre représentation des listes."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Étant donnés $n$ $\\lambda$-termes $M_1$, $M_2$, ..., $M_n$, on peut représenter la liste de ces termes par le $\\lambda$-terme\n",
"\n",
"$$ <M_1, M_2, \\ldots, M_n> = \\lambda x.[M_1, [M_2, \\ldots[M_n, <>]\\ldots],$$\n",
"définition dans laquelle $<>$ désigne la liste vide qui peut être représentée par \n",
"$$ <> = \\lambda x.\\lambda s.x\\,\\, (= \\mathtt{FAUX}).$$"
]
},
{
"cell_type": "code",
"execution_count": 103,
"metadata": {},
"outputs": [],
"source": [
"LVIDE = Lambda_terme('!x.!s.x')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le terme $\\mathtt{LCONS}$ permettant d'ajouter un terme $t$ en tête d'une liste $r$ peut alors être facilement écrit de la manière suivante en utilisant $\\mathtt{CONS}$.\n",
"\n",
"$$ \\mathtt{LCONS} = \\lambda t.\\lambda r.\\lambda x.((\\mathtt{CONS}\\ t)\\ r).$$"
]
},
{
"cell_type": "code",
"execution_count": 104,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λt.λr.λx.((CONS t) r)\n",
"λt.λr.λx.((λx.λy.λs.((s x) y) t) r)\n"
]
}
],
"source": [
"M_LCONS = Lambda_terme('!t.!r.!x.((CONS t) r)')\n",
"print(M_LCONS)\n",
"LCONS = M_LCONS.subs('CONS', CONS)\n",
"print(LCONS)"
]
},
{
"cell_type": "code",
"execution_count": 105,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λx.λs.((s M1) λx.λs.((s M2) λx.λs.((s M3) λx.λs.x)))\n"
]
}
],
"source": [
"M1 = Lambda_terme('M1')\n",
"M2 = Lambda_terme('M2')\n",
"M3 = Lambda_terme('M3')\n",
"L = LCONS.applique(M1).applique(LCONS.applique(M2).applique(LCONS.applique(M3).applique(LVIDE)))\n",
"print(L.forme_normale())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Notons que si $L$ est une liste non vide, alors quelque soit le terme $M$, $(L\\ M)$ se réduit en un couple dont la seconde composante est la liste reste de $L$. En particulier, le terme $M$ a disparu."
]
},
{
"cell_type": "code",
"execution_count": 106,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λs.((s M1) λx.λs.((s M2) λx.λs.((s M3) λx.λs.x)))\n"
]
}
],
"source": [
"print(L.applique(Lambda_terme('M')).forme_normale())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Et dans le cas de la liste vide, $(\\mathtt{LVIDE}\\ M)$ se réduit en $\\lambda s.M$."
]
},
{
"cell_type": "code",
"execution_count": 107,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λs.M\n"
]
}
],
"source": [
"print(LVIDE.applique(Lambda_terme('M')).forme_normale())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Les deux remarques précédentes sont à la base de la définition des sélecteurs $\\mathtt{LCAR}$ et $\\mathtt{LCDR}$ présentés maintenant."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le sélecteur $\\mathtt{LCAR}$ permettant d'obtenir l'élément de tête d'une liste est construit en utilisant $\\mathtt{CAR}$.\n",
"\n",
"$$ \\mathtt{LCAR} = \\lambda l.(\\mathtt{CAR}\\ (l\\ \\mathtt{VRAI})).$$"
]
},
{
"cell_type": "code",
"execution_count": 108,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λl.(CAR (l VRAI))\n",
"λl.(λc.(c λx.λy.x) (l λx.λy.x))\n"
]
}
],
"source": [
"M_LCAR = Lambda_terme('!l.(CAR (l VRAI))')\n",
"print(M_LCAR)\n",
"L_CAR = M_LCAR.subs('CAR', CAR).subs('VRAI', VRAI)\n",
"print(L_CAR)"
]
},
{
"cell_type": "code",
"execution_count": 109,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λl.(λc.(c λx.λy.x) (l λx.λy.x)) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))))\n",
" 1: ---> (λc.(c λx.λy.x) (((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.x))\n",
" 2: ---> ((((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.x) λx.λy.x)\n",
" 3: ---> (((λr.λx.((λx.λy.λs.((s x) y) M1) r) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.x) λx.λy.x)\n",
" 4: ---> ((λx.((λx.λy.λs.((s x) y) M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.x) λx.λy.x)\n",
" 5: ---> (((λx.λy.λs.((s x) y) M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.x)\n",
" 6: ---> ((λy.λs.((s M1) y) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.x)\n",
" 7: ---> (λs.((s M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.x)\n",
" 8: ---> ((λx.λy.x M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x)))\n",
" 9: ---> (λy.M1 ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x)))\n",
" 10: ---> M1\n",
"Forme normale calculée : M1\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 109,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"L_CAR.applique(L).forme_normale(verbose=True) == Lambda_terme('M1')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Notons que \n",
"$$(\\mathtt{LCAR}\\ \\mathtt{LVIDE}) \\twoheadrightarrow_\\beta \\mathtt{LVIDE}.$$ "
]
},
{
"cell_type": "code",
"execution_count": 110,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λl.(λc.(c λx.λy.x) (l λx.λy.x)) λx.λs.x)\n",
" 1: ---> (λc.(c λx.λy.x) (λx.λs.x λx.λy.x))\n",
" 2: ---> ((λx.λs.x λx.λy.x) λx.λy.x)\n",
" 3: ---> (λs.λx.λy.x λx.λy.x)\n",
" 4: ---> λx.λy.x\n",
"Forme normale calculée : λx.λy.x\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 110,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"L_CAR.applique(LVIDE).forme_normale(verbose=True) == LVIDE"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le sélecteur $\\mathtt{LCDR}$ permettant d'obtenir le reste d'une liste se définit à l'aide de $\\mathtt{CDR}$.\n",
"\n",
"$$ CDR = \\lambda l.(\\mathtt{CDR}\\ (l\\ \\mathtt{VRAI})).$$"
]
},
{
"cell_type": "code",
"execution_count": 111,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λl.(CDR (l VRAI))\n",
"λl.(λc.(c λx.λy.y) (l λx.λy.x))\n"
]
}
],
"source": [
"M_LCDR = Lambda_terme('!l.(CDR (l VRAI))')\n",
"print(M_LCDR)\n",
"LCDR = M_LCDR.subs('CDR', CDR).subs('VRAI', VRAI)\n",
"print(LCDR)"
]
},
{
"cell_type": "code",
"execution_count": 112,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λl.(λc.(c λx.λy.y) (l λx.λy.x)) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))))\n",
" 1: ---> (λc.(c λx.λy.y) (((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.x))\n",
" 2: ---> ((((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.x) λx.λy.y)\n",
" 3: ---> (((λr.λx.((λx.λy.λs.((s x) y) M1) r) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.x) λx.λy.y)\n",
" 4: ---> ((λx.((λx.λy.λs.((s x) y) M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.x) λx.λy.y)\n",
" 5: ---> (((λx.λy.λs.((s x) y) M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.y)\n",
" 6: ---> ((λy.λs.((s M1) y) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.y)\n",
" 7: ---> (λs.((s M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.y)\n",
" 8: ---> ((λx.λy.y M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x)))\n",
" 9: ---> (λy.y ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x)))\n",
" 10: ---> ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))\n",
" 11: ---> (λr.λx.((λx.λy.λs.((s x) y) M2) r) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))\n",
" 12: ---> λx.((λx.λy.λs.((s x) y) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))\n",
" 13: ---> λx.(λy.λs.((s M2) y) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))\n",
" 14: ---> λx.λs.((s M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))\n",
" 15: ---> λx.λs.((s M2) (λr.λx.((λx.λy.λs.((s x) y) M3) r) λx.λs.x))\n",
" 16: ---> λx.λs.((s M2) λx.((λx.λy.λs.((s x) y) M3) λx.λs.x))\n",
" 17: ---> λx.λs.((s M2) λx.(λy.λs.((s M3) y) λx.λs.x))\n",
" 18: ---> λx.λs.((s M2) λx.λs.((s M3) λx.λs.x))\n",
"Forme normale calculée : λx.λs.((s M2) λx.λs.((s M3) λx.λs.x))\n"
]
},
{
"data": {
"text/plain": [
"<lambda_calcul.Lambda_terme at 0x7f71cc309a20>"
]
},
"execution_count": 112,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"LCDR.applique(L).forme_normale(verbose=True)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Notons que \n",
"$$(\\mathtt{LCDR}\\ \\mathtt{LVIDE}) \\twoheadrightarrow_\\beta \\mathtt{LVIDE}.$$ "
]
},
{
"cell_type": "code",
"execution_count": 113,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λl.(λc.(c λx.λy.y) (l λx.λy.x)) λx.λs.x)\n",
" 1: ---> (λc.(c λx.λy.y) (λx.λs.x λx.λy.x))\n",
" 2: ---> ((λx.λs.x λx.λy.x) λx.λy.y)\n",
" 3: ---> (λs.λx.λy.x λx.λy.y)\n",
" 4: ---> λx.λy.x\n",
"Forme normale calculée : λx.λy.x\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 113,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"LCDR.applique(LVIDE).forme_normale(verbose=True) == LVIDE"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le terme qui permet de distinguer une liste vide d'une liste qui ne l'est pas est\n",
"\n",
"$$ \\mathtt{LESTVIDE} = \\lambda l.((l\\ \\mathtt{VRAI})\\ \\lambda t.\\lambda r.\\mathtt{FAUX}).$$"
]
},
{
"cell_type": "code",
"execution_count": 114,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λl.((l VRAI) λt.λr.FAUX)\n"
]
}
],
"source": [
"M_LESTVIDE = Lambda_terme('!l.((l VRAI) !t.!r.FAUX)')\n",
"print(M_LESTVIDE)\n",
"LESTVIDE = M_LESTVIDE.subs('VRAI', VRAI).subs('FAUX', FAUX)"
]
},
{
"cell_type": "code",
"execution_count": 115,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λl.((l λx.λy.x) λt.λr.λx.λy.y) λx.λs.x)\n",
" 1: ---> ((λx.λs.x λx.λy.x) λt.λr.λx.λy.y)\n",
" 2: ---> (λs.λx.λy.x λt.λr.λx.λy.y)\n",
" 3: ---> λx.λy.x\n",
"Forme normale calculée : λx.λy.x\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 115,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"LESTVIDE.applique(LVIDE).forme_normale(verbose=True) == VRAI"
]
},
{
"cell_type": "code",
"execution_count": 116,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λl.((l λx.λy.x) λt.λr.λx.λy.y) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))))\n",
" 1: ---> ((((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.x) λt.λr.λx.λy.y)\n",
" 2: ---> (((λr.λx.((λx.λy.λs.((s x) y) M1) r) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.x) λt.λr.λx.λy.y)\n",
" 3: ---> ((λx.((λx.λy.λs.((s x) y) M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λx.λy.x) λt.λr.λx.λy.y)\n",
" 4: ---> (((λx.λy.λs.((s x) y) M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λt.λr.λx.λy.y)\n",
" 5: ---> ((λy.λs.((s M1) y) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λt.λr.λx.λy.y)\n",
" 6: ---> (λs.((s M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x))) λt.λr.λx.λy.y)\n",
" 7: ---> ((λt.λr.λx.λy.y M1) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x)))\n",
" 8: ---> (λr.λx.λy.y ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M2) ((λt.λr.λx.((λx.λy.λs.((s x) y) t) r) M3) λx.λs.x)))\n",
" 9: ---> λx.λy.y\n",
"Forme normale calculée : λx.λy.y\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 116,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"LESTVIDE.applique(L).forme_normale(verbose=True) == FAUX"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Itération"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On l'a vu à plusieurs occasions ($\\mathtt{ADD}$, $\\mathtt{MUL}$, $\\mathtt{EXP}$, $\\mathtt{NUL}$, $\\mathtt{SUB}$), les numéraux de Church permettent d'itérer l'application d'un terme."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Étudions encore un cas d'école avec la classique fonction factorielle qui peut se programmer en Python à l'aide d'une boucle `for`.\n",
"\n",
"~~~python\n",
"def fact(n):\n",
" f = 1\n",
" for i in range(n+1):\n",
" f = f*i\n",
" return f\n",
"~~~"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Ce programme utilise deux variables $\\mathtt{i}$ et $\\mathtt{f}$.\n",
"\n",
"Si on ajoute la valeur fictive 0 pour la variable $\\mathtt{i}$ avant la boucle `for`, le couple ($\\mathtt{i}$, $\\mathtt{f}$) prend les valeurs successives : (0, 1), (1, 1), (2, 2), (3, 6), ..., ($n$, $n!$). Ainsi à chaque étape de l'itération le couple est transformé selon la règle :\n",
"\n",
"$$ (i, f) \\rightarrow (i+1, f\\times i).$$\n",
"\n",
"C'est cette règle qui est itérée $n$ fois. Et cette règle peut être représentée par un $\\lambda$-terme transformant un couple $[\\lceil i\\rceil, \\lceil f\\rceil]$ en le couple $[\\lceil i+1\\rceil, \\lceil f\\times i\\rceil]$."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Ce qui peut être fait par \n",
"\n",
"$$ \\mathtt{FACT} = \\lambda n.(CDR\\ ((n\\ \\lambda c.[(SUC\\ (CAR\\ c)), ((MUL\\ (CAR\\ c))\\ (CDR\\ c))])\\ [ZERO, ZERO])).$$"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Voici une réalisation de ce terme (que nous nommons $\\mathtt{FACTv1}$ puisque d'autre réalisations de $\\mathtt{}$ seront envisagées dans la suite)."
]
},
{
"cell_type": "code",
"execution_count": 117,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λn.(CDR ((n λc.((CONS (SUC (CAR c))) ((MUL (SUC (CAR c))) (CDR c)))) ((CONS ZERO) UN)))\n",
"λn.(λc.(c λx.λy.y) ((n λc.((λx.λy.λs.((s x) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.x) c))) ((λn.λm.λf.(n (m f)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.x) c))) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.(f x))))\n"
]
}
],
"source": [
"M_FACTv1 = Lambda_terme('!n.(CDR ((n !c.((CONS (SUC (CAR c))) ((MUL (SUC (CAR c))) (CDR c)))) ((CONS ZERO) UN)))')\n",
"print(M_FACTv1)\n",
"FACTv1 = M_FACTv1.subs('CONS', CONS).subs('CAR', CAR).subs('CDR', CDR).subs('SUC', SUC).subs('MUL', MUL).subs('UN', UN).subs('ZERO', ZERO)\n",
"print(FACTv1)"
]
},
{
"cell_type": "code",
"execution_count": 118,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 118,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv1.applique(ZERO).forme_normale() == UN"
]
},
{
"cell_type": "code",
"execution_count": 119,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 119,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv1.applique(UN).forme_normale() == UN"
]
},
{
"cell_type": "code",
"execution_count": 120,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 120,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv1.applique(DEUX).forme_normale() == DEUX"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Pour calculer $(\\mathtt{FACTv1}\\ \\mathtt{TROIS})$, il faut au moins 309 étapes de réduction."
]
},
{
"cell_type": "code",
"execution_count": 121,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 121,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv1.applique(TROIS).forme_normale(nb_etapes_max=309) == SIX"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Et pour (𝙵𝙰𝙲𝚃𝚟𝟷 QUATRE), il en faut au moins 1284."
]
},
{
"cell_type": "code",
"execution_count": 122,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 122,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv1.applique(QUATRE).forme_normale(nb_etapes_max=1284) == MUL.applique(QUATRE).applique(SIX).forme_normale()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"En suivant le principe qui a conduit à écrire le terme $\\mathtt{FACTv1}$, on comprend que n'importe quelle fonction qui peut être programmée (en Python, ou tout autre langage) peut être représentée par un $\\lambda$-terme."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Et la récursivité ? Et les boucles `while` ? "
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Dernier point de notre exploration du pouvoir d'expression du $\\lambda$-calcul qui achèvera (peut-être) de nous convaincre que c'est un langage de programmation : peut-on représenter des fonctions récursives ? peut-on représenter des fonctions dont l'algorithme nécessite une boucle `while` ?"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Exprimer la récursivité sans nom ?"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Prenons encore la fonction factorielle comme exemple classique de fonction récursive. En Python on peut l'écrire de la façon suivante\n",
"\n",
"~~~python\n",
"def fact(n):\n",
" if n == 0:\n",
" return 1\n",
" else:\n",
" return n * fact(n - 1)\n",
"~~~"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"En examinant le code de cette version récursive de la fonction factorielle, on s'aperçoit que nous disposons de tous les ingrédients pour écrire un $\\lambda$-terme analogue. Le voici :\n",
"\n",
"$$ \\mathtt{FACT} = \\lambda n.(((\\mathtt{IF}\\ (\\mathtt{NUL}\\ n))\\ \\lceil 1\\rceil)\\ ((\\mathtt{MUL}\\ n)\\ (\\mathtt{FACT}\\ (\\mathtt{PRED}\\ n)))).$$\n",
"\n",
"\n",
"Hmmm ... Trop facile ! Il y a un hic !\n",
"Ce terme n'est pas valide car dans le terme désigné par le nom $\\mathtt{FACT}$, il y a le nom $\\mathtt{FACT}$, et en $\\lambda$-calcul les seuls noms intervenants dans les $\\lambda$-termes sont les variables. Donc le nom $\\mathtt{FACT}$ dans le $\\lambda$-terme ci-dessus est juste une variable et n'est pas le $\\lambda$-terme nommé $\\mathtt{FACT}$. "
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"En programmation on dit souvent d'une fonction qu'elle est récursive lorsqu'elle fait appel à elle-même, comme le fait la fonction `fact` ci-dessus. Et l'appel à une fonction se fait par le nom de cette fonction.\n",
"\n",
"Comme en $\\lambda$-calcul, il n'y a pas de nom, il semble, en apparence, que la définition de $\\lambda$-termes suivant un schéma récursif soit impossible.\n",
"\n",
"On va voir qu'il n'en est rien."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Avec une couche d'abstraction supplémentaire"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Dans l'essai de $\\lambda$-terme pour définir $\\mathtt{FACT}$, remplaçons le nom $\\mathtt{}$ par une variable, $f$ par exemple, et ajoutons une couche d'abstraction sur cette variable afin qu'elle soit liée. Nous obtenons un terme que nous nommerons $\\Phi_{fact}$.\n",
"\n",
"$$ \\Phi_{fact} = \\lambda f.\\lambda n.(((\\mathtt{IF}\\ (\\mathtt{NUL}\\ n))\\ \\lceil 1\\rceil)\\ ((\\mathtt{MUL}\\ n)\\ (f\\ (\\mathtt{PRED}\\ n)))).$$\n",
"\n",
"Ce $\\lambda$-terme est parfaitement valide. \n",
"\n",
"Mais, compte-tenu de la couche d'abstraction supplémentaire, ce n'est certainement pas un terme candidat pour être le terme $\\mathtt{FACT}$ que nous recherchons."
]
},
{
"cell_type": "code",
"execution_count": 123,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λf.λn.(((IF (NUL n)) UN) ((MUL n) (f (PRED n))))\n",
"λf.λn.(((λc.λa.λs.((c a) s) (λn.((n λx.λx.λy.y) λx.λy.x) n)) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) n) (f (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) n))))\n"
]
}
],
"source": [
"M_PHI_FACT = Lambda_terme('!f.!n.(((IF (NUL n)) UN) ((MUL n) (f (PRED n))))')\n",
"print(M_PHI_FACT)\n",
"PHI_FACT = M_PHI_FACT.subs('IF', IF).subs('NUL', NUL).subs('UN', UN).subs('MUL', MUL).subs('PRED', PRED)\n",
"print(PHI_FACT)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"En fait pour envisager d'utiliser ce terme pour calculer des factorielles, il faut d'abord l'appliquer à un terme (une fonction) $f$ puis appliquer à un entier (de Church). Autrement dit suivre le schéma\n",
"\n",
"$$((\\Phi_{fact}\\ f)\\ \\lceil n\\rceil).$$\n",
"\n",
"Mais quel terme (ou fonction) $f$ utiliser ?"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Et si on commençait par une fonction (un peu bizarre) nulle part définie, ou dit en termes plus $\\lambda$-calculesque, par un terme dont aucune application ne possède une forme normale :\n",
"\n",
"$$ \\mathtt{BOTTOM} = \\lambda y.\\Omega,$$\n",
"où, pour rappel, $\\Omega = (\\lambda x.(x\\ x)\\ \\lambda x.(x\\ x))$ qui, comme on l'a vu, n'est pas normalisable. \n",
"\n",
"Il est clair que pour n'importe quel terme $M$, on a\n",
"\n",
"$$(\\mathtt{BOTTOM}\\ M) \\rightarrow_\\beta\\Omega\\rightarrow_\\beta\\Omega\\rightarrow_\\beta\\ldots.$$"
]
},
{
"cell_type": "code",
"execution_count": 124,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λy.(λx.(x x) λx.(x x))\n"
]
}
],
"source": [
"BOTTOM = Lambda_terme('!y.OMEGA').subs('OMEGA', OMEGA)\n",
"print(BOTTOM)"
]
},
{
"cell_type": "code",
"execution_count": 125,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λy.(λx.(x x) λx.(x x)) M)\n",
" 1: ---> (λx.(x x) λx.(x x))\n",
" 2: ---> (λx.(x x) λx.(x x))\n",
" 3: ---> (λx.(x x) λx.(x x))\n",
"Pas de forme normale atteinte après 3 étapes de réduction\n"
]
}
],
"source": [
"BOTTOM.applique(Lambda_terme('M')).forme_normale(verbose=True, nb_etapes_max=3)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Appliquons notre terme $\\Phi_{fact}$ à $\\mathtt{BOTTOM}$,"
]
},
{
"cell_type": "code",
"execution_count": 126,
"metadata": {},
"outputs": [],
"source": [
"F1 = PHI_FACT.applique(BOTTOM)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"et appliquons ensuite le terme obtenu à des entiers de Church."
]
},
{
"cell_type": "code",
"execution_count": 127,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 127,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"F1.applique(ZERO).forme_normale() == UN"
]
},
{
"cell_type": "code",
"execution_count": 128,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λf.λn.(((λc.λa.λs.((c a) s) (λn.((n λx.λx.λy.y) λx.λy.x) n)) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) n) (f (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) n)))) λy.(λx.(x x) λx.(x x))) λf.λx.(f x))\n",
" 1: ---> (λn.(((λc.λa.λs.((c a) s) (λn.((n λx.λx.λy.y) λx.λy.x) n)) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) n) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) n)))) λf.λx.(f x))\n",
" 2: ---> (((λc.λa.λs.((c a) s) (λn.((n λx.λx.λy.y) λx.λy.x) λf.λx.(f x))) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
" 3: ---> ((λa.λs.(((λn.((n λx.λx.λy.y) λx.λy.x) λf.λx.(f x)) a) s) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
" 4: ---> (λs.(((λn.((n λx.λx.λy.y) λx.λy.x) λf.λx.(f x)) λf.λx.(f x)) s) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
" 5: ---> (((λn.((n λx.λx.λy.y) λx.λy.x) λf.λx.(f x)) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
" 6: ---> ((((λf.λx.(f x) λx.λx.λy.y) λx.λy.x) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
" 7: ---> (((λx.(λx.λx.λy.y x) λx.λy.x) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
" 8: ---> (((λx.λx.λy.y λx.λy.x) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
" 9: ---> ((λx.λy.y λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
" 10: ---> (λy.y ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
" 11: ---> ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x))))\n",
" 12: ---> (λm.λf.(λf.λx.(f x) (m f)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x))))\n",
" 13: ---> λf.(λf.λx.(f x) ((λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x))) f))\n",
" 14: ---> λf.λx.(((λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x))) f) x)\n",
" 15: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
" 16: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
" 17: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
" 18: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
" 19: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
" 20: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
"Pas de forme normale atteinte après 20 étapes de réduction\n"
]
}
],
"source": [
"F1.applique(UN).forme_normale(verbose=True, nb_etapes_max=20) "
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le terme $F_1$ appliqué à $\\lceil 0\\rceil$ donne $\\lceil 1\\rceil$. Mais, l'application à tout autre entier de Church n'est pas normalisable.\n",
"\n",
"Autrement dit la fonction représentée par $F_1$ calcule bien $0! = 1$, ... et c'est tout. C'est tout de même mieux que $\\mathtt{BOTTOM}$ !\n",
"\n",
"Continuons et définissons $F_2 = (\\Phi_{fact}\\ F_1)$."
]
},
{
"cell_type": "code",
"execution_count": 129,
"metadata": {},
"outputs": [],
"source": [
"F2 = PHI_FACT.applique(F1)"
]
},
{
"cell_type": "code",
"execution_count": 130,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 130,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"F2.applique(ZERO).forme_normale() == UN"
]
},
{
"cell_type": "code",
"execution_count": 131,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 131,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"F2.applique(UN).forme_normale() == UN"
]
},
{
"cell_type": "code",
"execution_count": 132,
"metadata": {},
"outputs": [],
"source": [
"F2.applique(DEUX).forme_normale()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le terme $F_2$ appliqué à $\\lceil n\\rceil$, avec $n=0\\mbox{ ou }1$ donne bien $\\lceil n!\\rceil$. Mais pour tout autre entier l'application n'est pas normalisable. On progresse.\n",
"\n",
"En fait si on définit la suite de termes $F_n$ par récurrence en posant\n",
"\n",
"\\begin{align}\n",
" F_0 &= \\mathtt{BOTTOM}\\\\\n",
" F_1 &= (\\Phi_{fact}\\ F_0)\\\\\n",
" F_2 &= (\\Phi_{fact}\\ F_1)\\\\\n",
" \\vdots\\\\\n",
" F_{n+1} &= (\\Phi_{fact}\\ F_n)\n",
"\\end{align}\n",
"chacun des termes de cette suite est en mesure de représenter une fonction factorielle partielle. Plus précisément, pour chaque entier $n$ on a\n",
"\n",
"$$ (F_n\\ \\lceil k\\rceil) \\twoheadrightarrow_\\beta \\lceil k!\\rceil \\mbox{ si } 0\\leq k < n,$$\n",
"et $(F_n\\ \\lceil k\\rceil)$ n'est pas normalisable si $k\\geq n$."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Vérifions cela sur le terme $F_4$."
]
},
{
"cell_type": "code",
"execution_count": 133,
"metadata": {},
"outputs": [],
"source": [
"F4 = QUATRE.applique(PHI_FACT).applique(BOTTOM)"
]
},
{
"cell_type": "code",
"execution_count": 134,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 134,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"F4.applique(ZERO).forme_normale() == UN"
]
},
{
"cell_type": "code",
"execution_count": 135,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 135,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"F4.applique(UN).forme_normale() == UN"
]
},
{
"cell_type": "code",
"execution_count": 136,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 136,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"F4.applique(DEUX).forme_normale(nb_etapes_max=244) == DEUX"
]
},
{
"cell_type": "code",
"execution_count": 137,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 137,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"F4.applique(TROIS).forme_normale(nb_etapes_max=1510) == SIX"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Avec le terme $\\Phi_{fact}$, nous sommes en mesure de définir des fonctions « approximant » de mieux en mieux la fonction factorielle, mais le procédé itératif décrit ne permet pas d'obtenir le terme $\\mathtt{FACT}$ voulu.\n",
"\n",
"Remarquons néanmoins que si nous avons ce terme $\\mathtt{FACT}$, alors on a\n",
"\n",
"$$ (\\Phi_{fact}\\ \\mathtt{FACT}) \\rightarrow_\\beta\n",
" \\lambda n.(((\\mathtt{IF}\\ (\\mathtt{NUL}\\ n))\\ \\lceil 1\\rceil)\\ ((\\mathtt{MUL}\\ n)\\ (\\mathtt{FACT}\\ (\\mathtt{PRED}\\ n)))),$$\n",
"qui est un terme correspondant exactement à ce que nous recherchons depuis le début. De cette réduction, on peut déduire que\n",
"$$ (\\Phi_{fact}\\ \\mathtt{FACT}) =_\\beta \\mathtt{FACT},$$\n",
"et cette équivalence montre que le terme $\\mathtt{FACT}$ que l'on recherche est un point fixe du terme $\\Phi_{fact}$. Or on a vu comment construire un terme point fixe d'un autre. \n",
"\n",
"$$\\mathtt{FACT} = (\\lambda x.(\\Phi_{fact}\\ (x\\ x))\\ \\lambda x.(\\Phi_{fact}\\ (x\\ x))).$$\n",
"Ce terme est un $\\lambda$-terme valide qui vérifie pour tout entier $n\\geq 0$\n",
"$$(\\mathtt{FACT}\\ \\lceil n\\rceil) =_\\beta \\lceil n!\\rceil.$$"
]
},
{
"cell_type": "code",
"execution_count": 138,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λx.(λf.λn.(((λc.λa.λs.((c a) s) (λn.((n λx.λx.λy.y) λx.λy.x) n)) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) n) (f (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) n)))) (x x)) λx.(λf.λn.(((λc.λa.λs.((c a) s) (λn.((n λx.λx.λy.y) λx.λy.x) n)) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) n) (f (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x))) n)))) (x x)))\n"
]
}
],
"source": [
"W = Lambda_terme('!x.(PHIFACT (x x))').subs('PHIFACT', PHI_FACT)\n",
"FACTv2 = Lambda_terme('(W W)').subs('W', W)\n",
"print(FACTv2)"
]
},
{
"cell_type": "code",
"execution_count": 139,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 139,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv2.applique(ZERO).forme_normale() == UN"
]
},
{
"cell_type": "code",
"execution_count": 140,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 140,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv2.applique(UN).forme_normale() == UN"
]
},
{
"cell_type": "code",
"execution_count": 141,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 141,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv2.applique(DEUX).forme_normale(nb_etapes_max=247) == DEUX"
]
},
{
"cell_type": "code",
"execution_count": 142,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 142,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv2.applique(TROIS).forme_normale(nb_etapes_max=1524) == SIX"
]
},
{
"cell_type": "code",
"execution_count": 143,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 143,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv2.applique(QUATRE).forme_normale(nb_etapes_max=10383) == int_en_church(24)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Combinateur de point fixe"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Le combinateur de point fixe de Curry est défini par\n",
"\n",
"$$ Y = \\lambda f.(\\lambda x.(f\\ (x\\ x))\\ \\lambda x.(f\\ (x\\ x))).$$\n",
"\n",
"Il permet de construire un terme point fixe de n'importe quel terme $\\Phi$, ce terme se définissant par $F = (Y\\ \\Phi).$. En effet,\n",
"\n",
"$$ F = (Y\\ \\Phi) \\rightarrow_\\beta (\\lambda x.(\\Phi\\ (x\\ x))\\ \\lambda x.(\\Phi\\ (x\\ x)) \\rightarrow_\\beta\n",
" (\\Phi\\ (\\lambda x.(\\Phi\\ (x\\ x)\\ \\lambda x.(\\Phi\\ (x\\ x))),$$\n",
"et\n",
"$$ (\\Phi\\ F) = (\\Phi\\ (Y\\ \\Phi)) \\rightarrow_\\beta\n",
" (\\Phi\\ (\\lambda x.(\\Phi\\ (x\\ x)\\ \\lambda x.(\\Phi\\ (x\\ x))),$$\n",
"ce qui permet de conclure que\n",
"$$ F =_\\beta (\\Phi\\ F).$$"
]
},
{
"cell_type": "code",
"execution_count": 144,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λf.(λx.(f (x x)) λx.(f (x x)))\n"
]
}
],
"source": [
"Y = Lambda_terme('!f.(!x.(f (x x)) !x.(f (x x)))')\n",
"print(Y)"
]
},
{
"cell_type": "code",
"execution_count": 145,
"metadata": {},
"outputs": [],
"source": [
"FACTv3 = Y.applique(PHI_FACT)"
]
},
{
"cell_type": "code",
"execution_count": 146,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 146,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv3.applique(ZERO).forme_normale() == UN"
]
},
{
"cell_type": "code",
"execution_count": 147,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 147,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv3.applique(UN).forme_normale() == UN"
]
},
{
"cell_type": "code",
"execution_count": 148,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 148,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv3.applique(DEUX).forme_normale(nb_etapes_max=248) == DEUX"
]
},
{
"cell_type": "code",
"execution_count": 149,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 149,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv3.applique(TROIS).forme_normale(nb_etapes_max=1525) == SIX"
]
},
{
"cell_type": "code",
"execution_count": 150,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 150,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv3.applique(QUATRE).forme_normale(nb_etapes_max=10384) == int_en_church(24)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Remarque** $Y$ n'est pas normalisable, et quelque soit le $\\lambda$-terme $M$, $(Y\\ M)$ ne l'est pas. Pourtant ces derniers termes peuvent s'avérer utiles. "
]
},
{
"cell_type": "code",
"execution_count": 151,
"metadata": {},
"outputs": [],
"source": [
"PF = Y.applique(Lambda_terme('M'))"
]
},
{
"cell_type": "code",
"execution_count": 152,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λf.(λx.(f (x x)) λx.(f (x x))) M)\n",
" 1: ---> (λx.(M (x x)) λx.(M (x x)))\n",
" 2: ---> (M (λx.(M (x x)) λx.(M (x x))))\n",
" 3: ---> (M (M (λx.(M (x x)) λx.(M (x x)))))\n",
" 4: ---> (M (M (M (λx.(M (x x)) λx.(M (x x))))))\n",
" 5: ---> (M (M (M (M (λx.(M (x x)) λx.(M (x x)))))))\n",
" 6: ---> (M (M (M (M (M (λx.(M (x x)) λx.(M (x x))))))))\n",
" 7: ---> (M (M (M (M (M (M (λx.(M (x x)) λx.(M (x x)))))))))\n",
" 8: ---> (M (M (M (M (M (M (M (λx.(M (x x)) λx.(M (x x))))))))))\n",
" 9: ---> (M (M (M (M (M (M (M (M (λx.(M (x x)) λx.(M (x x)))))))))))\n",
" 10: ---> (M (M (M (M (M (M (M (M (M (λx.(M (x x)) λx.(M (x x))))))))))))\n",
"Pas de forme normale atteinte après 10 étapes de réduction\n"
]
}
],
"source": [
"PF.forme_normale(verbose=True, nb_etapes_max=10)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Un autre combinateur de point fixe"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Voici un autre combinateur de point fixe, dû à Turing.\n",
"\n",
"$$\\Theta = (\\lambda x.\\lambda y.(y\\ ((x\\ x)\\ y))\\ \\lambda x.\\lambda y.(y\\ ((x\\ x)\\ y))).$$"
]
},
{
"cell_type": "code",
"execution_count": 153,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λx.λy.(y ((x x) y)) λx.λy.(y ((x x) y)))\n"
]
}
],
"source": [
"THETA = Lambda_terme('(!x.!y.(y ((x x) y)) !x.!y.(y ((x x) y)))')\n",
"print(THETA)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Ce combinateur est un redex, et c'est le seul redex parmi ses sous-termes.une étape de réduction donne\n",
"\n",
"$$ \\Theta \\rightarrow_\\beta \\lambda y.(y\\ (\\Theta\\ y)).$$\n",
"\n",
"Par conséquent, en réduisant le redex le plus à gauche, en deux étapes on obtient\n",
"$$ (\\Theta\\ \\Phi) \\rightarrow_\\beta (\\lambda y.(y\\ (\\Theta\\ y))\\ \\Phi) \\rightarrow_\\beta\n",
" (\\Phi\\ (\\Theta\\ \\Phi)).$$\n",
"Ce qui établit que $\\Theta$ est bien un combinateur de point fixe, mais aussi que contrairement à $Y$\n",
"$$ (\\Theta\\ \\Phi) \\twoheadrightarrow_\\beta (\\Phi\\ (\\Theta\\ \\Phi)).$$"
]
},
{
"cell_type": "code",
"execution_count": 154,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λy.(y ((λx.λy.(y ((x x) y)) λx.λy.(y ((x x) y))) y))\n"
]
}
],
"source": [
"red_theta, _ = THETA.reduit()\n",
"print(red_theta)"
]
},
{
"cell_type": "code",
"execution_count": 155,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"((λx.λy.(y ((x x) y)) λx.λy.(y ((x x) y))) PHI)\n",
" 1: ---> (λy.(y ((λx.λy.(y ((x x) y)) λx.λy.(y ((x x) y))) y)) PHI)\n",
" 2: ---> (PHI ((λx.λy.(y ((x x) y)) λx.λy.(y ((x x) y))) PHI))\n",
"Pas de forme normale atteinte après 2 étapes de réduction\n"
]
}
],
"source": [
"THETA.applique(Lambda_terme('PHI')).forme_normale(verbose=True, nb_etapes_max=2)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Utilisons $\\Theta$ pour définir une quatrième version de $\\mathtt{FACT}$. "
]
},
{
"cell_type": "code",
"execution_count": 156,
"metadata": {},
"outputs": [],
"source": [
"FACTv4 = THETA.applique(PHI_FACT)"
]
},
{
"cell_type": "code",
"execution_count": 157,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 157,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv4.applique(ZERO).forme_normale() == UN"
]
},
{
"cell_type": "code",
"execution_count": 158,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 158,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv4.applique(UN).forme_normale() == UN"
]
},
{
"cell_type": "code",
"execution_count": 159,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 159,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv4.applique(DEUX).forme_normale(nb_etapes_max=252) == DEUX"
]
},
{
"cell_type": "code",
"execution_count": 160,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 160,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv4.applique(TROIS).forme_normale(nb_etapes_max=1540) == SIX"
]
},
{
"cell_type": "code",
"execution_count": 161,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 161,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"FACTv4.applique(QUATRE).forme_normale(nb_etapes_max=10448) == int_en_church(24)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Au titre d'un autre exemple, envisageons maintenant d'établir un $\\lambda$-terme qui permet de calculer la longueur d'une liste.\n",
"\n",
"La longueur d'une liste s'exprime récursivement par\n",
"\n",
"\\begin{align}\n",
" \\mbox{long(<>)} &= 0\\\\\n",
" \\mbox{long(<x,L>)} &= 1 + \\mbox{long(L)}.\n",
"\\end{align}\n",
"\n",
"Avec une couche d'abstraction supplémentaire nous définissons le terme\n",
"\n",
"$$\\Phi_{long} = \\lambda f.\\lambda l.(((\\mathtt{IF}\\ (\\mathtt{LESTVIDE}\\ l))\\ \\mathtt{ZERO})\\ (\\mathtt{SUC}\\ (f\\ (\\mathtt{LCDR}\\ l)))).$$"
]
},
{
"cell_type": "code",
"execution_count": 162,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λf.λl.(((IF (LESTVIDE l)) ZERO) (SUC (f (LCDR l))))\n"
]
}
],
"source": [
"M_PHI_LONG = Lambda_terme('!f.!l.(((IF (LESTVIDE l)) ZERO)(SUC (f (LCDR l))))')\n",
"print(M_PHI_LONG)\n",
"PHI_LONG = M_PHI_LONG.subs('IF', IF).subs('LESTVIDE', LESTVIDE).subs('ZERO', ZERO).subs('SUC', SUC).subs('LCDR', LCDR)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Définissions le terme $\\mathtt{LONG}$ à l'aide de l'un ou l'autre de nos deux combinateurs de point fixe.\n",
"\n",
"$$ \\mathtt{LONG} = (\\Theta\\ \\Phi_{long}).$$"
]
},
{
"cell_type": "code",
"execution_count": 163,
"metadata": {},
"outputs": [],
"source": [
"LONG = THETA.applique(PHI_LONG)"
]
},
{
"cell_type": "code",
"execution_count": 164,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 164,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"LONG.applique(LVIDE).forme_normale() == ZERO"
]
},
{
"cell_type": "code",
"execution_count": 165,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 165,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"M1 = Lambda_terme('M1')\n",
"M2 = Lambda_terme('M2')\n",
"M3 = Lambda_terme('M3')\n",
"L = LCONS.applique(M1).applique(LCONS.applique(M2).applique(LCONS.applique(M3).applique(LVIDE)))\n",
"LONG.applique(L).forme_normale(nb_etapes_max=135) == TROIS"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Et la boucle `while` ?"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Bien ! on voit comment construire un $\\lambda$-terme exprimant un algorithme récursif. Mais comment exprimer une itération conditionnelle (boucle `while`) ? "
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"La réponse tient simplement dans le fait qu'une itération conditionnelle s'exprime généralement en suivant le schéma\n",
"\n",
"~~~python\n",
"while p(e):\n",
" e = t(e)\n",
"~~~\n",
"dans lequel \n",
"\n",
"* `e` désigne l'état courant des variables, \n",
"* `p(e)` exprime une condition dépendant de l'état courant \n",
"* et `t(e)` est un traitement pouvant modifier l'état courant.\n",
"\n",
"Ce schéma peut être reformulé de manière récursive en écrivant\n",
"\n",
"~~~python\n",
"def tq(e):\n",
" if p(e):\n",
" e = t(e)\n",
" return tq(e)\n",
" else:\n",
" return e\n",
"~~~"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Il suffit donc de considérer le $\\lambda$-terme\n",
"\n",
"$$\\Phi_{while} = \\lambda f.\\lambda p.\\lambda t.\\lambda e.(((\\mathtt{IF}\\ (p\\ e))\\ (((f\\ p)\\ t)\\ (t\\ e))\\ e),$$\n",
"\n",
"puis de définir le terme\n",
"\n",
"$$ \\mathtt{WHILE} = (Y\\ \\Phi_{while}),$$\n",
"ou \n",
"$$ \\mathtt{WHILE} = (\\Theta\\ \\Phi_{while}).$$"
]
},
{
"cell_type": "code",
"execution_count": 166,
"metadata": {},
"outputs": [],
"source": [
"M_PHI_WHILE = Lambda_terme('!f.!p.!t.!e.(((IF (p e)) (((f p) t) (t e))) e)')\n",
"PHI_WHILE = M_PHI_WHILE.subs('IF', IF)\n",
"WHILE = Y.applique(PHI_WHILE)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Pour terminer, utilisons notre terme $\\mathtt{WHILE}$ pour construire une terme permettant de calculer la division euclidienne de deux entiers, dernière opération arithmétique de base que nous n'avons pas réalisée."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On veut un terme $\\mathtt{DIV}$ qui comme la fonction `divmod` de Python donne, sous forme d'un couple, le quotient et le reste de la division d'un entier $m$ par un entier $n$.\n",
"\n",
"On pourrait programmer cette fonction en Python de cette façon :\n",
"\n",
"~~~python\n",
"def divmod(m, n):\n",
" q, r = 0, m\n",
" while r >= n:\n",
" q, r = q + 1, r - n\n",
" return (q, r)\n",
"~~~\n",
"Dans cet algorithme \n",
"* l'état `e` est le triplet de variables `(q, r, n)`\n",
"* la condition `p(e)` est exprimée par l'inégalité `r >= n`\n",
"* et le traitement `t(e)` modifiant l'état courant est le construction du couple `(q + 1, r - n, n)`.\n",
"\n",
"\\begin{align}\n",
" P &= \\lambda e.((\\mathtt{INF}\\ (\\mathtt{CDR}\\ (\\mathtt{CDR}\\ e))) (\\mathtt{CAR}\\ (\\mathtt{CDR}\\ e)))\\\\\n",
" T &= \\lambda e.((\\mathtt{CONS}\\ (\\mathtt{SUC}\\ (\\mathtt{CAR}\\ e))) ((\\mathtt{CONS}\\ ((\\mathtt{SUB}\\ (\\mathtt{CAR}\\ (\\mathtt{CDR}\\ e))) (\\mathtt{CDR}\\ (\\mathtt{CDR}\\ e)))) (\\mathtt{CDR}\\ (\\mathtt{CDR}\\ e))))\\\\\n",
" \\mathtt{DIVMOD} &= \\lambda m.\\lambda n.((((\\mathtt{WHILE}\\ P))\\ T)\\ [\\lceil 0\\rceil, [m, n]]).\n",
"\\end{align}"
]
},
{
"cell_type": "code",
"execution_count": 167,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λe.((INF (CDR (CDR e))) (CAR (CDR e)))\n",
"λe.((CONS (SUC (CAR e))) ((CONS ((SUB (CAR (CDR e))) (CDR (CDR e)))) (CDR (CDR e))))\n",
"λm.λn.(((WHILE P) T) ((CONS ZERO) ((CONS m) n)))\n",
"λm.λn.((((λf.(λx.(f (x x)) λx.(f (x x))) λf.λp.λt.λe.(((λc.λa.λs.((c a) s) (p e)) (((f p) t) (t e))) e)) λe.((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) n) n) m)) (λc.(c λx.λy.y) (λc.(c λx.λy.y) e))) (λc.(c λx.λy.x) (λc.(c λx.λy.y) e)))) λe.((λx.λy.λs.((s x) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.x) e))) ((λx.λy.λs.((s x) y) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.((s x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.((s x) y) λf.λx.x) λf.λx.x)))) n) (λc.(c λx.λy.x) (λc.(c λx.λy.y) e))) (λc.(c λx.λy.y) (λc.(c λx.λy.y) e)))) (λc.(c λx.λy.y) (λc.(c λx.λy.y) e))))) ((λx.λy.λs.((s x) y) λf.λx.x) ((λx.λy.λs.((s x) y) m) n)))\n"
]
}
],
"source": [
"M_P = Lambda_terme('!e.((INF (CDR (CDR e))) (CAR (CDR e)))')\n",
"print(M_P)\n",
"P = M_P.subs('INF', INF).subs('CAR', CAR).subs('CDR', CDR)\n",
"M_T = Lambda_terme('!e.((CONS (SUC (CAR e))) ((CONS ((SUB (CAR (CDR e))) (CDR (CDR e)))) (CDR (CDR e))))')\n",
"print(M_T)\n",
"T = M_T.subs('CONS', CONS).subs('CAR', CAR).subs('CDR', CDR).subs('SUC', SUC).subs('SUB', SUB)\n",
"M_DIVMOD = Lambda_terme('!m.!n.(((WHILE P) T) ((CONS ZERO) ((CONS m) n)))')\n",
"print(M_DIVMOD)\n",
"DIVMOD = M_DIVMOD.subs('WHILE', WHILE).subs('P', P).subs('T', T).subs('CONS', CONS).subs('ZERO', ZERO)\n",
"print(DIVMOD)"
]
},
{
"cell_type": "code",
"execution_count": 168,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"CPU times: user 17.1 s, sys: 7.09 ms, total: 17.1 s\n",
"Wall time: 17.1 s\n"
]
},
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 168,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"%%time\n",
"tests = []\n",
"for a in range(10):\n",
" for b in range(1, 10):\n",
" q, r = divmod(a, b)\n",
" A, B = int_en_church(a), int_en_church(b)\n",
" Q, R = int_en_church(q), int_en_church(r)\n",
" res = DIVMOD.applique(A).applique(B).forme_normale(nb_etapes_max=10000)\n",
" #print(res)\n",
" tests.append((a, b, res == CONS.applique(Q).applique(CONS.applique(R).applique(B)).forme_normale()))\n",
"all(t[2] for t in tests)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Conclusion"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Nous arrêtons là ce premier contact avec le $\\lambda$-calcul.\n",
"\n",
"Nous avons vu que ce langage très élémentaire, avec l'abstraction et l'application pour seules constructions, et la règle de $\\beta$-réduction pour seule transformation de $\\lambda$-termes, permet de représenter les données de base de n'importe quel langage de programmation, les booléens, les entiers, les couples, les listes, et permet d'exprimer les expressions conditionnelles, les itérations conditionnelles ou non, et la récursivité. En fait le $\\lambda$-calcul est un langage Turing-complet ... même s'il est particulièrement inefficace.\n",
"\n",
"D'autres sujets relatifs au $\\lambda$-calcul n'ont pas été abordés :\n",
"\n",
"* stratégies de réduction : paresseuse, par valeurs ..., et leurs conséquences.\n",
"* $\\lambda$-calcul typé."
]
},
{
"cell_type": "markdown",
"metadata": {
"incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
},
"source": [
"# $\\lambda$-calcul avec les lambda-expressions de Python"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Dans cette partie, les lambda-expressions de Python vont être utilisées pour représenter les abstractions, et les applications seront des appels de fonction.\n",
"\n",
"Les seuls mots du langage Python que nous utiliserons seront `lambda` et `if`. Les autres mots (`def`, `while`, `for` ...) seront bannis. Nous utiliserons aussi les entiers prédéfinis dans le langage avec certaines opérations arithmétiques."
]
},
{
"cell_type": "markdown",
"metadata": {
"incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
},
"source": [
"## Les booléens"
]
},
{
"cell_type": "code",
"execution_count": 169,
"metadata": {},
"outputs": [],
"source": [
"vrai = lambda x: lambda y: x\n",
"faux = lambda x: lambda y: y"
]
},
{
"cell_type": "code",
"execution_count": 170,
"metadata": {},
"outputs": [],
"source": [
"def booleen_en_bool(b):\n",
" return b(True)(False)"
]
},
{
"cell_type": "code",
"execution_count": 171,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, False)"
]
},
"execution_count": 171,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(booleen_en_bool(b) for b in (vrai, faux))"
]
},
{
"cell_type": "code",
"execution_count": 172,
"metadata": {},
"outputs": [],
"source": [
"If = lambda c: lambda a: lambda s: c(a)(s) "
]
},
{
"cell_type": "code",
"execution_count": 173,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"1"
]
},
"execution_count": 173,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"If(vrai)(1)(2)"
]
},
{
"cell_type": "code",
"execution_count": 174,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"2"
]
},
"execution_count": 174,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"If(faux)(1)(2)"
]
},
{
"cell_type": "code",
"execution_count": 175,
"metadata": {},
"outputs": [],
"source": [
"#If(vrai)(1)(1/0)"
]
},
{
"cell_type": "code",
"execution_count": 176,
"metadata": {},
"outputs": [],
"source": [
"non = lambda b: If(b)(faux)(vrai)"
]
},
{
"cell_type": "code",
"execution_count": 177,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(False, True)"
]
},
"execution_count": 177,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(booleen_en_bool(non(b)) for b in (vrai, faux))"
]
},
{
"cell_type": "code",
"execution_count": 178,
"metadata": {},
"outputs": [],
"source": [
"et = lambda b1: lambda b2: If(b1)(b2)(faux)"
]
},
{
"cell_type": "code",
"execution_count": 179,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, False, False, False)"
]
},
"execution_count": 179,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(booleen_en_bool(et(b1)(b2)) for b1 in (vrai, faux) \n",
" for b2 in (vrai, faux))"
]
},
{
"cell_type": "code",
"execution_count": 180,
"metadata": {},
"outputs": [],
"source": [
"ou = lambda b1: lambda b2: If(b1)(vrai)(b2)"
]
},
{
"cell_type": "code",
"execution_count": 181,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, True, True, False)"
]
},
"execution_count": 181,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(booleen_en_bool(ou(b1)(b2)) for b1 in (vrai, faux) \n",
" for b2 in (vrai, faux))"
]
},
{
"cell_type": "markdown",
"metadata": {
"incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
},
"source": [
"## Les entiers de Church"
]
},
{
"cell_type": "code",
"execution_count": 182,
"metadata": {},
"outputs": [],
"source": [
"zero = lambda f: lambda x: x"
]
},
{
"cell_type": "code",
"execution_count": 183,
"metadata": {},
"outputs": [],
"source": [
"un = lambda f: lambda x: f(x)"
]
},
{
"cell_type": "code",
"execution_count": 184,
"metadata": {},
"outputs": [],
"source": [
"deux = lambda f: lambda x: f(f(x))"
]
},
{
"cell_type": "code",
"execution_count": 185,
"metadata": {},
"outputs": [],
"source": [
"trois = lambda f: lambda x: f(f(f(x)))"
]
},
{
"cell_type": "code",
"execution_count": 186,
"metadata": {},
"outputs": [],
"source": [
"def entier_church_en_int(ec):\n",
" return ec(lambda n: n+1)(0)"
]
},
{
"cell_type": "code",
"execution_count": 187,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(0, 1, 2, 3)"
]
},
"execution_count": 187,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(entier_church_en_int(n) for n in (zero, un, deux, trois))"
]
},
{
"cell_type": "code",
"execution_count": 188,
"metadata": {},
"outputs": [],
"source": [
"suc = lambda n: lambda f: lambda x: f(n(f)(x))"
]
},
{
"cell_type": "code",
"execution_count": 189,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(1, 2, 3, 4)"
]
},
"execution_count": 189,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(entier_church_en_int(suc(n)) for n in (zero, un, deux, trois)) "
]
},
{
"cell_type": "code",
"execution_count": 190,
"metadata": {},
"outputs": [],
"source": [
"def int_en_entier_church(n):\n",
" if n == 0:\n",
" return zero\n",
" else:\n",
" return suc(int_en_entier_church(n - 1))"
]
},
{
"cell_type": "code",
"execution_count": 191,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)"
]
},
"execution_count": 191,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(entier_church_en_int(int_en_entier_church(n)) for n in range(10))"
]
},
{
"cell_type": "code",
"execution_count": 192,
"metadata": {},
"outputs": [],
"source": [
"add = lambda n: lambda m: lambda f: lambda x: n(f)(m(f)(x))"
]
},
{
"cell_type": "code",
"execution_count": 193,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"5"
]
},
"execution_count": 193,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"cinq = add(deux)(trois)\n",
"entier_church_en_int(cinq)"
]
},
{
"cell_type": "code",
"execution_count": 194,
"metadata": {},
"outputs": [],
"source": [
"mul = lambda n: lambda m: lambda f: n(m(f))"
]
},
{
"cell_type": "code",
"execution_count": 195,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"6"
]
},
"execution_count": 195,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"six = mul(deux)(trois)\n",
"entier_church_en_int(six)"
]
},
{
"cell_type": "code",
"execution_count": 196,
"metadata": {},
"outputs": [],
"source": [
"exp = lambda n: lambda m: m(n)"
]
},
{
"cell_type": "code",
"execution_count": 197,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"8"
]
},
"execution_count": 197,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"huit = exp(deux)(trois)\n",
"entier_church_en_int(huit)"
]
},
{
"cell_type": "code",
"execution_count": 198,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"9"
]
},
"execution_count": 198,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"neuf = exp(trois)(deux)\n",
"entier_church_en_int(neuf)"
]
},
{
"cell_type": "code",
"execution_count": 199,
"metadata": {},
"outputs": [],
"source": [
"est_nul = lambda n : n(lambda x: faux)(vrai)"
]
},
{
"cell_type": "code",
"execution_count": 200,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, False, False, False, False, False, False)"
]
},
"execution_count": 200,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(booleen_en_bool(est_nul(n)) \n",
" for n in (zero, un, deux, trois, cinq, six, huit))"
]
},
{
"cell_type": "markdown",
"metadata": {
"incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
},
"source": [
"## Les couples"
]
},
{
"cell_type": "code",
"execution_count": 201,
"metadata": {},
"outputs": [],
"source": [
"cons = lambda x: lambda y: lambda z: z(x)(y)"
]
},
{
"cell_type": "code",
"execution_count": 202,
"metadata": {},
"outputs": [],
"source": [
"un_deux = cons(un)(deux)"
]
},
{
"cell_type": "code",
"execution_count": 203,
"metadata": {},
"outputs": [],
"source": [
"car = lambda c: c(vrai)\n",
"cdr = lambda c: c(faux)"
]
},
{
"cell_type": "code",
"execution_count": 204,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(1, 2)"
]
},
"execution_count": 204,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entier_church_en_int(car(un_deux)), entier_church_en_int(cdr(un_deux))"
]
},
{
"cell_type": "code",
"execution_count": 205,
"metadata": {},
"outputs": [],
"source": [
"pred = lambda n: car(n(lambda c: cons(cdr(c))(suc(cdr(c))))(cons(zero)(zero)))"
]
},
{
"cell_type": "code",
"execution_count": 206,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(0, 0, 1, 2, 3, 4, 5, 6, 7, 8)"
]
},
"execution_count": 206,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(entier_church_en_int(pred(int_en_entier_church(n))) for n in range(10))"
]
},
{
"cell_type": "code",
"execution_count": 207,
"metadata": {},
"outputs": [],
"source": [
"sub = lambda n: lambda m: m(pred)(n)"
]
},
{
"cell_type": "code",
"execution_count": 208,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"5"
]
},
"execution_count": 208,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"entier_church_en_int(sub(huit)(trois))"
]
},
{
"cell_type": "code",
"execution_count": 209,
"metadata": {},
"outputs": [],
"source": [
"est_inf_ou_egal = lambda n: lambda m: est_nul(sub(m)(n))"
]
},
{
"cell_type": "code",
"execution_count": 210,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, True, True, True, True, True, False, False, False, False)"
]
},
"execution_count": 210,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(booleen_en_bool(est_inf_ou_egal(cinq)(int_en_entier_church(n))) \n",
" for n in range(10))"
]
},
{
"cell_type": "code",
"execution_count": 211,
"metadata": {},
"outputs": [],
"source": [
"est_egal = lambda n: lambda m: et(est_inf_ou_egal(n)(m))(est_inf_ou_egal(m)(n))"
]
},
{
"cell_type": "code",
"execution_count": 212,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(False, False, False, False, False, True, False, False, False, False)"
]
},
"execution_count": 212,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(booleen_en_bool(est_egal(cinq)(int_en_entier_church(n))) \n",
" for n in range(10))"
]
},
{
"cell_type": "markdown",
"metadata": {
"incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
},
"source": [
"## Itération"
]
},
{
"cell_type": "code",
"execution_count": 213,
"metadata": {},
"outputs": [],
"source": [
"fact = lambda n: cdr(n(lambda c: (cons(suc(car(c)))(mul(suc(car(c)))(cdr(c)))))(cons(zero)(un)))"
]
},
{
"cell_type": "code",
"execution_count": 214,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(1, 1, 2, 6, 24, 120, 720)"
]
},
"execution_count": 214,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(entier_church_en_int(fact(int_en_entier_church(n))) for n in range(7))"
]
},
{
"cell_type": "markdown",
"metadata": {
"incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
},
"source": [
"## Combinateur de point fixe"
]
},
{
"cell_type": "code",
"execution_count": 215,
"metadata": {},
"outputs": [],
"source": [
"phi_fact = lambda f: lambda n: 1 if n == 0 else n*f(n-1)"
]
},
{
"cell_type": "code",
"execution_count": 216,
"metadata": {},
"outputs": [],
"source": [
"bottom = lambda x: (lambda y: y(y))(lambda y:y(y))"
]
},
{
"cell_type": "code",
"execution_count": 217,
"metadata": {},
"outputs": [],
"source": [
"f0 = phi_fact(bottom)\n",
"f1 = phi_fact(f0)\n",
"f2 = phi_fact(f1)\n",
"f3 = phi_fact(f2)\n",
"f4 = phi_fact(f3)"
]
},
{
"cell_type": "code",
"execution_count": 218,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(1, 1, 2, 6)"
]
},
"execution_count": 218,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(f4(n) for n in range(4))"
]
},
{
"cell_type": "code",
"execution_count": 219,
"metadata": {},
"outputs": [],
"source": [
"def fact_rec(n):\n",
" if n == 0:\n",
" return 1\n",
" else:\n",
" return n * fact_rec(n - 1)"
]
},
{
"cell_type": "code",
"execution_count": 220,
"metadata": {},
"outputs": [],
"source": [
"fact2 = phi_fact(fact_rec)"
]
},
{
"cell_type": "code",
"execution_count": 221,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(1, 1, 2, 6, 24, 120, 720)"
]
},
"execution_count": 221,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(fact2(n) for n in range(7))"
]
},
{
"cell_type": "code",
"execution_count": 222,
"metadata": {},
"outputs": [],
"source": [
"fix_curry = lambda f: (lambda x: lambda y: f(x(x))(y))(lambda x: lambda y: f(x(x))(y))"
]
},
{
"cell_type": "code",
"execution_count": 223,
"metadata": {},
"outputs": [],
"source": [
"fact3 = fix_curry(phi_fact)"
]
},
{
"cell_type": "code",
"execution_count": 224,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(1, 1, 2, 6, 24, 120, 720)"
]
},
"execution_count": 224,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"tuple(fact3(n) for n in range(7))"
]
},
{
"cell_type": "markdown",
"metadata": {
"incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
},
"source": [
"## Un programme obscur"
]
},
{
"cell_type": "code",
"execution_count": 225,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"hello world!\n"
]
}
],
"source": [
"print((lambda x: (lambda y: lambda z: x(y(y))(z))(lambda y: lambda z: x(y(y))(z))) \n",
" (lambda x: lambda y: '' if y == [] else chr(y[0])+x(y[1:]))\n",
" (((lambda x: (lambda y: lambda z: x(y(y))(z)) (lambda y: lambda z: x(y(y))(z)))\n",
" (lambda x: lambda y: lambda z: [] if z == [] else [y(z[0])]+x(y)(z[1:]))) \n",
" (lambda x: (lambda x: (lambda y: lambda z: x(y(y))(z))(lambda y: lambda z: x(y(y))(z)))\n",
" (lambda x: lambda y: lambda z: lambda t: 1 if t == 0 else (lambda x: ((lambda u: 1 if u == 0 else z)(t % 2)) * x * x % y)\n",
" (x(y)(z)(t // 2)))(989)(x)(761))\n",
" ([377, 900, 27, 27, 182, 647, 163, 182, 390, 27, 726, 937])))"
]
},
{
"cell_type": "code",
"execution_count": 226,
"metadata": {},
"outputs": [],
"source": [
"phiListEnChaine = lambda x: lambda y: '' if y == [] else chr(y[0]) + x(y[1:])"
]
},
{
"cell_type": "code",
"execution_count": 227,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"'ABCDEFGHIJKLMNOPQRSTUVWXYZ'"
]
},
"execution_count": 227,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"fix_curry(phiListEnChaine)([65+k for k in range(26)])"
]
},
{
"cell_type": "code",
"execution_count": 228,
"metadata": {},
"outputs": [],
"source": [
"phiMap = lambda x: lambda y: lambda z: [] if z == [] else [y(z[0])] + x(y)(z[1:])"
]
},
{
"cell_type": "code",
"execution_count": 229,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"[1, 4, 9, 16]"
]
},
"execution_count": 229,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"fix_curry(phiMap)(lambda x: x*x)([1, 2, 3, 4])"
]
},
{
"cell_type": "code",
"execution_count": 230,
"metadata": {},
"outputs": [],
"source": [
"phiExpoMod = lambda x: lambda y: lambda z: lambda t: 1 if z == 0 else (lambda u: 1 if u == 0 else y)(z % 2) * x(y)(z//2)(t) ** 2 % t"
]
},
{
"cell_type": "code",
"execution_count": 231,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"24"
]
},
"execution_count": 231,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"fix_curry(phiExpoMod)(2)(10)(1000)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"jupytext": {
"formats": "ipynb,md"
},
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.7.3"
},
"toc-autonumbering": true,
"toc-showcode": false,
"toc-showmarkdowntxt": false,
"widgets": {
"application/vnd.jupyter.widget-state+json": {
"state": {},
"version_major": 2,
"version_minor": 0
}
}
},
"nbformat": 4,
"nbformat_minor": 4
}
Reference in New Issue View Git Blame Copy Permalink