Lambda_Calcul/lambda_calcul.ipynb

{
 "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",
    "2. la deuxième partie reprend la partie « pouvoir d'expression du $\\lambda$-calcul » en l'illustrant avec les lambda-expressions du langage Python."
   ]
  },
  {
   "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": [
    "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."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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.(x y) x))\n",
      "  2: ---> ((λx.(x y) x) y)\n",
      "  3: ---> ((x y) y)\n",
      "Forme normale calculée : ((x y) y)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fa0c27bd240>"
      ]
     },
     "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",
    "$$ VRAI = \\lambda x.\\lambda y.x,$$\n",
    "et\n",
    "$$ 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": [
    "#### 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: ---> (((λc.λa.λs.((c a) s) λx.λy.x) ALORS) SINON)\n",
      "  2: ---> ((λa.λs.((λx.λy.x a) s) ALORS) SINON)\n",
      "  3: ---> (λs.((λx.λy.x ALORS) s) SINON)\n",
      "  4: ---> ((λx.λy.x ALORS) SINON)\n",
      "  5: ---> (λy.ALORS SINON)\n",
      "  6: ---> ALORS\n",
      "Forme normale calculée : ALORS\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fa0c27e4588>"
      ]
     },
     "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: ---> (((λc.λa.λs.((c a) s) λx.λy.y) ALORS) SINON)\n",
      "  2: ---> ((λa.λs.((λx.λy.y a) s) ALORS) SINON)\n",
      "  3: ---> (λs.((λx.λy.y ALORS) s) SINON)\n",
      "  4: ---> ((λx.λy.y ALORS) SINON)\n",
      "  5: ---> (λy.y SINON)\n",
      "  6: ---> SINON\n",
      "Forme normale calculée : SINON\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fa0c27e4c18>"
      ]
     },
     "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: ---> (((λc.λa.λs.((c a) s) λx.λy.x) ALORS) (λx.(x x) λx.(x x)))\n",
      "  2: ---> ((λa.λs.((λx.λy.x a) s) ALORS) (λx.(x x) λx.(x x)))\n",
      "  3: ---> (λs.((λx.λy.x ALORS) s) (λx.(x x) λx.(x x)))\n",
      "  4: ---> ((λx.λy.x ALORS) (λx.(x x) λx.(x x)))\n",
      "  5: ---> (λy.ALORS (λx.(x x) λx.(x x)))\n",
      "  6: ---> ALORS\n",
      "Forme normale calculée : ALORS\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fa0c27e8128>"
      ]
     },
     "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: ---> (((λc.λa.λs.((c a) s) λx.λy.y) (λx.(x x) λx.(x x))) SINON)\n",
      "  2: ---> ((λa.λs.((λx.λy.y a) s) (λx.(x x) λx.(x x))) SINON)\n",
      "  3: ---> (λs.((λx.λy.y (λx.(x x) λx.(x x))) s) SINON)\n",
      "  4: ---> ((λx.λy.y (λx.(x x) λx.(x x))) SINON)\n",
      "  5: ---> (λy.y SINON)\n",
      "  6: ---> SINON\n",
      "Forme normale calculée : SINON\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fa0c27c77b8>"
      ]
     },
     "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 `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",
    "$$ ET = \\lambda a.\\lambda b.(((IF\\ a)\\ b)\\ 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: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.x) λx.λy.x)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.x) b) λx.λy.y) λx.λy.x)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) λx.λy.y)\n",
      "  4: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.x) λx.λy.y)\n",
      "  5: ---> (λs.((λx.λy.x λx.λy.x) s) λx.λy.y)\n",
      "  6: ---> ((λx.λy.x λx.λy.x) λx.λy.y)\n",
      "  7: ---> (λy.λx.λy.x λx.λy.y)\n",
      "  8: ---> λ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: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.x) λx.λy.y)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.x) b) λx.λy.y) λx.λy.y)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.y) λx.λy.y)\n",
      "  4: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.y) λx.λy.y)\n",
      "  5: ---> (λs.((λx.λy.x λx.λy.y) s) λx.λy.y)\n",
      "  6: ---> ((λx.λy.x λx.λy.y) λx.λy.y)\n",
      "  7: ---> (λy.λx.λy.y λx.λy.y)\n",
      "  8: ---> λ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: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.y) λx.λy.x)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.y) b) λx.λy.y) λx.λy.x)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) λx.λy.y)\n",
      "  4: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.x) λx.λy.y)\n",
      "  5: ---> (λs.((λx.λy.y λx.λy.x) s) λx.λy.y)\n",
      "  6: ---> ((λx.λy.y λx.λy.x) λx.λy.y)\n",
      "  7: ---> (λy.y λx.λy.y)\n",
      "  8: ---> λ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: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.y) λx.λy.y)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.y) b) λx.λy.y) λx.λy.y)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.y) λx.λy.y)\n",
      "  4: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.y) λx.λy.y)\n",
      "  5: ---> (λs.((λx.λy.y λx.λy.y) s) λx.λy.y)\n",
      "  6: ---> ((λx.λy.y λx.λy.y) λx.λy.y)\n",
      "  7: ---> (λy.y λx.λy.y)\n",
      "  8: ---> λ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",
    "$$ OU = \\lambda a.\\lambda b.(((IF\\ a)\\ 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: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.x) λx.λy.x)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) b) λx.λy.x)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) λx.λy.x)\n",
      "  4: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.x) λx.λy.x)\n",
      "  5: ---> (λs.((λx.λy.x λx.λy.x) s) λx.λy.x)\n",
      "  6: ---> ((λx.λy.x λx.λy.x) λx.λy.x)\n",
      "  7: ---> (λy.λx.λy.x λx.λy.x)\n",
      "  8: ---> λ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: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.x) λx.λy.y)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) b) λx.λy.y)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) λx.λy.y)\n",
      "  4: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.x) λx.λy.y)\n",
      "  5: ---> (λs.((λx.λy.x λx.λy.x) s) λx.λy.y)\n",
      "  6: ---> ((λx.λy.x λx.λy.x) λx.λy.y)\n",
      "  7: ---> (λy.λx.λy.x λx.λy.y)\n",
      "  8: ---> λ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: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.y) λx.λy.x)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) b) λx.λy.x)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) λx.λy.x)\n",
      "  4: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.x) λx.λy.x)\n",
      "  5: ---> (λs.((λx.λy.y λx.λy.x) s) λx.λy.x)\n",
      "  6: ---> ((λx.λy.y λx.λy.x) λx.λy.x)\n",
      "  7: ---> (λy.y λx.λy.x)\n",
      "  8: ---> λ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: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.y) λx.λy.y)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) b) λx.λy.y)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) λx.λy.y)\n",
      "  4: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.x) λx.λy.y)\n",
      "  5: ---> (λs.((λx.λy.y λx.λy.x) s) λx.λy.y)\n",
      "  6: ---> ((λx.λy.y λx.λy.x) λx.λy.y)\n",
      "  7: ---> (λy.y λx.λy.y)\n",
      "  8: ---> λ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",
    "$$ NON = \\lambda a.(((IF\\ a)\\ FAUX)\\ 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: ---> (λa.(((λc.λa.λs.((c a) s) a) λx.λy.y) λx.λy.x) λx.λy.x)\n",
      "  2: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.y) λx.λy.x)\n",
      "  3: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.y) λx.λy.x)\n",
      "  4: ---> (λs.((λx.λy.x λx.λy.y) s) λx.λy.x)\n",
      "  5: ---> ((λx.λy.x λx.λy.y) λx.λy.x)\n",
      "  6: ---> (λy.λx.λy.y λx.λy.x)\n",
      "  7: ---> λ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: ---> (λa.(((λc.λa.λs.((c a) s) a) λx.λy.y) λx.λy.x) λx.λy.y)\n",
      "  2: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.y) λx.λy.x)\n",
      "  3: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.y) λx.λy.x)\n",
      "  4: ---> (λs.((λx.λy.y λx.λy.y) s) λx.λy.x)\n",
      "  5: ---> ((λx.λy.y λx.λy.y) λ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": 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": "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": [
    "#### Successeur"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 56,
   "metadata": {},
   "outputs": [],
   "source": [
    "SUC = Lambda_terme('!n.!f.!x.(f ((n f) x))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 57,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x)))\n",
      "  1: ---> (λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x)))\n",
      "  2: ---> λf.λx.(f ((λf.λx.(f (f x)) f) x))\n",
      "  3: ---> λf.λx.(f (λx.(f (f x)) x))\n",
      "  4: ---> λ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": "code",
   "execution_count": 58,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λf.λx.(f (f (f x))) λn.λf.λx.(f ((n f) x))) λf.λx.x)\n",
      "  1: ---> ((λf.λx.(f (f (f x))) λn.λf.λx.(f ((n f) x))) λf.λx.x)\n",
      "  2: ---> (λ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)\n",
      "  3: ---> (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.x)))\n",
      "  4: ---> λf.λx.(f (((λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.x)) f) x))\n",
      "  5: ---> λf.λx.(f ((λf.λx.(f (((λn.λf.λx.(f ((n f) x)) λf.λx.x) f) x)) f) x))\n",
      "  6: ---> λf.λx.(f (λx.(f (((λn.λf.λx.(f ((n f) x)) λf.λx.x) f) x)) x))\n",
      "  7: ---> λf.λx.(f (f (((λn.λf.λx.(f ((n f) x)) λf.λx.x) f) x)))\n",
      "  8: ---> λf.λx.(f (f ((λf.λx.(f ((λf.λx.x f) x)) f) x)))\n",
      "  9: ---> λf.λx.(f (f (λx.(f ((λf.λx.x f) x)) x)))\n",
      " 10: ---> λf.λx.(f (f (f ((λf.λx.x f) x))))\n",
      " 11: ---> λf.λx.(f (f (f (λx.x x))))\n",
      " 12: ---> λf.λx.(f (f (f x)))\n",
      "Forme normale calculée : λf.λx.(f (f (f x)))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fa0c27f5a58>"
      ]
     },
     "execution_count": 58,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "TROIS.applique(SUC).applique(ZERO).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Addition"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 59,
   "metadata": {},
   "outputs": [],
   "source": [
    "ADD = Lambda_terme('!n.!m.!f.!x.((n f) ((m f) x))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 60,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λn.λm.λf.λx.((n f) ((m f) x)) λf.λx.(f x)) λf.λx.(f (f (f x))))\n",
      "  1: ---> ((λn.λm.λf.λx.((n f) ((m f) x)) λf.λx.(f x)) λf.λx.(f (f (f x))))\n",
      "  2: ---> (λm.λf.λx.((λf.λx.(f x) f) ((m f) x)) λf.λx.(f (f (f x))))\n",
      "  3: ---> λf.λx.((λf.λx.(f x) f) ((λf.λx.(f (f (f x))) f) x))\n",
      "  4: ---> λf.λx.(λx.(f x) ((λf.λx.(f (f (f x))) 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": 61,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λn.λm.λf.λx.((n f) ((m f) x)) λf.λx.(f (f (f x)))) λf.λx.(f (f x)))\n",
      "  1: ---> ((λn.λm.λf.λx.((n f) ((m f) x)) λf.λx.(f (f (f x)))) λf.λx.(f (f x)))\n",
      "  2: ---> (λm.λf.λx.((λf.λx.(f (f (f x))) f) ((m f) x)) λf.λx.(f (f x)))\n",
      "  3: ---> λf.λx.((λf.λx.(f (f (f x))) f) ((λf.λx.(f (f x)) f) x))\n",
      "  4: ---> λf.λx.(λx.(f (f (f x))) ((λf.λx.(f (f x)) f) x))\n",
      "  5: ---> λf.λx.(f (f (f ((λf.λx.(f (f x)) f) x))))\n",
      "  6: ---> λf.λx.(f (f (f (λx.(f (f x)) x))))\n",
      "  7: ---> λ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": 62,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λn.λm.λf.λx.((n f) ((m f) x)) λf.λx.(f (f (f (f x))))) λf.λx.(f (f (f x))))\n",
      "  1: ---> ((λn.λm.λf.λx.((n f) ((m f) x)) λf.λx.(f (f (f (f x))))) λf.λx.(f (f (f x))))\n",
      "  2: ---> (λm.λf.λx.((λf.λx.(f (f (f (f x)))) f) ((m f) x)) λf.λx.(f (f (f x))))\n",
      "  3: ---> λf.λx.((λf.λx.(f (f (f (f x)))) f) ((λf.λx.(f (f (f x))) f) x))\n",
      "  4: ---> λf.λx.(λx.(f (f (f (f x)))) ((λf.λx.(f (f (f x))) f) x))\n",
      "  5: ---> λf.λx.(f (f (f (f ((λf.λx.(f (f (f x))) f) x)))))\n",
      "  6: ---> λf.λx.(f (f (f (f (λx.(f (f (f x))) x)))))\n",
      "  7: ---> λ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": "code",
   "execution_count": 63,
   "metadata": {},
   "outputs": [],
   "source": [
    "MUL = Lambda_terme('!n.!m.!f.(n (m f))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 64,
   "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: ---> ((λn.λm.λf.(n (m f)) λf.λx.(f (f x))) λf.λx.(f (f (f x))))\n",
      "  2: ---> (λm.λf.(λf.λx.(f (f x)) (m f)) λf.λx.(f (f (f x))))\n",
      "  3: ---> λf.(λf.λx.(f (f x)) (λf.λx.(f (f (f x))) f))\n",
      "  4: ---> λf.λx.((λf.λx.(f (f (f x))) f) ((λf.λx.(f (f (f x))) f) x))\n",
      "  5: ---> λf.λx.(λx.(f (f (f x))) ((λf.λx.(f (f (f x))) f) x))\n",
      "  6: ---> λf.λx.(f (f (f ((λf.λx.(f (f (f x))) f) x))))\n",
      "  7: ---> λf.λx.(f (f (f (λx.(f (f (f x))) x))))\n",
      "  8: ---> λ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": [
    "#### Exponentiation"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 65,
   "metadata": {},
   "outputs": [],
   "source": [
    "EXP = Lambda_terme('!n.!m.(m n)')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 66,
   "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: ---> ((λn.λm.(m n) λf.λx.(f (f x))) λf.λx.(f (f (f x))))\n",
      "  2: ---> (λm.(m λf.λx.(f (f x))) λf.λx.(f (f (f x))))\n",
      "  3: ---> (λf.λx.(f (f (f x))) λf.λx.(f (f x)))\n",
      "  4: ---> λx.(λf.λx.(f (f x)) (λf.λx.(f (f x)) (λf.λx.(f (f x)) x)))\n",
      "  5: ---> λ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",
      "  6: ---> λ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",
      "  7: ---> λ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",
      "  8: ---> λ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",
      "  9: ---> λx.λx0.(x (x ((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0))))\n",
      " 10: ---> λx.λx0.(x (x (λx0.(x (x x0)) ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0))))\n",
      " 11: ---> λx.λx0.(x (x (x (x ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0)))))\n",
      " 12: ---> λx.λx0.(x (x (x (x (λx0.((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) x) x0)) x0)))))\n",
      " 13: ---> λx.λx0.(x (x (x (x ((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) x) x0))))))\n",
      " 14: ---> λx.λx0.(x (x (x (x (λx0.(x (x x0)) ((λf.λx.(f (f x)) x) x0))))))\n",
      " 15: ---> λx.λx0.(x (x (x (x (x (x ((λf.λx.(f (f x)) x) x0)))))))\n",
      " 16: ---> λx.λx0.(x (x (x (x (x (x (λx0.(x (x x0)) x0)))))))\n",
      " 17: ---> λ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": 67,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 67,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "HUIT == MUL.applique(DEUX).applique(QUATRE).forme_normale()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 68,
   "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: ---> ((λn.λm.(m n) λf.λx.(f (f (f x)))) λf.λx.(f (f x)))\n",
      "  2: ---> (λm.(m λf.λx.(f (f (f x)))) λf.λx.(f (f x)))\n",
      "  3: ---> (λf.λx.(f (f x)) λf.λx.(f (f (f x))))\n",
      "  4: ---> λx.(λf.λx.(f (f (f x))) (λf.λx.(f (f (f x))) x))\n",
      "  5: ---> λ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",
      "  6: ---> λx.λx0.(λx0.(x (x (x x0))) ((λf.λx.(f (f (f x))) x) ((λf.λx.(f (f (f x))) x) x0)))\n",
      "  7: ---> λx.λx0.(x (x (x ((λf.λx.(f (f (f x))) x) ((λf.λx.(f (f (f x))) x) x0)))))\n",
      "  8: ---> λx.λx0.(x (x (x (λx0.(x (x (x x0))) ((λf.λx.(f (f (f x))) x) x0)))))\n",
      "  9: ---> λx.λx0.(x (x (x (x (x (x ((λf.λx.(f (f (f x))) x) x0)))))))\n",
      " 10: ---> λx.λx0.(x (x (x (x (x (x (λx0.(x (x (x x0))) x0)))))))\n",
      " 11: ---> λ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": 69,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 69,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "NEUF == ADD.applique(SEPT).applique(DEUX).forme_normale()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Nullité"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 70,
   "metadata": {},
   "outputs": [],
   "source": [
    "NUL = Lambda_terme('!n.((n !x.FAUX) VRAI)').subs('FAUX', FAUX).subs('VRAI', VRAI)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 71,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λn.((n λx.λx.λy.y) λx.λy.x)\n"
     ]
    }
   ],
   "source": [
    "print(NUL)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 72,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λn.((n λx.λx.λy.y) λx.λy.x) λf.λx.x)\n",
      "  1: ---> (λn.((n λx.λx.λy.y) λx.λy.x) λf.λx.x)\n",
      "  2: ---> ((λf.λx.x λx.λx.λy.y) λx.λy.x)\n",
      "  3: ---> (λx.x λx.λy.x)\n",
      "  4: ---> λx.λy.x\n",
      "Forme normale calculée : λx.λy.x\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 72,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "NUL.applique(ZERO).forme_normale(verbose=True) == VRAI"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 73,
   "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: ---> (λn.((n λx.λx.λy.y) λx.λy.x) λf.λx.(f (f (f x))))\n",
      "  2: ---> ((λf.λx.(f (f (f x))) λx.λx.λy.y) λx.λy.x)\n",
      "  3: ---> (λx.(λx.λx.λy.y (λx.λx.λy.y (λx.λx.λy.y x))) λx.λy.x)\n",
      "  4: ---> (λx.λx.λy.y (λx.λx.λy.y (λx.λx.λy.y λx.λy.x)))\n",
      "  5: ---> λx.λy.y\n",
      "Forme normale calculée : λx.λy.y\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 73,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "NUL.applique(TROIS).forme_normale(verbose=True) == FAUX"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Couples et listes"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 74,
   "metadata": {},
   "outputs": [],
   "source": [
    "CONS = Lambda_terme('!x.!y.!s.(((IF s) x) y)').subs('IF', IF)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 75,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y)\n"
     ]
    }
   ],
   "source": [
    "print(CONS)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 76,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  1: ---> ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  2: ---> (λy.λs.(((λc.λa.λs.((c a) s) s) λf.λx.(f x)) y) λf.λx.(f (f x)))\n",
      "  3: ---> λs.(((λc.λa.λs.((c a) s) s) λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  4: ---> λs.((λa.λs0.((s a) s0) λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  5: ---> λs.(λs0.((s λf.λx.(f x)) s0) λf.λx.(f (f x)))\n",
      "  6: ---> λ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": 77,
   "metadata": {},
   "outputs": [],
   "source": [
    "CAR = Lambda_terme('!c.(c VRAI)').subs('VRAI', VRAI)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 78,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λc.(c λx.λy.x)\n"
     ]
    }
   ],
   "source": [
    "print(CAR)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 79,
   "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: ---> (λc.(c λx.λy.x) λs.((s λf.λx.(f x)) λf.λx.(f (f x))))\n",
      "  2: ---> (λs.((s λf.λx.(f x)) λf.λx.(f (f x))) λx.λy.x)\n",
      "  3: ---> ((λx.λy.x λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  4: ---> (λy.λf.λx.(f x) λf.λx.(f (f x)))\n",
      "  5: ---> λf.λx.(f x)\n",
      "Forme normale calculée : λf.λx.(f x)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 79,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "CAR.applique(UN_DEUX).forme_normale(verbose=True) == UN"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 80,
   "metadata": {},
   "outputs": [],
   "source": [
    "CDR = Lambda_terme('!c.(c FAUX)').subs('FAUX', FAUX)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 81,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λc.(c λx.λy.y)\n"
     ]
    }
   ],
   "source": [
    "print(CDR)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 82,
   "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: ---> (λc.(c λx.λy.y) λs.((s λf.λx.(f x)) λf.λx.(f (f x))))\n",
      "  2: ---> (λs.((s λf.λx.(f x)) λf.λx.(f (f x))) λx.λy.y)\n",
      "  3: ---> ((λx.λy.y λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  4: ---> (λy.y λf.λx.(f (f x)))\n",
      "  5: ---> λf.λx.(f (f x))\n",
      "Forme normale calculée : λf.λx.(f (f x))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 82,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "CDR.applique(UN_DEUX).forme_normale(verbose=True) == DEUX"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 83,
   "metadata": {},
   "outputs": [],
   "source": [
    "M = Lambda_terme('M')\n",
    "CPLE_M = CONS.applique(CAR.applique(M)).applique(CDR.applique(M))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 84,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.x) M)) (λc.(c λx.λy.y) M)))\n",
      "  1: ---> (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.x) M)) (λc.(c λx.λy.y) M)))\n",
      "  2: ---> (((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.x) M)) (λc.(c λx.λy.y) M)) λx.λy.y)\n",
      "  3: ---> ((λy.λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.x) M)) y) (λc.(c λx.λy.y) M)) λx.λy.y)\n",
      "  4: ---> (λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.x) M)) (λc.(c λx.λy.y) M)) λx.λy.y)\n",
      "  5: ---> (((λc.λa.λs.((c a) s) λx.λy.y) (λc.(c λx.λy.x) M)) (λc.(c λx.λy.y) M))\n",
      "  6: ---> ((λa.λs.((λx.λy.y a) s) (λc.(c λx.λy.x) M)) (λc.(c λx.λy.y) M))\n",
      "  7: ---> (λs.((λx.λy.y (λc.(c λx.λy.x) M)) s) (λc.(c λx.λy.y) M))\n",
      "  8: ---> ((λx.λy.y (λc.(c λx.λy.x) M)) (λc.(c λx.λy.y) M))\n",
      "  9: ---> (λy.y (λc.(c λx.λy.y) M))\n",
      " 10: ---> (λc.(c λx.λy.y) M)\n",
      " 11: ---> (M λx.λy.y)\n",
      "Forme normale calculée : (M λx.λy.y)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fa0c27dc7f0>"
      ]
     },
     "execution_count": 84,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "CDR.applique(CPLE_M).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 85,
   "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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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": 86,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f (f x)))\n",
      "  1: ---> (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f (f x)))\n",
      "  2: ---> (λc.(c λx.λy.x) ((λf.λx.(f (f x)) λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))\n",
      "  3: ---> (((λf.λx.(f (f x)) λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
      "  4: ---> ((λx.(λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
      "  5: ---> ((λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λx.λy.x)\n",
      "  6: ---> (((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) λx.λy.x)\n",
      "  7: ---> ((λy.λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) λx.λy.x)\n",
      "  8: ---> (λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) λx.λy.x)\n",
      "  9: ---> (((λc.λa.λs.((c a) s) λx.λy.x) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 10: ---> ((λa.λs.((λx.λy.x a) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 11: ---> (λs.((λx.λy.x (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) s) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 12: ---> ((λx.λy.x (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 13: ---> (λy.(λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 14: ---> (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))\n",
      " 15: ---> ((λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.y)\n",
      " 16: ---> (((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λx.λy.y)\n",
      " 17: ---> ((λy.λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λx.λy.y)\n",
      " 18: ---> (λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λx.λy.y)\n",
      " 19: ---> (((λc.λa.λs.((c a) s) λx.λy.y) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))\n",
      " 20: ---> ((λa.λs.((λx.λy.y a) s) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))\n",
      " 21: ---> (λs.((λx.λy.y (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) s) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))\n",
      " 22: ---> ((λx.λy.y (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))\n",
      " 23: ---> (λy.y (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))\n",
      " 24: ---> (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))\n",
      " 25: ---> λf.λx.(f (((λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) f) x))\n",
      " 26: ---> λf.λx.(f (((((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x) λx.λy.y) f) x))\n",
      " 27: ---> λf.λx.(f ((((λy.λs.(((λc.λa.λs.((c a) s) s) λf.λx.x) y) λf.λx.x) λx.λy.y) f) x))\n",
      " 28: ---> λf.λx.(f (((λs.(((λc.λa.λs.((c a) s) s) λf.λx.x) λf.λx.x) λx.λy.y) f) x))\n",
      " 29: ---> λf.λx.(f (((((λc.λa.λs.((c a) s) λx.λy.y) λf.λx.x) λf.λx.x) f) x))\n",
      " 30: ---> λf.λx.(f ((((λa.λs.((λx.λy.y a) s) λf.λx.x) λf.λx.x) f) x))\n",
      " 31: ---> λf.λx.(f (((λs.((λx.λy.y λf.λx.x) s) λf.λx.x) f) x))\n",
      " 32: ---> λf.λx.(f ((((λx.λy.y λf.λx.x) λf.λx.x) f) x))\n",
      " 33: ---> λf.λx.(f (((λy.y λf.λx.x) f) x))\n",
      " 34: ---> λf.λx.(f ((λf.λx.x f) x))\n",
      " 35: ---> λf.λx.(f (λx.x x))\n",
      " 36: ---> λf.λx.(f x)\n",
      "Forme normale calculée : λf.λx.(f x)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 86,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "PRED.applique(DEUX).forme_normale(verbose=True) == UN"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 87,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.x)\n",
      "  1: ---> (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.x)\n",
      "  2: ---> (λc.(c λx.λy.x) ((λf.λx.x λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))\n",
      "  3: ---> (((λf.λx.x λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
      "  4: ---> ((λx.x ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
      "  5: ---> (((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x) λx.λy.x)\n",
      "  6: ---> ((λy.λs.(((λc.λa.λs.((c a) s) s) λf.λx.x) y) λf.λx.x) λx.λy.x)\n",
      "  7: ---> (λs.(((λc.λa.λs.((c a) s) s) λf.λx.x) λf.λx.x) λx.λy.x)\n",
      "  8: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λf.λx.x) λf.λx.x)\n",
      "  9: ---> ((λa.λs.((λx.λy.x a) s) λf.λx.x) λf.λx.x)\n",
      " 10: ---> (λs.((λx.λy.x λf.λx.x) s) λf.λx.x)\n",
      " 11: ---> ((λx.λy.x λf.λx.x) λf.λx.x)\n",
      " 12: ---> (λy.λf.λx.x λf.λx.x)\n",
      " 13: ---> λf.λx.x\n",
      "Forme normale calculée : λf.λx.x\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 87,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "PRED.applique(ZERO).forme_normale(verbose=True) == ZERO"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 88,
   "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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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": 89,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) λf.λx.(f (f (f x)))) λf.λx.(f x))\n",
      "  1: ---> ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) λf.λx.(f (f (f x)))) λf.λx.(f x))\n",
      "  2: ---> (λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λf.λx.(f (f (f x)))) λf.λx.(f x))\n",
      "  3: ---> ((λf.λx.(f x) λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λf.λx.(f (f (f x))))\n",
      "  4: ---> (λx.(λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) x) λf.λx.(f (f (f x))))\n",
      "  5: ---> (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f (f (f x))))\n",
      "  6: ---> (λc.(c λx.λy.x) ((λf.λx.(f (f (f x))) λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))\n",
      "  7: ---> (((λf.λx.(f (f (f x))) λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
      "  8: ---> ((λx.(λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
      "  9: ---> ((λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λx.λy.x)\n",
      " 10: ---> (((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))) λx.λy.x)\n",
      " 11: ---> ((λy.λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))) λx.λy.x)\n",
      " 12: ---> (λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))) λx.λy.x)\n",
      " 13: ---> (((λc.λa.λs.((c a) s) λx.λy.x) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))))\n",
      " 14: ---> ((λa.λs.((λx.λy.x a) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))))\n",
      " 15: ---> (λs.((λx.λy.x (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) s) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))))\n",
      " 16: ---> ((λx.λy.x (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))))\n",
      " 17: ---> (λy.(λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))))\n",
      " 18: ---> (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))\n",
      " 19: ---> ((λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λx.λy.y)\n",
      " 20: ---> (((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) λx.λy.y)\n",
      " 21: ---> ((λy.λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) λx.λy.y)\n",
      " 22: ---> (λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) λx.λy.y)\n",
      " 23: ---> (((λc.λa.λs.((c a) s) λx.λy.y) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 24: ---> ((λa.λs.((λx.λy.y a) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 25: ---> (λs.((λx.λy.y (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) s) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 26: ---> ((λx.λy.y (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 27: ---> (λy.y (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 28: ---> (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))\n",
      " 29: ---> λf.λx.(f (((λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) f) x))\n",
      " 30: ---> λf.λx.(f ((((λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.y) f) x))\n",
      " 31: ---> λf.λx.(f (((((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λx.λy.y) f) x))\n",
      " 32: ---> λf.λx.(f ((((λy.λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λx.λy.y) f) x))\n",
      " 33: ---> λf.λx.(f (((λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λx.λy.y) f) x))\n",
      " 34: ---> λf.λx.(f (((((λc.λa.λs.((c a) s) λx.λy.y) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) f) x))\n",
      " 35: ---> λf.λx.(f ((((λa.λs.((λx.λy.y a) s) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) f) x))\n",
      " 36: ---> λf.λx.(f (((λs.((λx.λy.y (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) s) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) f) x))\n",
      " 37: ---> λf.λx.(f ((((λx.λy.y (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) f) x))\n",
      " 38: ---> λf.λx.(f (((λy.y (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) f) x))\n",
      " 39: ---> λf.λx.(f (((λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) f) x))\n",
      " 40: ---> λf.λx.(f ((λf.λx.(f (((λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) f) x)) f) x))\n",
      " 41: ---> λf.λx.(f (λx.(f (((λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) f) x)) x))\n",
      " 42: ---> λf.λx.(f (f (((λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) f) x)))\n",
      " 43: ---> λf.λx.(f (f (((((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x) λx.λy.y) f) x)))\n",
      " 44: ---> λf.λx.(f (f ((((λy.λs.(((λc.λa.λs.((c a) s) s) λf.λx.x) y) λf.λx.x) λx.λy.y) f) x)))\n",
      " 45: ---> λf.λx.(f (f (((λs.(((λc.λa.λs.((c a) s) s) λf.λx.x) λf.λx.x) λx.λy.y) f) x)))\n",
      " 46: ---> λf.λx.(f (f (((((λc.λa.λs.((c a) s) λx.λy.y) λf.λx.x) λf.λx.x) f) x)))\n",
      " 47: ---> λf.λx.(f (f ((((λa.λs.((λx.λy.y a) s) λf.λx.x) λf.λx.x) f) x)))\n",
      " 48: ---> λf.λx.(f (f (((λs.((λx.λy.y λf.λx.x) s) λf.λx.x) f) x)))\n",
      " 49: ---> λf.λx.(f (f ((((λx.λy.y λf.λx.x) λf.λx.x) f) x)))\n",
      " 50: ---> λf.λx.(f (f (((λy.y λf.λx.x) f) x)))\n",
      " 51: ---> λf.λx.(f (f ((λf.λx.x f) x)))\n",
      " 52: ---> λf.λx.(f (f (λx.x x)))\n",
      " 53: ---> λf.λx.(f (f x))\n",
      "Forme normale calculée : λf.λx.(f (f x))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 89,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "SUB.applique(TROIS).applique(UN).forme_normale(verbose=True) == DEUX"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 90,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λn.λm.(NUL ((SUB 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)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 91,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 91,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "INF.applique(TROIS).applique(UN).forme_normale() == FAUX"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 92,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 92,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "INF.applique(UN).applique(TROIS).forme_normale() == VRAI"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 93,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 93,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "INF.applique(UN).applique(UN).forme_normale() == VRAI"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 94,
   "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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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": 95,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 95,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "EGAL.applique(UN).applique(UN).forme_normale() == VRAI"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 96,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 96,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "EGAL.applique(UN).applique(DEUX).forme_normale() == FAUX"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Itération"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 97,
   "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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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": 98,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 98,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv1.applique(ZERO).forme_normale() == UN"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 99,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 99,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv1.applique(UN).forme_normale() == UN"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 100,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "None\n"
     ]
    }
   ],
   "source": [
    "print(FACTv1.applique(DEUX).forme_normale())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 101,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 101,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv1.applique(DEUX).forme_normale(nb_etapes_max=118) == DEUX"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 102,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 102,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv1.applique(TROIS).forme_normale(nb_etapes_max=403) == SIX"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 103,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 103,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv1.applique(QUATRE).forme_normale(nb_etapes_max=1672) == MUL.applique(QUATRE).applique(SIX).forme_normale()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Et la récursivité ? "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 104,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λn.(((IF ((EGAL n) ZERO)) UN) ((MUL n) (f (PRED n))))\n",
      "λf.λn.(((λc.λa.λs.((c a) s) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) n) λf.λx.x)) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) n) (f (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) n))))\n"
     ]
    }
   ],
   "source": [
    "M_PHI_FACT = Lambda_terme('!f.!n.(((IF ((EGAL n) ZERO)) UN) ((MUL n) (f (PRED n))))')\n",
    "print(M_PHI_FACT)\n",
    "PHI_FACT = M_PHI_FACT.subs('IF', IF).subs('EGAL', EGAL).subs('ZERO', ZERO).subs('UN', UN).subs('MUL', MUL).subs('PRED', PRED)\n",
    "print(PHI_FACT)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 105,
   "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": 106,
   "metadata": {},
   "outputs": [],
   "source": [
    "FACT0 = PHI_FACT.applique(BOTTOM)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 107,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 107,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACT0.applique(ZERO).forme_normale() == UN"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 108,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λf.λn.(((λc.λa.λs.((c a) s) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) n) λf.λx.x)) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) n) (f (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) n)))) λy.(λx.(x x) λx.(x x))) λf.λx.(f x))\n",
      "  1: ---> ((λf.λn.(((λc.λa.λs.((c a) s) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) n) λf.λx.x)) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) n) (f (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) n)))) λy.(λx.(x x) λx.(x x))) λf.λx.(f x))\n",
      "  2: ---> (λn.(((λc.λa.λs.((c a) s) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) n) λf.λx.x)) λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) n)))) λf.λx.(f x))\n",
      "  3: ---> (((λc.λa.λs.((c a) s) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) λf.λx.(f x)) λf.λx.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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      "  4: ---> ((λa.λs.((((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) λf.λx.(f x)) λf.λx.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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      "  5: ---> (λs.((((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) λf.λx.(f x)) λf.λx.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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      "  6: ---> ((((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) λf.λx.(f x)) λf.λx.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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      "  7: ---> (((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.(f x)) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) λf.λx.(f x))) λf.λx.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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      "  8: ---> ((((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.(f x)) λf.λx.x)) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      "  9: ---> (((λb.(((λc.λa.λs.((c a) s) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.(f x)) λf.λx.x)) 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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 10: ---> (((((λc.λa.λs.((c a) s) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.(f x)) λf.λx.x)) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 11: ---> ((((λa.λs.((((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.(f x)) λf.λx.x) a) s) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 12: ---> (((λs.((((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.(f x)) λf.λx.x) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) s) λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 13: ---> ((((((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.(f x)) λf.λx.x) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 14: ---> (((((λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) λf.λx.(f x)) m)) λf.λx.x) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 15: ---> (((((λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) λf.λx.(f x)) λf.λx.x)) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 16: ---> ((((((((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) λf.λx.(f x)) λf.λx.x) λx.λx.λy.y) λx.λy.x) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 17: ---> (((((((λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λf.λx.(f x)) λf.λx.x) λx.λx.λy.y) λx.λy.x) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 18: ---> ((((((((λf.λx.x λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λf.λx.(f x)) λx.λx.λy.y) λx.λy.x) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 19: ---> (((((((λx.x λf.λx.(f x)) λx.λx.λy.y) λx.λy.x) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 20: ---> ((((((λf.λx.(f x) λx.λx.λy.y) λx.λy.x) ((λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λ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.(((λc.λa.λs.((c a) 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.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      "Pas de forme normale atteinte après 20 étapes de réduction\n"
     ]
    }
   ],
   "source": [
    "FACT0.applique(UN).forme_normale(verbose=True, nb_etapes_max=20)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 109,
   "metadata": {},
   "outputs": [],
   "source": [
    "FACT1 = PHI_FACT.applique(FACT0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 110,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 110,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACT1.applique(ZERO).forme_normale() == UN"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 111,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 111,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACT1.applique(UN).forme_normale(nb_etapes_max=110) == UN"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 112,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.(λx.(f (x x)) λx.(f (x x)))\n"
     ]
    }
   ],
   "source": [
    "FIX_CURRY = Lambda_terme('!f.(!x.(f (x x)) !x.(f (x x)))')\n",
    "print(FIX_CURRY)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 113,
   "metadata": {},
   "outputs": [],
   "source": [
    "FACTv2 = FIX_CURRY.applique(PHI_FACT)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 114,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 114,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv2.applique(ZERO).forme_normale() == UN"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 115,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 115,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv2.applique(UN).forme_normale(nb_etapes_max=113) == UN"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 116,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 116,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv2.applique(DEUX).forme_normale(nb_etapes_max=516) == DEUX"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 117,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 117,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv2.applique(TROIS).forme_normale(nb_etapes_max=2882) == SIX"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 118,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 118,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv2.applique(QUATRE).forme_normale(nb_etapes_max=18668) == MUL.applique(QUATRE).applique(SIX).forme_normale()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 119,
   "metadata": {},
   "outputs": [],
   "source": [
    "PF = FIX_CURRY.applique(Lambda_terme('M'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 120,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λf.(λx.(f (x x)) λx.(f (x x))) M)\n",
      "  1: ---> (λf.(λx.(f (x x)) λx.(f (x x))) M)\n",
      "  2: ---> (λx.(M (x x)) λx.(M (x x)))\n",
      "  3: ---> (M (λx.(M (x x)) λx.(M (x x))))\n",
      "  4: ---> (M (M (λx.(M (x x)) λx.(M (x x)))))\n",
      "  5: ---> (M (M (M (λx.(M (x x)) λx.(M (x x))))))\n",
      "  6: ---> (M (M (M (M (λx.(M (x x)) λx.(M (x x)))))))\n",
      "  7: ---> (M (M (M (M (M (λx.(M (x x)) λx.(M (x x))))))))\n",
      "  8: ---> (M (M (M (M (M (M (λx.(M (x x)) λx.(M (x x)))))))))\n",
      "  9: ---> (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 (λ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": "code",
   "execution_count": 121,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λx.λy.(y ((x x) y)) λx.λy.(y ((x x) y)))\n"
     ]
    }
   ],
   "source": [
    "FIX_TURING = Lambda_terme('(!x.!y.(y ((x x) y)) !x.!y.(y ((x x) y)))')\n",
    "print(FIX_TURING)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 122,
   "metadata": {},
   "outputs": [],
   "source": [
    "FACTv3 = FIX_TURING.applique(PHI_FACT)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 123,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 123,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv3.applique(ZERO).forme_normale() == UN"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 124,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 124,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv3.applique(UN).forme_normale(nb_etapes_max=114) == UN"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 125,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 125,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv3.applique(DEUX).forme_normale(nb_etapes_max=520) == DEUX"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 126,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 126,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv3.applique(TROIS).forme_normale(nb_etapes_max=2897) == SIX"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 127,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 127,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FACTv3.applique(QUATRE).forme_normale(nb_etapes_max=18732) == MUL.applique(QUATRE).applique(SIX).forme_normale()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "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": {},
   "source": [
    "## Les booléens"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 128,
   "metadata": {},
   "outputs": [],
   "source": [
    "vrai = lambda x: lambda y: x\n",
    "faux = lambda x: lambda y: y"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 129,
   "metadata": {},
   "outputs": [],
   "source": [
    "def booleen_en_bool(b):\n",
    "    return b(True)(False)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 130,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(True, False)"
      ]
     },
     "execution_count": 130,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(booleen_en_bool(b) for b in (vrai, faux))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 131,
   "metadata": {},
   "outputs": [],
   "source": [
    "If = lambda c: lambda a: lambda s: c(a)(s) "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 132,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "1"
      ]
     },
     "execution_count": 132,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "If(vrai)(1)(2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 133,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "2"
      ]
     },
     "execution_count": 133,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "If(faux)(1)(2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 134,
   "metadata": {},
   "outputs": [],
   "source": [
    "#If(vrai)(1)(1/0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 135,
   "metadata": {},
   "outputs": [],
   "source": [
    "non = lambda b: If(b)(faux)(vrai)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 136,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(False, True)"
      ]
     },
     "execution_count": 136,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(booleen_en_bool(non(b)) for b in (vrai, faux))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 137,
   "metadata": {},
   "outputs": [],
   "source": [
    "et = lambda b1: lambda b2: If(b1)(b2)(faux)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 138,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(True, False, False, False)"
      ]
     },
     "execution_count": 138,
     "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": 139,
   "metadata": {},
   "outputs": [],
   "source": [
    "ou = lambda b1: lambda b2: If(b1)(vrai)(b2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 140,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(True, True, True, False)"
      ]
     },
     "execution_count": 140,
     "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": {},
   "source": [
    "## Les entiers de Church"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 141,
   "metadata": {},
   "outputs": [],
   "source": [
    "zero = lambda f: lambda x: x"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 142,
   "metadata": {},
   "outputs": [],
   "source": [
    "un = lambda f: lambda x: f(x)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 143,
   "metadata": {},
   "outputs": [],
   "source": [
    "deux = lambda f: lambda x: f(f(x))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 144,
   "metadata": {},
   "outputs": [],
   "source": [
    "trois = lambda f: lambda x: f(f(f(x)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 145,
   "metadata": {},
   "outputs": [],
   "source": [
    "def entier_church_en_int(ec):\n",
    "    return ec(lambda n: n+1)(0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 146,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(0, 1, 2, 3)"
      ]
     },
     "execution_count": 146,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(entier_church_en_int(n) for n in (zero, un, deux, trois))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 147,
   "metadata": {},
   "outputs": [],
   "source": [
    "suc = lambda n: lambda f: lambda x: f(n(f)(x))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 148,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(1, 2, 3, 4)"
      ]
     },
     "execution_count": 148,
     "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": 149,
   "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": 150,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)"
      ]
     },
     "execution_count": 150,
     "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": 151,
   "metadata": {},
   "outputs": [],
   "source": [
    "add = lambda n: lambda m: lambda f: lambda x: n(f)(m(f)(x))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 152,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "5"
      ]
     },
     "execution_count": 152,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "cinq = add(deux)(trois)\n",
    "entier_church_en_int(cinq)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 153,
   "metadata": {},
   "outputs": [],
   "source": [
    "mul = lambda n: lambda m: lambda f: n(m(f))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 154,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "6"
      ]
     },
     "execution_count": 154,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "six = mul(deux)(trois)\n",
    "entier_church_en_int(six)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 155,
   "metadata": {},
   "outputs": [],
   "source": [
    "exp = lambda n: lambda m: m(n)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 156,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "8"
      ]
     },
     "execution_count": 156,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "huit = exp(deux)(trois)\n",
    "entier_church_en_int(huit)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 157,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "9"
      ]
     },
     "execution_count": 157,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "neuf = exp(trois)(deux)\n",
    "entier_church_en_int(neuf)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 158,
   "metadata": {},
   "outputs": [],
   "source": [
    "est_nul = lambda n : n(lambda x: faux)(vrai)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 159,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(True, False, False, False, False, False, False)"
      ]
     },
     "execution_count": 159,
     "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": {},
   "source": [
    "## Les couples"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 160,
   "metadata": {},
   "outputs": [],
   "source": [
    "cons = lambda x: lambda y: lambda z: z(x)(y)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 161,
   "metadata": {},
   "outputs": [],
   "source": [
    "un_deux = cons(un)(deux)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 162,
   "metadata": {},
   "outputs": [],
   "source": [
    "car = lambda c: c(vrai)\n",
    "cdr = lambda c: c(faux)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 163,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(1, 2)"
      ]
     },
     "execution_count": 163,
     "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": 164,
   "metadata": {},
   "outputs": [],
   "source": [
    "pred = lambda n: car(n(lambda c: cons(cdr(c))(suc(cdr(c))))(cons(zero)(zero)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 165,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(0, 0, 1, 2, 3, 4, 5, 6, 7, 8)"
      ]
     },
     "execution_count": 165,
     "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": 166,
   "metadata": {},
   "outputs": [],
   "source": [
    "sub = lambda n: lambda m: m(pred)(n)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 167,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "5"
      ]
     },
     "execution_count": 167,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entier_church_en_int(sub(huit)(trois))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 168,
   "metadata": {},
   "outputs": [],
   "source": [
    "est_inf_ou_egal = lambda n: lambda m: est_nul(sub(m)(n))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 169,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(True, True, True, True, True, True, False, False, False, False)"
      ]
     },
     "execution_count": 169,
     "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": 170,
   "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": 171,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(False, False, False, False, False, True, False, False, False, False)"
      ]
     },
     "execution_count": 171,
     "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": {},
   "source": [
    "## Itération"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 172,
   "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": 173,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(1, 1, 2, 6, 24, 120, 720)"
      ]
     },
     "execution_count": 173,
     "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": {},
   "source": [
    "## Combinateur de point fixe"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 174,
   "metadata": {},
   "outputs": [],
   "source": [
    "phi_fact = lambda f: lambda n: 1 if n == 0 else n*f(n-1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 175,
   "metadata": {},
   "outputs": [],
   "source": [
    "bottom = lambda x: (lambda y: y(y))(lambda y:y(y))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 176,
   "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": 177,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(1, 1, 2, 6)"
      ]
     },
     "execution_count": 177,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(f4(n) for n in range(4))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 178,
   "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": 179,
   "metadata": {},
   "outputs": [],
   "source": [
    "fact2 = phi_fact(fact_rec)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 180,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(1, 1, 2, 6, 24, 120, 720)"
      ]
     },
     "execution_count": 180,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(fact2(n) for n in range(7))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 181,
   "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": 182,
   "metadata": {},
   "outputs": [],
   "source": [
    "fact3 = fix_curry(phi_fact)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 183,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(1, 1, 2, 6, 24, 120, 720)"
      ]
     },
     "execution_count": 183,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(fact3(n) for n in range(7))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Un programme obscur"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 184,
   "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": 185,
   "metadata": {},
   "outputs": [],
   "source": [
    "phiListEnChaine = lambda x: lambda y: '' if y == [] else chr(y[0]) + x(y[1:])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 186,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'ABCDEFGHIJKLMNOPQRSTUVWXYZ'"
      ]
     },
     "execution_count": 186,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "fix_curry(phiListEnChaine)([65+k for k in range(26)])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 187,
   "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": 188,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[1, 4, 9, 16]"
      ]
     },
     "execution_count": 188,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "fix_curry(phiMap)(lambda x: x*x)([1, 2, 3, 4])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 189,
   "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": 190,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "24"
      ]
     },
     "execution_count": 190,
     "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-showcode": false,
  "toc-showmarkdowntxt": false,
  "widgets": {
   "application/vnd.jupyter.widget-state+json": {
    "state": {},
    "version_major": 2,
    "version_minor": 0
   }
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}