agreg/Lambda_Calcul_en_OCaml.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "toc": "true"
   },
   "source": [
    "# Table of Contents\n",
    " <p><div class=\"lev1 toc-item\"><a href=\"#Lambda-calcul-implémenté-en-OCaml\" data-toc-modified-id=\"Lambda-calcul-implémenté-en-OCaml-1\"><span class=\"toc-item-num\">1&nbsp;&nbsp;</span>Lambda-calcul implémenté en OCaml</a></div><div class=\"lev2 toc-item\"><a href=\"#Expressions\" data-toc-modified-id=\"Expressions-11\"><span class=\"toc-item-num\">1.1&nbsp;&nbsp;</span>Expressions</a></div><div class=\"lev2 toc-item\"><a href=\"#But-?\" data-toc-modified-id=\"But-?-12\"><span class=\"toc-item-num\">1.2&nbsp;&nbsp;</span>But ?</a></div><div class=\"lev2 toc-item\"><a href=\"#Grammaire\" data-toc-modified-id=\"Grammaire-13\"><span class=\"toc-item-num\">1.3&nbsp;&nbsp;</span>Grammaire</a></div><div class=\"lev2 toc-item\"><a href=\"#L'identité\" data-toc-modified-id=\"L'identité-14\"><span class=\"toc-item-num\">1.4&nbsp;&nbsp;</span>L'identité</a></div><div class=\"lev2 toc-item\"><a href=\"#Conditionnelles\" data-toc-modified-id=\"Conditionnelles-15\"><span class=\"toc-item-num\">1.5&nbsp;&nbsp;</span>Conditionnelles</a></div><div class=\"lev2 toc-item\"><a href=\"#Nombres\" data-toc-modified-id=\"Nombres-16\"><span class=\"toc-item-num\">1.6&nbsp;&nbsp;</span>Nombres</a></div><div class=\"lev2 toc-item\"><a href=\"#Test-d'inégalité\" data-toc-modified-id=\"Test-d'inégalité-17\"><span class=\"toc-item-num\">1.7&nbsp;&nbsp;</span>Test d'inégalité</a></div><div class=\"lev2 toc-item\"><a href=\"#Successeurs\" data-toc-modified-id=\"Successeurs-18\"><span class=\"toc-item-num\">1.8&nbsp;&nbsp;</span>Successeurs</a></div><div class=\"lev2 toc-item\"><a href=\"#Prédecesseurs\" data-toc-modified-id=\"Prédecesseurs-19\"><span class=\"toc-item-num\">1.9&nbsp;&nbsp;</span>Prédecesseurs</a></div><div class=\"lev2 toc-item\"><a href=\"#Addition\" data-toc-modified-id=\"Addition-110\"><span class=\"toc-item-num\">1.10&nbsp;&nbsp;</span>Addition</a></div><div class=\"lev2 toc-item\"><a href=\"#Multiplication\" data-toc-modified-id=\"Multiplication-111\"><span class=\"toc-item-num\">1.11&nbsp;&nbsp;</span>Multiplication</a></div><div class=\"lev2 toc-item\"><a href=\"#Paires\" data-toc-modified-id=\"Paires-112\"><span class=\"toc-item-num\">1.12&nbsp;&nbsp;</span>Paires</a></div><div class=\"lev2 toc-item\"><a href=\"#Prédécesseurs,-deuxième-essai\" data-toc-modified-id=\"Prédécesseurs,-deuxième-essai-113\"><span class=\"toc-item-num\">1.13&nbsp;&nbsp;</span>Prédécesseurs, deuxième essai</a></div><div class=\"lev2 toc-item\"><a href=\"#Listes\" data-toc-modified-id=\"Listes-114\"><span class=\"toc-item-num\">1.14&nbsp;&nbsp;</span>Listes</a></div><div class=\"lev2 toc-item\"><a href=\"#La-fonction-U\" data-toc-modified-id=\"La-fonction-U-115\"><span class=\"toc-item-num\">1.15&nbsp;&nbsp;</span>La fonction U</a></div><div class=\"lev2 toc-item\"><a href=\"#La-récursion-via-la-fonction-Y\" data-toc-modified-id=\"La-récursion-via-la-fonction-Y-116\"><span class=\"toc-item-num\">1.16&nbsp;&nbsp;</span>La récursion via la fonction Y</a></div><div class=\"lev2 toc-item\"><a href=\"#Conclusion\" data-toc-modified-id=\"Conclusion-117\"><span class=\"toc-item-num\">1.17&nbsp;&nbsp;</span>Conclusion</a></div>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Lambda-calcul implémenté en OCaml\n",
    "\n",
    "Ce notebook est inspiré de [ce post de blog du Professeur Matt Might](http://matt.might.net/articles/python-church-y-combinator/), qui implémente un mini langage de programmation en $\\lambda$-calcul, en Python.\n",
    "Je vais faire la même chose en OCaml.\n",
    "\n",
    "## Expressions\n",
    "On rappelle que les expressions du [Lambda calcul](https://fr.wikipedia.org/wiki/Lambda-calcul), ou $\\lambda$-calcul, sont les suivantes :\n",
    "$$ \\begin{cases}\n",
    "x, y, z & \\text{(des variables)} \\\\\n",
    "u v & \\text{(application de deux termes}\\, u, v\\; \\text{)} \\\\\n",
    "\\lambda x. v & \\text{(lambda-function prenant la variable}\\; x \\;\\text{et le terme}\\; v \\;\\text{)}\n",
    "\\end{cases} $$\n",
    "\n",
    "## But ?\n",
    "Le but ne va pas être de les représenter comme ça avec des types formels en Caml, mais plutôt d'utiliser les constructions de Caml, respectivement `u(v)` et `fun x -> v` pour l'application et les fonctions anonymes, et encoder des fonctionnalités de plus haut niveau dans ce langage réduit.\n",
    "\n",
    "## Grammaire\n",
    "Avec une grammaire BNF, si `<var>` désigne un nom d'expression valide (on se limitera à des noms en miniscules consistitués des 26 lettres `a,b,..,z`) :\n",
    "\n",
    "    <exp> ::= <var>\n",
    "    | <exp>(<exp>)\n",
    "    | fun <var> -> <exp>\n",
    "    | (<exp>)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "----\n",
    "## L'identité"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val identite : 'a -> 'a = <fun>\n"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let identite = fun x -> x ;;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val vide : 'a -> 'a = <fun>\n"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let vide = fun x -> x ;;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Conditionnelles\n",
    "La conditionnelle est `si cond alors valeur_vraie sinon valeur_fausse`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val si : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = <fun>\n"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let si = fun cond valeur_vraie valeur_fausse -> cond valeur_vraie valeur_fausse ;;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "C'est très simple, du moment qu'on s'assure que `cond` est soit `vrai` soit `faux` tels que définis par leur comportement :\n",
    "\n",
    "    si vrai e1 e2 == e1\n",
    "    si faux e1 e2 == e2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "File \"[14]\", line 1, characters 28-41:\n",
      "Warning 27: unused variable valeur_fausse.\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "val vrai : 'a -> 'b -> 'a = <fun>\n"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "File \"[14]\", line 2, characters 15-27:\n",
      "Warning 27: unused variable valeur_vraie.\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "val faux : 'a -> 'b -> 'b = <fun>\n"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let vrai = fun valeur_vraie valeur_fausse -> valeur_vraie ;;\n",
    "let faux = fun valeur_vraie valeur_fausse -> valeur_fausse ;;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "La négation est facile !"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val non : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c = <fun>\n"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let non = fun v x y -> v y x;;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "En fait, on va forcer une évaluation paresseuse, comme ça si l'une des deux expressions ne terminent pas, l'évaluation fonctionne quand même."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "File \"[16]\", line 1, characters 38-51:\n",
      "Warning 27: unused variable valeur_fausse.\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "val vrai_paresseux : (unit -> 'a) -> 'b -> 'a = <fun>\n"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "File \"[16]\", line 2, characters 25-37:\n",
      "Warning 27: unused variable valeur_vraie.\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "val faux_paresseux : 'a -> (unit -> 'b) -> 'b = <fun>\n"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let vrai_paresseux = fun valeur_vraie valeur_fausse -> valeur_vraie () ;;\n",
    "let faux_paresseux = fun valeur_vraie valeur_fausse -> valeur_fausse () ;;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Pour rendre paresseux un terme, rien de plus simple !"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val paresseux : 'a -> unit -> 'a = <fun>\n"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let paresseux = fun f -> fun () -> f ;;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Nombres\n",
    "La représentation de Church consiste a écrire $n$ comme $\\lambda f. \\lambda z. f^n z$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "type 'a nombres = ('a -> 'a) -> 'a -> 'a\n"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "type entiers_church = (int -> int) -> int -> int\n"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "type 'a nombres = ('a -> 'a) -> 'a -> 'a;;  (* inutilisé *)\n",
    "type entiers_church = (int -> int) -> int -> int;;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "$0$ est trivialement $\\lambda f. \\lambda z. z$ :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "File \"[34]\", line 1, characters 16-17:\n",
      "Warning 27: unused variable f.\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "val zero : ('a -> 'a) -> 'a -> 'a = <fun>\n"
      ]
     },
     "execution_count": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let zero = fun (f : ('a -> 'a)) (z : 'a) -> z ;;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "$1$ est $\\lambda f. \\lambda z. f z$ :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val un : ('a -> 'a) -> 'a -> 'a = <fun>\n"
      ]
     },
     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let un = fun (f : ('a -> 'a)) -> f ;;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Avec l'opérateur de composition, l'écriture des entiers suivants est facile."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b = <fun>\n"
      ]
     },
     "execution_count": 36,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let compose = fun f g x -> f (g x);;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val deux : ('a -> 'a) -> 'a -> 'a = <fun>\n"
      ]
     },
     "execution_count": 37,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "val trois : ('a -> 'a) -> 'a -> 'a = <fun>\n"
      ]
     },
     "execution_count": 37,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "val quatre : ('a -> 'a) -> 'a -> 'a = <fun>\n"
      ]
     },
     "execution_count": 37,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let deux = fun f -> compose f f;;  (* == compose f (un f) *)\n",
    "let trois = fun f -> compose f (deux f) ;;\n",
    "let quatre = fun f -> compose f (trois f) ;;\n",
    "(* etc *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On peut généraliser ça, avec une fonction qui transforme un entier (`int`) de Caml en un entier de Church :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val entierChurch : int -> ('a -> 'a) -> 'a -> 'a = <fun>\n"
      ]
     },
     "execution_count": 38,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let rec entierChurch (n : int) =\n",
    "    fun f z -> if n = 0 then z else f ((entierChurch (n-1)) f z)\n",
    ";;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Par exemple :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 0\n"
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "- : int = 7\n"
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "- : int = 8\n"
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "(entierChurch 0) (fun x -> x + 1) 0;; (* 0 *)\n",
    "(entierChurch 7) (fun x -> x + 1) 0;; (* 7 *)\n",
    "(entierChurch 3) (fun x -> 2*x) 1;; (* 8 *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Et une fonction qui fait l'inverse (note : cette fonction n'est *pas* un $\\lambda$-terme) :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val entierNatif : ((int -> int) -> int -> int) -> int = <fun>\n"
      ]
     },
     "execution_count": 40,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let entierNatif c : int =\n",
    "    c (fun x -> x + 1) 0\n",
    ";;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Un petit test :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 0\n"
      ]
     },
     "execution_count": 41,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "- : int = 1\n"
      ]
     },
     "execution_count": 41,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif (si vrai zero un);; (* 0 *)\n",
    "entierNatif (si faux zero un);; (* 1 *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 100\n"
      ]
     },
     "execution_count": 42,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif (entierChurch 100);; (* 100 *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Test d'inégalité\n",
    "On a besoin de pouvoir tester si $n \\leq 0$ (ou $n = 0$) en fait."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "File \"[43]\", line 2, characters 29-30:\n",
      "Warning 27: unused variable z.\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "val estnul : (('a -> 'b -> 'c -> 'c) -> ('d -> 'e -> 'd) -> 'f) -> 'f = <fun>\n"
      ]
     },
     "execution_count": 43,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "(* prend un lambda f lambda z. ... est donne vrai ssi n = 0 ou faux sinon *)\n",
    "let estnul = fun n -> n (fun z -> faux) (vrai);;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "File \"[44]\", line 2, characters 32-33:\n",
      "Warning 27: unused variable z.\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "val estnonnul : (('a -> 'b -> 'c -> 'b) -> ('d -> 'e -> 'e) -> 'f) -> 'f =\n",
       "  <fun>\n"
      ]
     },
     "execution_count": 44,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "(* prend un lambda f lambda z. ... est donne vrai ssi n > 0 ou faux sinon *)\n",
    "let estnonnul = fun n -> n (fun z -> vrai) (faux);;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On peut proposer cette autre implémentation, qui \"fonctionne\" pareil (au sens calcul des $\\beta$-réductions) mais est plus compliquée :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val estnonnul2 :\n",
       "  (('a -> 'b -> 'c -> 'c) -> ('d -> 'e -> 'd) -> 'f -> 'g -> 'h) ->\n",
       "  'g -> 'f -> 'h = <fun>\n"
      ]
     },
     "execution_count": 45,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let estnonnul2 = fun n -> non (estnul n);;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 46,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 0\n"
      ]
     },
     "execution_count": 46,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "- : int = 1\n"
      ]
     },
     "execution_count": 46,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "- : int = 1\n"
      ]
     },
     "execution_count": 46,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif (si (estnul zero) zero un);; (* 0 *)\n",
    "entierNatif (si (estnul un)   zero un);; (* 1 *)\n",
    "entierNatif (si (estnul deux) zero un);; (* 1 *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 47,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 1\n"
      ]
     },
     "execution_count": 47,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "- : int = 0\n"
      ]
     },
     "execution_count": 47,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "- : int = 0\n"
      ]
     },
     "execution_count": 47,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif (si (estnonnul zero) zero un);; (* 0 *)\n",
    "entierNatif (si (estnonnul un)   zero un);; (* 1 *)\n",
    "entierNatif (si (estnonnul deux) zero un);; (* 1 *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 48,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 1\n"
      ]
     },
     "execution_count": 48,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "- : int = 0\n"
      ]
     },
     "execution_count": 48,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "- : int = 0\n"
      ]
     },
     "execution_count": 48,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif (si (non (estnul zero)) zero un);; (* 0 *)\n",
    "entierNatif (si (non (estnul un))   zero un);; (* 1 *)\n",
    "entierNatif (si (non (estnul deux)) zero un);; (* 1 *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Successeurs\n",
    "Vue la représentation de Churc, $n+1$ consiste a appliquer l'argument $f$ une fois de plus :\n",
    "$f^{n+1}(z) = f (f^n(z))$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 49,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val succ : (('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b = <fun>\n"
      ]
     },
     "execution_count": 49,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let succ = fun n f z -> f ((n f) z) ;;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 50,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 2\n"
      ]
     },
     "execution_count": 50,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif (succ un);; (* 2 *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 51,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : ('a -> 'a) -> 'a -> 'a = <fun>\n"
      ]
     },
     "execution_count": 51,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "- : ('_a -> '_a) -> '_a -> '_a = <fun>\n"
      ]
     },
     "execution_count": 51,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "deux;;\n",
    "succ un;;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On remarque qu'ils ont le même typage, mais OCaml indique qu'il a moins d'informations à propos du deuxième : ce `'_a` signifie que le type est *contraint*, il sera fixé dès la première utilisation de cette fonction.\n",
    "\n",
    "C'est assez mystérieux, mais il faut retenir le point suivant : `deux` était écrit manuellement, donc le système a vu le terme en entier, il le connaît et saît que `deux = fun f -> fun x -> f (f x))`, pas de surprise. Par contre, `succ un` est le résultat d'une évaluation *partielle* et vaut `fun f z -> f ((deux f) z)`. Sauf que le système ne calcule pas tout et laisse l'évaluation partielle ! (heureusement !)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Si on appelle `succ un` à une fonction, le `'_a` va être contraint, et on ne pourra pas s'en reservir :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 54,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val succ_de_un : ('_a -> '_a) -> '_a -> '_a = <fun>\n"
      ]
     },
     "execution_count": 54,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let succ_de_un = succ un;;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 55,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int -> int = <fun>\n"
      ]
     },
     "execution_count": 55,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "(succ_de_un) (fun x -> x + 1);;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 56,
   "metadata": {},
   "outputs": [
    {
     "ename": "error",
     "evalue": "compile_error",
     "output_type": "error",
     "traceback": [
      "\u001b[32mFile \"[56]\", line 1, characters 23-24:\n\u001b[31mError: This expression has type int but an expression was expected of type\n         string\n\u001b[36m   1: \u001b[30m(succ_de_un) (fun x -> \u001b[4mx\u001b[0m\u001b[30m ^ \"0\");;\u001b[0m\n"
     ]
    }
   ],
   "source": [
    "(succ_de_un) (fun x -> x ^ \"0\");;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 57,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : string -> string = <fun>\n"
      ]
     },
     "execution_count": 57,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "(succ un) (fun x -> x ^ \"0\");;\n",
    "(* une valeur fraîchement calculée, sans contrainte *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Prédecesseurs\n",
    "Vue la représentation de Church, $\\lambda n. n-1$ n'existe pas... mais on peut tricher."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val pred : ((int -> int) -> int -> int) -> ('a -> 'a) -> 'a -> 'a = <fun>\n"
      ]
     },
     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let pred = fun n ->\n",
    "    if (entierNatif n) > 0 then entierChurch ((entierNatif n) - 1)\n",
    "    else zero\n",
    ";;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 1\n"
      ]
     },
     "execution_count": 31,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif (pred deux);; (* 1 *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 2\n"
      ]
     },
     "execution_count": 32,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif (pred trois);; (* 2 *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Addition\n",
    "\n",
    "Pour ajouter $n$ et $m$, il faut appliquer une fonction $f$ $n$ fois puis $m$ fois : $f^{n+m}(z) = f^n(f^m(z))$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val somme : ('a -> 'b -> 'c) -> ('a -> 'd -> 'b) -> 'a -> 'd -> 'c = <fun>\n"
      ]
     },
     "execution_count": 33,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let somme = fun n m f z -> n(f)( m(f)(z));;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val cinq : ('_a -> '_a) -> '_a -> '_a = <fun>\n"
      ]
     },
     "execution_count": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let cinq = somme deux trois ;;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 5\n"
      ]
     },
     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif cinq;;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val sept : (int -> int) -> int -> int = <fun>\n"
      ]
     },
     "execution_count": 36,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let sept = somme cinq deux ;;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 7\n"
      ]
     },
     "execution_count": 37,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif sept;;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Multiplication\n",
    "\n",
    "Pour multiplier $n$ et $m$, il faut appliquer le codage de $n$ exactement $m$ fois : $f^{nm}(z) = (f^n(f^n(...(f^n(z))...))$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val produit : ('a -> 'b) -> ('b -> 'c -> 'd) -> 'a -> 'c -> 'd = <fun>\n"
      ]
     },
     "execution_count": 38,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let produit = fun n m f z -> m(n(f))(z);;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On peut faire encore mieux avec l'opérateur de composition :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val produit : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c = <fun>\n"
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let produit = fun n m -> compose m n;;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val six : ('_a -> '_a) -> '_a -> '_a = <fun>\n"
      ]
     },
     "execution_count": 40,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let six = produit deux trois ;;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 6\n"
      ]
     },
     "execution_count": 41,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif six;;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val huit : ('_a -> '_a) -> '_a -> '_a = <fun>\n"
      ]
     },
     "execution_count": 42,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let huit = produit deux quatre ;;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 8\n"
      ]
     },
     "execution_count": 43,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif huit;;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Paires\n",
    "\n",
    "On va écrire un constructeur de paires, `paire a b` qui sera comme `(a, b)`, et deux destructeurs, `gauche` et `droite`, qui vérifient :\n",
    "\n",
    "    gauche (paire a b) == a\n",
    "    droite (paire a b) == b"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 75,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val paire : 'a -> 'b -> ('a -> 'b -> 'c) -> 'c = <fun>\n"
      ]
     },
     "execution_count": 75,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let paire = fun a b -> fun f -> f(a)(b);;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 76,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "File \"[76]\", line 1, characters 30-31:\n",
      "Warning 27: unused variable b.\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "val gauche : (('a -> 'b -> 'a) -> 'c) -> 'c = <fun>\n"
      ]
     },
     "execution_count": 76,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "File \"[76]\", line 2, characters 28-29:\n",
      "Warning 27: unused variable a.\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "val droite : (('a -> 'b -> 'b) -> 'c) -> 'c = <fun>\n"
      ]
     },
     "execution_count": 76,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let gauche = fun p -> p(fun a b -> a);;\n",
    "let droite = fun p -> p(fun a b -> b);;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 77,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 0\n"
      ]
     },
     "execution_count": 77,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "- : int = 1\n"
      ]
     },
     "execution_count": 77,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif (gauche (paire zero un));;\n",
    "entierNatif (droite (paire zero un));;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Prédécesseurs, deuxième essai\n",
    "\n",
    "Il y a une façon, longue et compliquée ([source](http://gregfjohnson.com/pred/)) d'y arriver, avec des paires."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 78,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val pred :\n",
       "  (((('a -> 'b -> 'a) -> 'c -> 'd) -> 'd) ->\n",
       "   ((('e -> 'e -> 'e) ->\n",
       "     ((('f -> 'g -> 'g) -> 'c -> 'h) -> 'h) ->\n",
       "     ((('i -> 'j -> 'j) -> 'k -> 'l) -> 'l) -> 'm) ->\n",
       "    'm) ->\n",
       "   ('n -> 'o -> 'o) -> 'p) ->\n",
       "  ((((('f -> 'g -> 'g) -> 'c -> 'h) -> 'h) ->\n",
       "    ((('i -> 'j -> 'j) -> 'k -> 'l) -> 'l) -> 'm) ->\n",
       "   'k) ->\n",
       "  'c -> 'p = <fun>\n"
      ]
     },
     "execution_count": 78,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let pred n suivant premier =\n",
    "    let pred_suivant = paire vrai premier in\n",
    "    let pred_premier = fun p ->\n",
    "        si (gauche p)\n",
    "        (paire faux premier)\n",
    "        (paire faux (suivant (droite p)))\n",
    "    in\n",
    "    let paire_finale = n pred_suivant pred_premier in\n",
    "    droite paire_finale\n",
    ";;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Malheureusement, ce n'est pas bien typé."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 79,
   "metadata": {},
   "outputs": [
    {
     "ename": "error",
     "evalue": "compile_error",
     "output_type": "error",
     "traceback": [
      "\u001b[32mFile \"[79]\", line 1, characters 18-22:\n\u001b[31mError: This expression has type\n         ((('a -> 'b -> 'a) -> 'c -> 'd) -> ('a -> 'b -> 'a) -> 'c -> 'd) ->\n         (('a -> 'b -> 'a) -> 'c -> 'd) -> ('a -> 'b -> 'a) -> 'c -> 'd\n       but an expression was expected of type\n         ((('a -> 'b -> 'a) -> 'c -> 'd) -> 'd) ->\n         ((('e -> 'e -> 'e) ->\n           ((('f -> 'g -> 'g) -> 'c -> 'h) -> 'h) ->\n           ((('i -> 'j -> 'j) -> 'k -> 'l) -> 'l) -> 'm) ->\n          'm) ->\n         ('n -> 'o -> 'o) -> 'p\n       The type variable 'd occurs inside ('a -> 'b -> 'a) -> 'c -> 'd\n\u001b[36m   1: \u001b[30mentierNatif (pred \u001b[4mdeux\u001b[0m\u001b[30m);; (* 1 *)\u001b[0m\n"
     ]
    }
   ],
   "source": [
    "entierNatif (pred deux);; (* 1 *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Listes\n",
    "\n",
    "Pour construire des listes (simplement chaînées), on a besoin d'une valeur pour la liste vide, `listevide`, d'un constructeur pour une liste `cons`, un prédicat pour la liste vide `estvide`, un accesseur `tete` et `queue`, et avec les contraintes suivantes (avec `vrai`, `faux` définis comme plus haut) :\n",
    "\n",
    "    estvide (listevide) == vrai\n",
    "    estvide (cons tt qu) == faux\n",
    "    \n",
    "    tete (cons tt qu) == tt\n",
    "    queue (cons tt qu) == qu\n",
    "\n",
    "On va stocker tout ça avec des fonctions qui attendront deux arguments (deux fonctions - rappel tout est fonction en $\\lambda$-calcul), l'une appellée si la liste est vide, l'autre si la liste n'est pas vide."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 58,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "File \"[58]\", line 1, characters 28-38:\n",
      "Warning 27: unused variable surpasvide.\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "val listevide : 'a -> 'b -> 'a = <fun>\n"
      ]
     },
     "execution_count": 58,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let listevide = fun survide surpasvide -> survide;;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 59,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val cons : 'a -> 'b -> 'c -> ('a -> 'b -> 'd) -> 'd = <fun>\n"
      ]
     },
     "execution_count": 59,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "File \"[59]\", line 1, characters 28-35:\n",
      "Warning 27: unused variable survide.\n"
     ]
    }
   ],
   "source": [
    "let cons = fun hd tl -> fun survide surpasvide -> surpasvide hd tl;;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Avec cette construction, `estvide` est assez simple : `survide` est `() -> vrai` et `surpasvide` est `tt qu -> faux`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 60,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "File \"[60]\", line 1, characters 45-47:\n",
      "Warning 27: unused variable tt.\n",
      "File \"[60]\", line 1, characters 48-50:\n",
      "Warning 27: unused variable qu.\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "val estvide : (('a -> 'b -> 'a) -> ('c -> 'd -> 'e -> 'f -> 'f) -> 'g) -> 'g =\n",
       "  <fun>\n"
      ]
     },
     "execution_count": 60,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let estvide = fun liste -> liste (vrai) (fun tt qu -> faux);;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Deux tests :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 61,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 1\n"
      ]
     },
     "execution_count": 61,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "- : int = 0\n"
      ]
     },
     "execution_count": 61,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif (si (estvide (listevide)) un zero);; (* estvide listevide == vrai *)\n",
    "entierNatif (si (estvide (cons un listevide)) un zero);; (* estvide (cons un listevide) == faux *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Et pour les deux extracteurs, c'est très facile avec cet encodage."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 62,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "File \"[62]\", line 1, characters 45-47:\n",
      "Warning 27: unused variable qu.\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "val tete : (('a -> 'a) -> ('b -> 'c -> 'b) -> 'd) -> 'd = <fun>\n"
      ]
     },
     "execution_count": 62,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "File \"[62]\", line 2, characters 43-45:\n",
      "Warning 27: unused variable tt.\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "val queue : (('a -> 'a) -> ('b -> 'c -> 'c) -> 'd) -> 'd = <fun>\n"
      ]
     },
     "execution_count": 62,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let tete = fun liste -> liste (vide) (fun tt qu -> tt);;\n",
    "let queue = fun liste -> liste (vide) (fun tt qu -> qu);;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 69,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : int = 1\n"
      ]
     },
     "execution_count": 69,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "- : int = 1\n"
      ]
     },
     "execution_count": 69,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "- : int = 2\n"
      ]
     },
     "execution_count": 69,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "entierNatif (tete (cons un listevide));;\n",
    "entierNatif (tete (queue (cons deux (cons un listevide))));;\n",
    "entierNatif (tete (queue (cons trois (cons deux (cons un listevide)))));;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Visualisons les types que Caml trouve a des listes de tailles croissantes :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 70,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : '_a ->\n",
       "    ((('_b -> '_b) -> '_b -> '_b) ->\n",
       "     ('_c ->\n",
       "      ((('_d -> '_d) -> '_d -> '_d) -> ('_e -> '_f -> '_e) -> '_g) -> '_g) ->\n",
       "     '_h) ->\n",
       "    '_h\n",
       "= <fun>\n"
      ]
     },
     "execution_count": 70,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "cons un (cons un listevide);;  (* 8 variables pour une liste de taille 2 *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 71,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : '_a ->\n",
       "    ((('_b -> '_b) -> '_b -> '_b) ->\n",
       "     ('_c ->\n",
       "      ((('_d -> '_d) -> '_d -> '_d) ->\n",
       "       ('_e ->\n",
       "        ((('_f -> '_f) -> '_f -> '_f) ->\n",
       "         ('_g ->\n",
       "          ((('_h -> '_h) -> '_h -> '_h) -> ('_i -> '_j -> '_i) -> '_k) -> '_k) ->\n",
       "         '_l) ->\n",
       "        '_l) ->\n",
       "       '_m) ->\n",
       "      '_m) ->\n",
       "     '_n) ->\n",
       "    '_n\n",
       "= <fun>\n"
      ]
     },
     "execution_count": 71,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "cons un (cons un (cons un (cons un listevide)));;  (* 14 variables pour une liste de taille 4 *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 72,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : '_a ->\n",
       "    ((('_b -> '_b) -> '_b -> '_b) ->\n",
       "     ('_c ->\n",
       "      ((('_d -> '_d) -> '_d -> '_d) ->\n",
       "       ('_e ->\n",
       "        ((('_f -> '_f) -> '_f -> '_f) ->\n",
       "         ('_g ->\n",
       "          ((('_h -> '_h) -> '_h -> '_h) ->\n",
       "           ('_i ->\n",
       "            ((('_j -> '_j) -> '_j -> '_j) ->\n",
       "             ('_k ->\n",
       "              ((('_l -> '_l) -> '_l -> '_l) ->\n",
       "               ('_m ->\n",
       "                ((('_n -> '_n) -> '_n -> '_n) ->\n",
       "                 ('_o ->\n",
       "                  ((('_p -> '_p) -> '_p -> '_p) -> ('_q -> '_r -> '_q) -> '_s) ->\n",
       "                  '_s) ->\n",
       "                 '_t) ->\n",
       "                '_t) ->\n",
       "               '_u) ->\n",
       "              '_u) ->\n",
       "             '_v) ->\n",
       "            '_v) ->\n",
       "           '_w) ->\n",
       "          '_w) ->\n",
       "         '_x) ->\n",
       "        '_x) ->\n",
       "       '_y) ->\n",
       "      '_y) ->\n",
       "     '_z) ->\n",
       "    '_z\n",
       "= <fun>\n"
      ]
     },
     "execution_count": 72,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "cons un (cons un (cons un (cons un (cons un (cons un (cons un (cons un listevide)))))));;  (* 26 variables pour une liste de taille 7 *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Pour ces raisons là, on se rend compte que le type donné par Caml à une liste de taille $k$ croît linéairement *en taille* en fonction de $k$ !\n",
    "\n",
    "Aucun espoir donc (avec cet encodage) d'avoir un type générique pour les listes représentés en Caml.\n",
    "\n",
    "Et donc nous ne sommes pas surpris de voir cet essai échouer :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 68,
   "metadata": {},
   "outputs": [
    {
     "ename": "error",
     "evalue": "compile_error",
     "output_type": "error",
     "traceback": [
      "\u001b[32mFile \"[68]\", line 2, characters 44-45:\n\u001b[31mError: This expression has type 'a but an expression was expected of type\n         (('b -> 'b) -> 'b -> 'b) -> ('c -> 'a -> 'd) -> 'e\n       The type variable 'a occurs inside\n       (('b -> 'b) -> 'b -> 'b) -> ('c -> 'a -> 'd) -> 'e\n\u001b[36m   1: \u001b[30mlet rec longueur liste =\n\u001b[36m   2: \u001b[30m    liste (zero) (fun t q -> succ (longueur \u001b[4mq\u001b[0m\u001b[30m))\n\u001b[36m   3: \u001b[30m;;\u001b[0m\n"
     ]
    }
   ],
   "source": [
    "let rec longueur liste =\n",
    "    liste (zero) (fun t q -> succ (longueur q))\n",
    ";;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<span style=\"color:red;\">En effet, `longueur` devrait être bien typée et `liste` et `q` devraient avoir le même type, or le type de `liste` est strictement plus grand que celui de `q`...</span>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On peut essayer de faire une fonction `ieme`.\n",
    "On veut que `ieme zero liste = tete` et `ieme n liste = ieme (pred n) (queue liste)`.\n",
    "\n",
    "En écrivant en haut niveau, on aimerait pouvoir faire :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 87,
   "metadata": {},
   "outputs": [
    {
     "ename": "error",
     "evalue": "compile_error",
     "output_type": "error",
     "traceback": [
      "\u001b[32mFile \"[87]\", line 2, characters 42-47:\n\u001b[31mError: This expression has type\n         ('a -> 'b -> 'a) ->\n         ('c -> 'd -> 'e -> 'f -> 'f) -> ('g -> 'h -> 'g) -> 'i -> 'j\n       but an expression was expected of type\n         ('a -> 'a) -> ('k -> 'l -> 'l) -> 'm\n       The type variable 'a occurs inside 'b -> 'a\n\u001b[36m   1: \u001b[30mlet pop liste =\n\u001b[36m   2: \u001b[30m    si (estvide liste) (listevide) (queue \u001b[4mliste\u001b[0m\u001b[30m)\n\u001b[36m   3: \u001b[30m;;\u001b[0m\n"
     ]
    }
   ],
   "source": [
    "let pop liste =\n",
    "    si (estvide liste) (listevide) (queue liste)\n",
    ";;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 86,
   "metadata": {},
   "outputs": [
    {
     "ename": "error",
     "evalue": "compile_error",
     "output_type": "error",
     "traceback": [
      "\u001b[32mFile \"[86]\", line 2, characters 12-15:\n\u001b[31mError: Unbound value pop\n\u001b[36m   1: \u001b[30mlet ieme n liste =\n\u001b[36m   2: \u001b[30m    tete (n \u001b[4mpop\u001b[0m\u001b[30m liste)\n\u001b[36m   3: \u001b[30m;;\u001b[0m\n"
     ]
    }
   ],
   "source": [
    "let ieme n liste =\n",
    "    tete (n pop liste)\n",
    ";;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## La fonction U\n",
    "\n",
    "C'est le premier indice que le $\\lambda$-calcul peut être utilisé comme modèle de calcul : le terme $U : f \\to f(f)$ ne termine pas si on l'applique à lui-même.\n",
    "\n",
    "Mais ce sera la faiblesse de l'utilisation de Caml : ce terme ne peut être correctement typé !"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 55,
   "metadata": {},
   "outputs": [
    {
     "ename": "error",
     "evalue": "compile_error",
     "output_type": "error",
     "traceback": [
      "\u001b[32mFile \"[55]\", line 1, characters 19-22:\n\u001b[31mError: This expression has type 'a -> 'b\n       but an expression was expected of type 'a\n       The type variable 'a occurs inside 'a -> 'b\n\u001b[36m   1: \u001b[30mlet u = fun f -> f \u001b[4m(f)\u001b[0m\u001b[30m;;\u001b[0m\n"
     ]
    }
   ],
   "source": [
    "let u = fun f -> f (f);;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A noter que même dans un langage non typé (par exemple Python), on peut définir $U$ mais son exécution échouera, soit à caude d'un dépassement de pile, soit parce qu'elle ne termine pas."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## La récursion via la fonction Y\n",
    "\n",
    "La fonction $Y$ trouve le point fixe d'une autre fonction.\n",
    "C'est très utile pour définir des fonctions par récurrence.\n",
    "\n",
    "Par exemple, la factorielle est le point fixe de la fonction suivante :\n",
    "\"$\\lambda f. \\lambda n. 1$ si $n \\leq 0$ sinon $n * f(n-1)$\" (écrite dans un langage plus haut niveau, pas en $\\lambda$-calcul).\n",
    "\n",
    "$Y$ satisfait ces contraintes : $Y(F) = f$ et $f = F(f)$.\n",
    "Donc $Y(F) = F(Y(F))$ et donc $Y = \\lambda F. F(Y(F))$. Mais ce premier essai ne marche pas."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 56,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val y : ('a -> 'a) -> 'a = <fun>\n"
      ]
     },
     "execution_count": 56,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let rec y = fun f -> f (y(f));;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 57,
   "metadata": {},
   "outputs": [
    {
     "ename": "error",
     "evalue": "compile_error",
     "output_type": "error",
     "traceback": [
      "\u001b[32mFile \"[57]\", line 1, characters 63-64:\n\u001b[31mError: This expression has type\n         ((('a -> 'b -> 'a) -> 'c -> 'd -> 'e -> 'e) -> 'd -> 'e -> 'e) ->\n         ((('f -> 'f -> 'f) ->\n           ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n           ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n) ->\n          'o ->\n          ('f -> 'f -> 'f) ->\n          ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n          ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n) ->\n         (('p -> 'p) -> 'p -> 'p) -> 'q -> 'r\n       but an expression was expected of type\n         ((('a -> 'b -> 'a) -> 'c -> 'd -> 'e -> 'e) -> 'd -> 'e -> 'e) ->\n         ((('f -> 'f -> 'f) ->\n           ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n           ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n) ->\n          'n) ->\n         ('s -> 't -> 't) -> 'u\n       The type variable 'n occurs inside\n       'o ->\n       ('f -> 'f -> 'f) ->\n       ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n       ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n\n\u001b[36m   1: \u001b[30mlet fact = y(fun f n -> si (estnul n) (un) (produit n (f (pred \u001b[4mn\u001b[0m\u001b[30m))));;\u001b[0m\n"
     ]
    }
   ],
   "source": [
    "let fact = y(fun f n -> si (estnul n) (un) (produit n (f (pred n))));;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On utilise la $\\eta$-expansion : si $e$ termine, $e$ est équivalent (ie tout calcul donne le même terme) à $\\lambda x. e(x)$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 58,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val y : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>\n"
      ]
     },
     "execution_count": 58,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let rec y = fun f -> f (fun x -> y(f)(x));;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Par contre, le typage n'arrive toujours pas à trouver que l'expression suivante devrait être bien définie :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 59,
   "metadata": {},
   "outputs": [
    {
     "ename": "error",
     "evalue": "compile_error",
     "output_type": "error",
     "traceback": [
      "\u001b[32mFile \"[59]\", line 1, characters 63-64:\n\u001b[31mError: This expression has type\n         ((('a -> 'b -> 'a) -> 'c -> 'd -> 'e -> 'e) -> 'd -> 'e -> 'e) ->\n         ((('f -> 'f -> 'f) ->\n           ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n           ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n) ->\n          'o ->\n          ('f -> 'f -> 'f) ->\n          ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n          ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n) ->\n         (('p -> 'p) -> 'p -> 'p) -> 'q -> 'r\n       but an expression was expected of type\n         ((('a -> 'b -> 'a) -> 'c -> 'd -> 'e -> 'e) -> 'd -> 'e -> 'e) ->\n         ((('f -> 'f -> 'f) ->\n           ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n           ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n) ->\n          'n) ->\n         ('s -> 't -> 't) -> 'u\n       The type variable 'n occurs inside\n       'o ->\n       ('f -> 'f -> 'f) ->\n       ((('g -> 'h -> 'h) -> 'c -> 'i) -> 'i) ->\n       ((('j -> 'k -> 'k) -> 'l -> 'm) -> 'm) -> 'n\n\u001b[36m   1: \u001b[30mlet fact = y(fun f n -> si (estnul n) (un) (produit n (f (pred \u001b[4mn\u001b[0m\u001b[30m))));;\u001b[0m\n"
     ]
    }
   ],
   "source": [
    "let fact = y(fun f n -> si (estnul n) (un) (produit n (f (pred n))));;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Conclusion\n",
    "\n",
    "Je n'ai pas réussi à traduire intégralement la prouesse initiale, écrite en Python, par Matt Might.\n",
    "Dommage, le typage de Caml est trop strict pour cet exercice."
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "OCaml 4.04.2",
   "language": "OCaml",
   "name": "ocaml-jupyter"
  },
  "language_info": {
   "codemirror_mode": "text/x-ocaml",
   "file_extension": ".ml",
   "mimetype": "text/x-ocaml",
   "name": "OCaml",
   "nbconverter_exporter": null,
   "pygments_lexer": "OCaml",
   "version": "4.04.2"
  },
  "toc": {
   "colors": {
    "hover_highlight": "#DAA520",
    "running_highlight": "#FF0000",
    "selected_highlight": "#FFD700"
   },
   "moveMenuLeft": true,
   "nav_menu": {
    "height": "364px",
    "width": "251px"
   },
   "navigate_menu": true,
   "number_sections": true,
   "sideBar": true,
   "threshold": 4,
   "toc_cell": true,
   "toc_section_display": "block",
   "toc_window_display": false
  },
  "varInspector": {
   "cols": {
    "lenName": 16,
    "lenType": 16,
    "lenVar": 40
   },
   "kernels_config": {
    "python": {
     "delete_cmd_postfix": "",
     "delete_cmd_prefix": "del ",
     "library": "var_list.py",
     "varRefreshCmd": "print(var_dic_list())"
    },
    "r": {
     "delete_cmd_postfix": ") ",
     "delete_cmd_prefix": "rm(",
     "library": "var_list.r",
     "varRefreshCmd": "cat(var_dic_list()) "
    }
   },
   "types_to_exclude": [
    "module",
    "function",
    "builtin_function_or_method",
    "instance",
    "_Feature"
   ],
   "window_display": false
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}