From 00061e2243915b92777ac73cc0d0ca8f70a6aa6a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=89ric=20Wegrzynowski?= Date: Fri, 29 Jan 2021 17:11:07 +0100 Subject: [PATCH] =?UTF-8?q?premier=20d=C3=A9p=C3=B4t?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- README.md | 4 + lambda_calcul.ipynb | 2255 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 2259 insertions(+) create mode 100644 README.md create mode 100644 lambda_calcul.ipynb diff --git a/README.md b/README.md new file mode 100644 index 0000000..68e7fc2 --- /dev/null +++ b/README.md @@ -0,0 +1,4 @@ +# Quelques essais autour du 饾渾-calcul + +# TODO +R茅diger le texte. diff --git a/lambda_calcul.ipynb b/lambda_calcul.ipynb new file mode 100644 index 0000000..1dba5cc --- /dev/null +++ b/lambda_calcul.ipynb @@ -0,0 +1,2255 @@ +{ + "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\u001b[0m in \u001b[0;36m\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\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 +}