{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "\n",
    "#  $\\lambda$-calcul"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
   },
   "source": [
    "## Analyseur lexical"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from sly import Lexer"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 56,
   "metadata": {},
   "outputs": [],
   "source": [
    "class LambdaSyntaxError(Exception):\n",
    "    def __init__(self, msg):\n",
    "        self.message = msg"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 61,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Lambda_lexer(Lexer):\n",
    "    tokens = {VAR, LPAR, RPAR, LAMBDA, POINT}\n",
    "    VAR = r'[a-zA-Z][a-zA-Z0-9]*'\n",
    "    LPAR = r'\\('\n",
    "    RPAR = r'\\)'\n",
    "    LAMBDA = r'\\!|λ'\n",
    "    POINT = r'\\.'\n",
    "    ignore = ' \\t'\n",
    "    \n",
    "    # Define a rule so we can track line numbers\n",
    "    @_(r'\\n+')\n",
    "    def ignore_newline(self, t):\n",
    "        self.lineno += len(t.value)\n",
    "        \n",
    "    def error(self, t):\n",
    "        raise LambdaSyntaxError('Caractère illégal : {:s} at position {:d}'.format(t.value[0], t.index))\n",
    "        self.index += 1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 62,
   "metadata": {},
   "outputs": [],
   "source": [
    "lexer = Lambda_lexer()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 63,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[Token(type='LPAR', value='(', lineno=1, index=0),\n",
       " Token(type='LPAR', value='(', lineno=1, index=1),\n",
       " Token(type='LAMBDA', value='!', lineno=1, index=2),\n",
       " Token(type='VAR', value='x', lineno=1, index=3),\n",
       " Token(type='POINT', value='.', lineno=1, index=4),\n",
       " Token(type='LPAR', value='(', lineno=1, index=5),\n",
       " Token(type='VAR', value='x', lineno=1, index=6),\n",
       " Token(type='VAR', value='x', lineno=1, index=8),\n",
       " Token(type='RPAR', value=')', lineno=1, index=9),\n",
       " Token(type='VAR', value='y', lineno=1, index=11),\n",
       " Token(type='RPAR', value=')', lineno=1, index=12),\n",
       " Token(type='LAMBDA', value='λ', lineno=2, index=14),\n",
       " Token(type='VAR', value='x', lineno=2, index=15),\n",
       " Token(type='POINT', value='.', lineno=2, index=16),\n",
       " Token(type='VAR', value='y', lineno=2, index=17),\n",
       " Token(type='RPAR', value=')', lineno=2, index=18)]"
      ]
     },
     "execution_count": 63,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "l = list(lexer.tokenize('''((!x.(x x) y)\n",
    "λx.y)'''))\n",
    "l"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 64,
   "metadata": {},
   "outputs": [
    {
     "ename": "LambdaSyntaxError",
     "evalue": "Caractère illégal : [ at position 3",
     "output_type": "error",
     "traceback": [
      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[0;31mLambdaSyntaxError\u001b[0m                         Traceback (most recent call last)",
      "\u001b[0;32m<ipython-input-64-43a42386c386>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mlist\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mlexer\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtokenize\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m'!x.[y z]'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[0;32m/usr/local/lib/python3.7/dist-packages/sly/lex.py\u001b[0m in \u001b[0;36mtokenize\u001b[0;34m(self, text, lineno, index)\u001b[0m\n\u001b[1;32m    441\u001b[0m                         \u001b[0mtok\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtype\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0;34m'ERROR'\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    442\u001b[0m                         \u001b[0mtok\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mvalue\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mtext\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0mindex\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 443\u001b[0;31m                         \u001b[0mtok\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0merror\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtok\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    444\u001b[0m                         \u001b[0;32mif\u001b[0m \u001b[0mtok\u001b[0m \u001b[0;32mis\u001b[0m \u001b[0;32mnot\u001b[0m \u001b[0;32mNone\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    445\u001b[0m                             \u001b[0;32myield\u001b[0m \u001b[0mtok\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;32m<ipython-input-61-fe1a231aa5a0>\u001b[0m in \u001b[0;36merror\u001b[0;34m(self, t)\u001b[0m\n\u001b[1;32m     14\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m     15\u001b[0m     \u001b[0;32mdef\u001b[0m \u001b[0merror\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mt\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m---> 16\u001b[0;31m         \u001b[0;32mraise\u001b[0m \u001b[0mLambdaSyntaxError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m'Caractère illégal : {:s} at position {:d}'\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mt\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mvalue\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;36m0\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mt\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mindex\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m     17\u001b[0m         \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mindex\u001b[0m \u001b[0;34m+=\u001b[0m \u001b[0;36m1\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;31mLambdaSyntaxError\u001b[0m: Caractère illégal : [ at position 3"
     ]
    }
   ],
   "source": [
    "list(lexer.tokenize('!x.[y z]'))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
   },
   "source": [
    "## Analyseur syntaxique"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "lines_to_next_cell": 0
   },
   "source": [
    "Voici la grammaire du langage décrivant les $\\lambda$-termes\n",
    "\n",
    "    term ::= VAR | LAMBDA VAR POINT term | LPAR term term RPAR\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "from sly import Parser"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Lambda_parser(Parser):\n",
    "    tokens = Lambda_lexer.tokens\n",
    "    \n",
    "    @_('VAR')\n",
    "    def term(self, p):\n",
    "        return Lambda_terme(0, p[0])\n",
    "    \n",
    "    @_('LAMBDA VAR POINT term')\n",
    "    def term(self, p):\n",
    "        return Lambda_terme(1, p[1], p.term)\n",
    "    \n",
    "    @_('LPAR term term RPAR')\n",
    "    def term(self, p):\n",
    "        return Lambda_terme(2, p.term0, p.term1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "parser = Lambda_parser()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## La classe `Lambda_terme`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [],
   "source": [
    "def autre_variable(var, variables):\n",
    "    n = 0\n",
    "    while var + '{:d}'.format(n) in variables:\n",
    "        n += 1\n",
    "    return var + '{:d}'.format(n)\n",
    "\n",
    "class Lambda_terme():\n",
    "    def __init__(self, categorie, *args):\n",
    "        if categorie not in (0, 1, 2):\n",
    "            raise Exception('categorie non valide')\n",
    "        if categorie == 0: \n",
    "            if len(args) != 1 or not isinstance(args[0], str):\n",
    "                raise Exception('mauvaise construction pour une variable')\n",
    "        elif categorie == 1:\n",
    "            if len(args) != 2 or not isinstance(args[0], str) or not isinstance(args[1], Lambda_terme):\n",
    "                raise Exception('mauvaise construction pour une abstraction')\n",
    "        else:\n",
    "            if len(args) != 2 or not isinstance(args[0], Lambda_terme) or not isinstance(args[1], Lambda_terme):\n",
    "                raise Exception('mauvaise construction pour une application')\n",
    "        self._content = (categorie,) + tuple(args)\n",
    "        \n",
    "    @staticmethod\n",
    "    def cree(descr):\n",
    "        return parser.parse(lexer.tokenize(descr))\n",
    "    \n",
    "    def est_variable(self):\n",
    "        return self._content[0] == 0\n",
    "\n",
    "    def est_abstraction(self):\n",
    "        return self._content[0] == 1\n",
    "\n",
    "    def est_application(self):\n",
    "        return self._content[0] == 2\n",
    "\n",
    "    def applique(self, terme):\n",
    "        if not isinstance(terme, Lambda_terme):\n",
    "            raise Exception('Application impossible')\n",
    "        return Lambda_terme(2, self, terme)\n",
    "    \n",
    "    def abstrait(self, var):\n",
    "        if not isinstance(var, str):\n",
    "            raise Exception(\"Variable d'Abstraction invalide\")\n",
    "        return Lambda_terme(1, var, self)\n",
    "    \n",
    "    def est_redex(self):\n",
    "        return self.est_application() and self._content[1].est_abstraction()\n",
    "    \n",
    "    def est_forme_normale(self):\n",
    "        if self.est_variable():\n",
    "            return True\n",
    "        elif self.est_abstraction():\n",
    "            return self._content[2].est_forme_normale()\n",
    "        else:\n",
    "            return not self._content[1].est_abstraction() and all(self._content[k].est_forme_normale() for k in (1, 2))\n",
    "        \n",
    "    def variables_libres(self):\n",
    "        if self.est_variable():\n",
    "            return {self._content[1]}\n",
    "        elif self.est_application():\n",
    "            var_libres = self._content[2].variables_libres()\n",
    "            return var_libres.union(self._content[1].variables_libres())\n",
    "        else:\n",
    "            var_libres = self._content[2].variables_libres()\n",
    "            var_libres.discard(self._content[1])\n",
    "            return var_libres\n",
    "    \n",
    "    def subs(self, var, terme):\n",
    "        if not isinstance(var, str):\n",
    "            raise Exception('subst possible uniquement pour les variables')\n",
    "        if not isinstance(terme, Lambda_terme):\n",
    "            raise Exception('subst possible uniquement sur un lambda-terme')\n",
    "        if self.est_variable():\n",
    "            if var == self._content[1]:\n",
    "                return terme\n",
    "            else:\n",
    "                return self\n",
    "        elif self.est_application():\n",
    "            return Lambda_terme(2, self._content[1].subs(var, terme), self._content[2].subs(var, terme))\n",
    "        else:\n",
    "            var_abstr = self._content[1]\n",
    "            corps_abstr = self._content[2]\n",
    "            var_libres_corps = corps_abstr.variables_libres()\n",
    "            if var == var_abstr or var not in var_libres_corps:\n",
    "                return self\n",
    "            elif var_abstr not in terme.variables_libres():\n",
    "                return Lambda_terme(1, var_abstr, corps_abstr.subs(var, terme))\n",
    "            else:\n",
    "                nouvelle_var = autre_variable(var_abstr, corps_abstr.variables_libres())\n",
    "                return Lambda_terme(1, \n",
    "                                    nouvelle_var, \n",
    "                                    corps_abstr.subs(var_abstr, Lambda_terme(0, nouvelle_var)).subs(var, terme))\n",
    "                    \n",
    "                \n",
    "    def _reduit(self):\n",
    "        if self.est_variable():\n",
    "            return self, False\n",
    "        elif self.est_abstraction():\n",
    "            corps_reduit, est_reduit = self._content[2]._reduit()\n",
    "            return (Lambda_terme(1, self._content[1], corps_reduit) if est_reduit else self, est_reduit)\n",
    "        else:\n",
    "            termegauche = self._content[1]\n",
    "            termedroit = self._content[2]\n",
    "            if termegauche.est_abstraction():\n",
    "                var_abstr = termegauche._content[1]\n",
    "                corps = termegauche._content[2]\n",
    "                return corps.subs(var_abstr, termedroit), True\n",
    "            else:\n",
    "                termegauche_reduit, est_reduit = termegauche._reduit()\n",
    "                if est_reduit:\n",
    "                    return Lambda_terme(2, termegauche_reduit, termedroit), est_reduit\n",
    "                else:\n",
    "                    termedroit_reduit, est_reduit = termedroit._reduit()\n",
    "                    return (Lambda_terme(2, termegauche, termedroit_reduit) if est_reduit else self, est_reduit)\n",
    "                \n",
    "    def reduit(self):\n",
    "        return self._reduit()\n",
    "            \n",
    "    def __str__(self):\n",
    "        if self.est_variable():\n",
    "            return self._content[1]\n",
    "        elif self.est_abstraction():\n",
    "            return 'λ{:s}.{:s}'.format(self._content[1], str(self._content[2]))\n",
    "        else:\n",
    "            return '({:s} {:s})'.format(str(self._content[1]), str(self._content[2]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = Lambda_terme(0, \"x\")\n",
    "T2 = Lambda_terme(1, \"x\", T1)\n",
    "T3 = Lambda_terme.cree('(!x.x x)')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "x\n",
      "λx.x\n",
      "(λx.x x)\n"
     ]
    }
   ],
   "source": [
    "print(T1)\n",
    "print(T2)\n",
    "print(T3)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(True, False, False)"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(t.est_variable() for t in (T1, T2, T3))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(False, True, False)"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(t.est_abstraction() for t in (T1, T2, T3))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(False, False, True)"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(t.est_application() for t in (T1, T2, T3))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(False, False, True)"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(t.est_redex() for t in (T1, T2, T3))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(True, True, False)"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(t.est_forme_normale() for t in (T1, T2, T3))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "({'x'}, set(), {'x'})"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(t.variables_libres() for t in (T1, T2, T3))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "x --> x\n",
      "x --> (y x)\n"
     ]
    }
   ],
   "source": [
    "print(T1, '-->', T1.subs('y', Lambda_terme.cree('(y x)')))\n",
    "print(T1, '-->', T1.subs('x', Lambda_terme.cree('(y x)')))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λx.y --> λx.y\n",
      "λx.y --> λx.(t z)\n",
      "λx.y --> λx0.(x z)\n"
     ]
    }
   ],
   "source": [
    "T4 = Lambda_terme.cree('!x.y')\n",
    "print(T4, '-->', T4.subs('x', Lambda_terme.cree('(y z)')))\n",
    "print(T4, '-->', T4.subs('y', Lambda_terme.cree('(t z)')))\n",
    "print(T4, '-->', T4.subs('y', Lambda_terme.cree('(x z)')))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λx.x x) --> (λx.x x)\n",
      "(λx.x x) --> (λx.x (y x))\n"
     ]
    }
   ],
   "source": [
    "print(T3, '-->', T3.subs('y', Lambda_terme.cree('(y x)')))\n",
    "print(T3, '-->', T3.subs('x', Lambda_terme.cree('(y x)')))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [],
   "source": [
    "OMEGA = Lambda_terme.cree('(!x.(x x) !x.(x x))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λx.(x x) λx.(x x))\n"
     ]
    }
   ],
   "source": [
    "print(OMEGA)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "OMEGA.est_redex()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 23,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "OMEGA.est_forme_normale()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "set()"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "OMEGA.variables_libres()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λx.(x x) λx.(x x))\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "res, est_red = OMEGA.reduit()\n",
    "print(res)\n",
    "print(est_red)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(eric vero) True\n"
     ]
    }
   ],
   "source": [
    "res, est_red = Lambda_terme.cree('(!x.(eric x) vero)').reduit()\n",
    "print(res, est_red)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [],
   "source": [
    "def calcul(lambda_terme, nb_etapes_max=100, verbose=False):\n",
    "    etape = 0\n",
    "    forme_normale_atteinte = False\n",
    "    if verbose: print(lambda_terme)\n",
    "    while not forme_normale_atteinte and etape < nb_etapes_max:\n",
    "        etape += 1\n",
    "        terme_reduit, est_reduit = lambda_terme.reduit()\n",
    "        if verbose: print('{:3d}: ---> {:s}'.format(etape, str(lambda_terme), str(terme_reduit)))\n",
    "        forme_normale_atteinte = not est_reduit\n",
    "        lambda_terme = terme_reduit\n",
    "    if forme_normale_atteinte:\n",
    "        if verbose: print('Forme normale calculée : {:s}'.format(str(terme_reduit)))\n",
    "        return terme_reduit\n",
    "    else:\n",
    "        if verbose: print('Pas de forme normale atteinte après {:d} étapes de réduction'.format(etape))\n",
    "        return None"
   ]
  },
  {
   "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": [
    "calcul(OMEGA, nb_etapes_max=10, verbose=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Entiers, successeurs, addition, multiplication et exponentiation"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [],
   "source": [
    "ZERO = Lambda_terme.cree('!f.!x.x')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [],
   "source": [
    "UN = Lambda_terme.cree('!f.!x.(f x)')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "metadata": {},
   "outputs": [],
   "source": [
    "DEUX = Lambda_terme.cree('!f.!x.(f (f x))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "metadata": {},
   "outputs": [],
   "source": [
    "SUC = Lambda_terme.cree('!n.!f.!x.(f ((n f) x))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "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 = calcul(SUC.applique(DEUX), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "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": [
       "<__main__.Lambda_terme at 0x7f6ff4374cc0>"
      ]
     },
     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "calcul(TROIS.applique(SUC).applique(ZERO), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "ADD = Lambda_terme.cree('!n.!m.!f.!x.((n f) ((m f) x))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "QUATRE = calcul(ADD.applique(UN).applique(TROIS), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "CINQ = calcul(ADD.applique(TROIS).applique(DEUX), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "SEPT = calcul(ADD.applique(QUATRE).applique(TROIS), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "MUL = Lambda_terme.cree('!n.!m.!f.(n (m f))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "SIX = calcul(MUL.applique(DEUX).applique(TROIS), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "EXP = Lambda_terme.cree('!n.!m.(m n)')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "HUIT = calcul(EXP.applique(DEUX).applique(TROIS), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "NEUF = calcul(EXP.applique(TROIS).applique(DEUX), verbose=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Booléens, opérateurs logiques et conditionnelles"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "VRAI = Lambda_terme.cree('!x.!y.x')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "FAUX = Lambda_terme.cree('!x.!y.y')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "COND = Lambda_terme.cree('!c.!a.!s.((c a) s)') "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(COND.applique(VRAI).applique(UN).applique(DEUX), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(COND.applique(FAUX).applique(UN).applique(DEUX), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "ET = COND.applique(Lambda_terme.cree('a')).applique(Lambda_terme.cree('b')).applique(FAUX).abstrait('b').abstrait('a')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(ET)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(ET.applique(VRAI).applique(VRAI), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(ET.applique(VRAI).applique(FAUX), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(ET.applique(FAUX).applique(VRAI), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(ET.applique(FAUX).applique(FAUX), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "OU = COND.applique(Lambda_terme.cree('a')).applique(VRAI).applique(Lambda_terme.cree('b')).abstrait('b').abstrait('a')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(OU.applique(VRAI).applique(VRAI), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(OU.applique(VRAI).applique(FAUX), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(OU.applique(FAUX).applique(VRAI), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(OU.applique(FAUX).applique(FAUX), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "NON = COND.applique(Lambda_terme.cree('a')).applique(FAUX).applique(VRAI).abstrait('a')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(NON.applique(VRAI), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(NON.applique(FAUX), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "NUL = Lambda_terme.cree('!n.((n !x.{:s}) {:s})'.format(str(FAUX), str(VRAI)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(NUL)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(NUL.applique(ZERO), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(NUL.applique(TROIS), verbose=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Couples"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "CONS = COND.applique(Lambda_terme.cree('s')).applique(Lambda_terme.cree('x')).applique(Lambda_terme.cree('y')).abstrait('s').abstrait('y').abstrait('x')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(CONS)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "UN_DEUX = calcul(CONS.applique(UN).applique(DEUX), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "CAR = Lambda_terme.cree('c').applique(VRAI).abstrait('c')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(CAR)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(CAR.applique(UN_DEUX), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "CDR = Lambda_terme.cree('c').applique(FAUX).abstrait('c')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(CDR.applique(UN_DEUX), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "M_PRED = Lambda_terme.cree('!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": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(PRED.applique(DEUX), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(PRED.applique(ZERO), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "M_SUB = Lambda_terme.cree('!n.!m.((m PRED) n)')\n",
    "print(M_SUB)\n",
    "SUB = M_SUB.subs('PRED', PRED)\n",
    "print(SUB)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(SUB.applique(TROIS).applique(UN), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "M_INF = Lambda_terme.cree('!n.!m.(NUL ((SUB m) n))')\n",
    "print(M_INF)\n",
    "INF = M_INF.subs('NUL', NUL).subs('SUB', SUB)\n",
    "#lambda n: lambda m: est_nul(sub(m)(n))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(INF.applique(TROIS).applique(UN), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(INF.applique(UN).applique(TROIS), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(INF.applique(UN).applique(UN), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "M_EGAL = Lambda_terme.cree('!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": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(EGAL.applique(UN).applique(UN)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(EGAL.applique(UN).applique(DEUX)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Itération"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "M_FACTv1 = Lambda_terme.cree('!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": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(FACTv1.applique(ZERO)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(FACTv1.applique(UN)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(FACTv1.applique(DEUX)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(FACTv1.applique(DEUX), nb_etapes_max=200))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(FACTv1.applique(TROIS), nb_etapes_max=500))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(FACTv1.applique(QUATRE), nb_etapes_max=1700))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Et la récursivité ? "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "M_PHI_FACT = Lambda_terme.cree('!f.!n.(((COND ((EGAL n) ZERO)) UN) ((MUL n) (f (PRED n))))')\n",
    "print(M_PHI_FACT)\n",
    "PHI_FACT = M_PHI_FACT.subs('COND', COND).subs('EGAL', EGAL).subs('ZERO', ZERO).subs('UN', UN).subs('MUL', MUL).subs('PRED', PRED)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "BOTTOM = Lambda_terme.cree('!y.OMEGA').subs('OMEGA', OMEGA)\n",
    "print(BOTTOM)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "FACT0 = PHI_FACT.applique(BOTTOM)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(FACT0.applique(ZERO)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(FACT0.applique(UN), verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "FACT1 = PHI_FACT.applique(FACT0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(FACT1.applique(ZERO)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(FACT1.applique(UN), nb_etapes_max=200))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "FIX_CURRY = Lambda_terme.cree('!f.(!x.(f (x x)) !x.(f (x x)))')\n",
    "print(FIX_CURRY)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "FACTv2 = FIX_CURRY.applique(PHI_FACT)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(FACTv2.applique(ZERO)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(FACTv2.applique(UN), nb_etapes_max=200))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(FACTv2.applique(DEUX), nb_etapes_max=700))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(FACTv2.applique(TROIS), nb_etapes_max=4000))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(calcul(FACTv2.applique(QUATRE), nb_etapes_max=25000))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "PF = FIX_CURRY.applique(Lambda_terme.cree('M'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "calcul(PF, verbose=True, nb_etapes_max=10)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "lines_to_next_cell": 2
   },
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# $\\lambda$-calcul avec les lambda-expressions de Python"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
   },
   "source": [
    "## Les entiers de Church"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "zero = lambda f: lambda x: x"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "un = lambda f: lambda x: f(x)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "deux = lambda f: lambda x: f(f(x))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "trois = lambda f: lambda x: f(f(f(x)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def entier_church_en_int(ec):\n",
    "    return ec(lambda n: n+1)(0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(entier_church_en_int(n) for n in (zero, un, deux, trois))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "suc = lambda n: lambda f: lambda x: f(n(f)(x))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(entier_church_en_int(suc(n)) for n in (zero, un, deux, trois)) "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "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": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(entier_church_en_int(int_en_entier_church(n)) for n in range(10))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "add = lambda n: lambda m: lambda f: lambda x: n(f)(m(f)(x))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cinq = add(deux)(trois)\n",
    "entier_church_en_int(cinq)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "mul = lambda n: lambda m: lambda f: n(m(f))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "six = mul(deux)(trois)\n",
    "entier_church_en_int(six)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "exp = lambda n: lambda m: m(n)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "huit = exp(deux)(trois)\n",
    "entier_church_en_int(huit)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
   },
   "source": [
    "## Les booléens"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "vrai = lambda x: lambda y: x\n",
    "faux = lambda x: lambda y: y"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def booleen_en_bool(b):\n",
    "    return b(True)(False)\n",
    "    "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(booleen_en_bool(b) for b in (vrai, faux))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cond = lambda c: lambda a: lambda s: c(a)(s) "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cond(vrai)(1)(2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cond(faux)(1)(2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cond(vrai)(1)(1/0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "non = lambda b: cond(b)(faux)(vrai)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(booleen_en_bool(non(b)) for b in (vrai, faux))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "et = lambda b1: lambda b2: cond(b1)(b2)(faux)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(booleen_en_bool(et(b1)(b2)) for b1 in (vrai, faux) for b2 in (vrai, faux))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "ou = lambda b1: lambda b2: cond(b1)(vrai)(b2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(booleen_en_bool(ou(b1)(b2)) for b1 in (vrai, faux) for b2 in (vrai, faux))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "est_nul = lambda n : n(lambda x: faux)(vrai)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(booleen_en_bool(est_nul(n)) for n in (zero, un, deux, trois, cinq, six, huit))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Les couples"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cons = lambda x: lambda y: lambda z: z(x)(y)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "un_deux = cons(un)(deux)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "car = lambda c: c(vrai)\n",
    "cdr = lambda c: c(faux)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "entier_church_en_int(car(un_deux)), entier_church_en_int(cdr(un_deux))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "pred = lambda n: car(n(lambda c: cons(cdr(c))(suc(cdr(c))))(cons(zero)(zero)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(entier_church_en_int(pred(int_en_entier_church(n))) for n in range(10))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "sub = lambda n: lambda m: m(pred)(n)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "entier_church_en_int(sub(huit)(trois))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "est_inf_ou_egal = lambda n: lambda m: est_nul(sub(m)(n))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(booleen_en_bool(est_inf_ou_egal(cinq)(int_en_entier_church(n))) for n in range(10))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "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": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(booleen_en_bool(est_egal(cinq)(int_en_entier_church(n))) for n in range(10))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
   },
   "source": [
    "## Itération"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "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": null,
   "metadata": {},
   "outputs": [],
   "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": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "phi_fact = lambda f: lambda n: 1 if n == 0 else n*f(n-1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "bottom = lambda x: (lambda y: y(y))(lambda y:y(y))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "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": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(f4(n) for n in range(4))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "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": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "fact2 = phi_fact(fact_rec)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(fact2(n) for n in range(7))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "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": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "fact3 = fix_curry(phi_fact)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(fact3(n) for n in range(7))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
   },
   "source": [
    "## Un programme obscur"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "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": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "phiListEnChaine = lambda x: lambda y: '' if y == [] else chr(y[0]) + x(y[1:])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "fix_curry(phiListEnChaine)([65+k for k in range(26)])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "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": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "fix_curry(phiMap)(lambda x: x*x)([1, 2, 3, 4])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "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": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "fix_curry(phiExpoMod)(2)(10)(1000)"
   ]
  }
 ],
 "metadata": {
  "jupytext": {
   "formats": "ipynb,md"
  },
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.7.3"
  },
  "toc-autonumbering": true,
  "widgets": {
   "application/vnd.jupyter.widget-state+json": {
    "state": {},
    "version_major": 2,
    "version_minor": 0
   }
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}