{
"cells": [
{
"cell_type": "markdown",
"metadata": {
"toc": "true"
},
"source": [
"# Table of Contents\n",
" "
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# TP 6 - Programmation pour la préparation à l'agrégation maths option info\n",
"TP 6 : Lambda calcul, représentations, calculs et quelques termes pratiques.\n",
"\n",
"- Référence en théorie : [ce poly en français de Jean Goubault-Larrecqu (ENS Cachan)](http://www.lsv.fr/%7Egoubault/Lambda/lambda.pdf) ou le livre \"Logique réduction résolution\", par René Lalement.\n",
"- Pour la pratique : [ce post de blog en anglais](http://matt.might.net/articles/python-church-y-combinator/)\n",
"- Pour plus, [cette page wikipédia](https://fr.wikipedia.org/wiki/Lambda-calcul)."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"- En OCaml."
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val print : ('a, out_channel, unit) format -> 'a = \n"
]
},
"execution_count": 1,
"metadata": {},
"output_type": "execute_result"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"The OCaml toplevel, version 4.04.2\n"
]
},
{
"data": {
"text/plain": [
"- : int = 0\n"
]
},
"execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let print = Printf.printf;;\n",
"Sys.command \"ocaml -version\";;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"----\n",
"# Représentation des $\\lambda$-termes en OCaml\n",
"\n",
"## Grammaire\n",
"\n",
"Avec une [grammaire BNF](https://fr.wikipedia.org/wiki/Forme_de_Backus-Naur), si `` désigne un nom d'expression valide (on se limitera à des noms en miniscules consistitués des 26 lettres a,b,..,z) :\n",
"\n",
" ::= \n",
" | ()\n",
" | fun -> \n",
" | ()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Ex1. Ecrire un type Caml représentant les $\\lambda$-termes"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"type variable = string\n"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"type terme = V of variable | A of terme * terme | F of variable * terme\n"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"type variable = string;;\n",
"\n",
"type terme =\n",
" | V of variable\n",
" | A of terme * terme\n",
" | F of variable * terme\n",
";;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Par exemple, l'identité est le terme $\\lambda x. x$."
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[7]\", line 1, characters 15-16:\n",
"Warning 41: F belongs to several types: terme terme\n",
"The first one was selected. Please disambiguate if this is wrong.\n"
]
},
{
"data": {
"text/plain": [
"val identite : terme = F (\"x\", V \"x\")\n"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let identite = F(\"x\", V(\"x\"));;"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[8]\", line 1, characters 17-18:\n",
"Warning 41: F belongs to several types: terme terme\n",
"The first one was selected. Please disambiguate if this is wrong.\n"
]
},
{
"data": {
"text/plain": [
"val identite_2 : terme = F (\"y\", V \"y\")\n"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let identite_2 = F(\"y\", V(\"y\"));;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Les deux termes sont différents mais égaux à $\\alpha$-renomage près."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Un autre exemple est le terme $\\Omega = (\\lambda x. xx)(\\lambda x. xx)$ (qui est le plus petit terme dont l'exécution par $\\beta$-réduction ne termine pas - cf [ce poly p7](http://www.lsv.fr/%7Egoubault/Lambda/lambda.pdf) si besoin)."
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[9]\", line 1, characters 12-13:\n",
"Warning 41: A belongs to several types: terme terme\n",
"The first one was selected. Please disambiguate if this is wrong.\n"
]
},
{
"data": {
"text/plain": [
"val omega : terme = A (F (\"x\", A (V \"x\", V \"x\")), F (\"x\", A (V \"x\", V \"x\")))\n"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let omega = A(F(\"x\", A(V(\"x\"), V(\"x\"))), F(\"x\", A(V(\"x\"), V(\"x\"))));;"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[10]\", line 1, characters 8-9:\n",
"Warning 41: F belongs to several types: terme terme\n",
"The first one was selected. Please disambiguate if this is wrong.\n"
]
},
{
"data": {
"text/plain": [
"val u : terme = F (\"x\", A (V \"x\", V \"x\"))\n"
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
},
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[10]\", line 2, characters 12-13:\n",
"Warning 41: A belongs to several types: terme terme\n",
"The first one was selected. Please disambiguate if this is wrong.\n"
]
},
{
"data": {
"text/plain": [
"val omega : terme = A (F (\"x\", A (V \"x\", V \"x\")), F (\"x\", A (V \"x\", V \"x\")))\n"
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let u = F(\"x\", A(V(\"x\"), V(\"x\")));;\n",
"let omega = A(u, u);"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Ex2. Ecrire une fonction qui affiche un $\\lambda$-terme en une chaîne de caractère\n",
"C'est très rapide."
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val sprintf : ('a, unit, string) format -> 'a = \n"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
},
{
"name": "stderr",
"output_type": "stream",
"text": [
"File \"[13]\", line 4, characters 6-7:\n",
"Warning 41: V belongs to several types: terme terme\n",
"The first one was selected. Please disambiguate if this is wrong.\n"
]
},
{
"data": {
"text/plain": [
"val string_of_terme : terme -> variable = \n"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let sprintf = Format.sprintf;;\n",
"\n",
"let rec string_of_terme = function\n",
" | V(s) -> s\n",
" | A(u, v) -> sprintf \"(%s)(%s)\" (string_of_terme u) (string_of_terme v)\n",
" (* \"(\" ^ (string_of_terme u) ^ \")\" ^ \"(\" ^ (string_of_terme v) ^ \")\" *)\n",
" | F(s, u) -> sprintf \"λ %s. (%s)\" s (string_of_terme u)\n",
" (* \"lambda \" ^ s ^ \".(\" ^ (string_of_terme u) *)\n",
";;"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"λ x. (x)\n"
]
},
{
"data": {
"text/plain": [
"- : unit = ()\n"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"λ y. (y)\n"
]
},
{
"data": {
"text/plain": [
"- : unit = ()\n"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"(λ x. ((x)(x)))(λ x. ((x)(x)))\n"
]
},
{
"data": {
"text/plain": [
"- : unit = ()\n"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"print_endline (string_of_terme identite);;\n",
"print_endline (string_of_terme identite_2);;\n",
"print_endline (string_of_terme omega);;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Ex3. Bonus : Ecrire une fonction qui transforme un $\\lambda$-terme en une chaîne représentant une fonction \"anonyme\" exécutable par Python. Rappel : `lambda x: ...` correspond à $\\lambda x. <...>$"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val sprintf : ('a, unit, string) format -> 'a = \n"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"val python_of_terme : terme -> variable = \n"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let sprintf = Format.sprintf;;\n",
"\n",
"let rec python_of_terme = function\n",
" | V(s) -> s\n",
" | A(u, v) -> sprintf \"(%s)(%s)\" (python_of_terme u) (python_of_terme v)\n",
" | F(s, u) -> sprintf \"lambda %s: (%s)\" s (python_of_terme u)\n",
";;"
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"lambda x: (x)\n"
]
},
{
"data": {
"text/plain": [
"- : unit = ()\n"
]
},
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"lambda y: (y)\n"
]
},
{
"data": {
"text/plain": [
"- : unit = ()\n"
]
},
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"(lambda x: ((x)(x)))(lambda x: ((x)(x)))\n"
]
},
{
"data": {
"text/plain": [
"- : unit = ()\n"
]
},
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"print_endline (python_of_terme identite);;\n",
"print_endline (python_of_terme identite_2);;\n",
"print_endline (python_of_terme omega);;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On peut ensuite simplement appeler Python sur un terme et vérifier s'il s'exécute ou non."
]
},
{
"cell_type": "code",
"execution_count": 35,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val execute_python_string : string -> int = \n"
]
},
"execution_count": 35,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let execute_python_string (s : string) : int =\n",
" Sys.command (sprintf \"python -c 'print(%s)'\" s)\n",
";;"
]
},
{
"cell_type": "code",
"execution_count": 36,
"metadata": {
"scrolled": true
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
" at 0x7fd84099c5f0>\n"
]
},
{
"data": {
"text/plain": [
"- : int = 0\n"
]
},
"execution_count": 36,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"execute_python_string (python_of_terme identite);;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On peut vérifier avec Python que ce terme $\\Omega$ ne termine pas :"
]
},
{
"cell_type": "code",
"execution_count": 34,
"metadata": {
"scrolled": true
},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"Traceback (most recent call last):\n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"\", line 1, in \n",
" File \"