TP 6 : Lambda calcul, représentations, calculs et quelques termes pratiques.
let print = Printf.printf;;
Sys.command "ocaml -version";;
val print : ('a, out_channel, unit) format -> 'a = <fun>
The OCaml toplevel, version 4.04.2
- : int = 0
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) :
<exp> ::= <var>
| <exp>(<exp>)
| fun <var> -> <exp>
| (<exp>)
type variable = string;;
type terme =
| V of variable
| A of terme * terme
| F of variable * terme
;;
type variable = string
type terme = V of variable | A of terme * terme | F of variable * terme
Par exemple, l'identité est le terme $\lambda x. x$.
let identite = F("x", V("x"));;
File "[7]", line 1, characters 15-16: Warning 41: F belongs to several types: terme terme The first one was selected. Please disambiguate if this is wrong.
val identite : terme = F ("x", V "x")
let identite_2 = F("y", V("y"));;
File "[8]", line 1, characters 17-18: Warning 41: F belongs to several types: terme terme The first one was selected. Please disambiguate if this is wrong.
val identite_2 : terme = F ("y", V "y")
Les deux termes sont différents mais égaux à $\alpha$-renomage près.
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 si besoin).
let omega = A(F("x", A(V("x"), V("x"))), F("x", A(V("x"), V("x"))));;
File "[9]", line 1, characters 12-13: Warning 41: A belongs to several types: terme terme The first one was selected. Please disambiguate if this is wrong.
val omega : terme = A (F ("x", A (V "x", V "x")), F ("x", A (V "x", V "x")))
let u = F("x", A(V("x"), V("x")));;
let omega = A(u, u);
File "[10]", line 1, characters 8-9: Warning 41: F belongs to several types: terme terme The first one was selected. Please disambiguate if this is wrong.
val u : terme = F ("x", A (V "x", V "x"))
File "[10]", line 2, characters 12-13: Warning 41: A belongs to several types: terme terme The first one was selected. Please disambiguate if this is wrong.
val omega : terme = A (F ("x", A (V "x", V "x")), F ("x", A (V "x", V "x")))
C'est très rapide.
let sprintf = Format.sprintf;;
let rec string_of_terme = function
| V(s) -> s
| A(u, v) -> sprintf "(%s)(%s)" (string_of_terme u) (string_of_terme v)
(* "(" ^ (string_of_terme u) ^ ")" ^ "(" ^ (string_of_terme v) ^ ")" *)
| F(s, u) -> sprintf "λ %s. (%s)" s (string_of_terme u)
(* "lambda " ^ s ^ ".(" ^ (string_of_terme u) *)
;;
val sprintf : ('a, unit, string) format -> 'a = <fun>
File "[13]", line 4, characters 6-7: Warning 41: V belongs to several types: terme terme The first one was selected. Please disambiguate if this is wrong.
val string_of_terme : terme -> variable = <fun>
print_endline (string_of_terme identite);;
print_endline (string_of_terme identite_2);;
print_endline (string_of_terme omega);;
λ x. (x)
- : unit = ()
λ y. (y)
- : unit = ()
(λ x. ((x)(x)))(λ x. ((x)(x)))
- : unit = ()
lambda x: ... correspond à $\lambda x. <...>$¶let sprintf = Format.sprintf;;
let rec python_of_terme = function
| V(s) -> s
| A(u, v) -> sprintf "(%s)(%s)" (python_of_terme u) (python_of_terme v)
| F(s, u) -> sprintf "lambda %s: (%s)" s (python_of_terme u)
;;
val sprintf : ('a, unit, string) format -> 'a = <fun>
val python_of_terme : terme -> variable = <fun>
print_endline (python_of_terme identite);;
print_endline (python_of_terme identite_2);;
print_endline (python_of_terme omega);;
lambda x: (x)
- : unit = ()
lambda y: (y)
- : unit = ()
(lambda x: ((x)(x)))(lambda x: ((x)(x)))
- : unit = ()
On peut ensuite simplement appeler Python sur un terme et vérifier s'il s'exécute ou non.
let execute_python_string (s : string) : int =
Sys.command (sprintf "python -c 'print(%s)'" s)
;;
val execute_python_string : string -> int = <fun>
execute_python_string (python_of_terme identite);;
<function <lambda> at 0x7fd84099c5f0>
- : int = 0
On peut vérifier avec Python que ce terme $\Omega$ ne termine pas :
execute_python_string (python_of_terme omega);;
Traceback (most recent call last): File "<string>", line 1, in <module> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda>
- : int = 1
File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> File "<string>", line 1, in <lambda> RuntimeError: maximum recursion depth exceeded
On peut définir des $\lambda$-termes utiles avec notre représentation, et on vérifiera ensuite en les exécutant via Python qu'ils sont corrects.
let none = F("x", V("x"));;
val none : terme = F ("x", V "x")
let compose u v = A(u, v);;
val compose : terme -> terme -> terme = <fun>
Ce n'est qu'un des encodages possibles.
let si = F("cond", F("v", F("f", A(A(V("cond"), V("v")), V("f")))));;
val si : terme = F ("cond", F ("v", F ("f", A (A (V "cond", V "v"), V "f"))))
print_endline (string_of_terme si);;
λ cond. (λ v. (λ f. (((cond)(v))(f))))
- : unit = ()
let vrai = F("v", F("f", V("v")));;
let faux = F("v", F("f", V("f")));;
val vrai : terme = F ("v", F ("f", V "v"))
val faux : terme = F ("v", F ("f", V "f"))
print_endline (string_of_terme vrai);;
print_endline (string_of_terme faux);;
λ v. (λ f. (v))
- : unit = ()
λ v. (λ f. (f))
- : unit = ()
On rappelle que pour $n \in \mathbb{N}$, $[n] = \lambda f. \lambda x. f^n(x)$ est son codage dit codage de Church dans les $\lambda$-termes.
let zero = F("f", F("x", V("x")));;
let un = F("f", F("x", A(V("f"), V("x"))));;
val zero : terme = F ("f", F ("x", V "x"))
val un : terme = F ("f", F ("x", A (V "f", V "x")))
let terme_of_int (n : int) : terme =
let rec aux = function
| 0 -> V("x")
| n -> A(V("f"), aux (n-1))
in
F("f", F("x", (aux n)))
;;
val terme_of_int : int -> terme = <fun>
let deux = terme_of_int 2;;
val deux : terme = F ("f", F ("x", A (V "f", A (V "f", V "x"))))
print_endline (string_of_terme deux);;
execute_python_string (python_of_terme deux);;
λ f. (λ x. ((f)((f)(x))))
- : unit = ()
<function <lambda> at 0x7f453cab55f0>
- : int = 0
On peut faire l'opération inverse, interpréter un entier de Church en Python.
let entier_natif_python = "lambda c: c(lambda x: x+1)(0)";;
val entier_natif_python : string = "lambda c: c(lambda x: x+1)(0)"
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme deux));;
2
- : int = 0
On est obligé de passer par une astuce, parce que $\lambda x. x + 1$ et $0$ ne sont pas des $\lambda$-termes.
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (terme_of_int 10)));;
10
- : int = 0
Bien sûr, tout ça est très limité !
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (terme_of_int 100)));;
s_push: parser stack overflow MemoryError
- : int = 1
Le successeur s'écrit $\mathrm{succ} = \lambda n. \lambda f. \lambda z. f(n(f)(z))$.
let successeur = F("n", F("f", F("z", A(V("f"), A(A(V("n"), V("f")), V("z"))))));;
val successeur : terme =
F ("n", F ("f", F ("z", A (V "f", A (A (V "n", V "f"), V "z")))))
print_endline (string_of_terme successeur);;
λ n. (λ f. (λ z. ((f)(((n)(f))(z)))))
- : unit = ()
let dix = terme_of_int 10;;
let onze = A(successeur, dix);;
val dix : terme =
F ("f",
F ("x",
A (V "f",
A (V "f",
A (V "f",
A (V "f",
A (V "f",
A (V "f", A (V "f", A (V "f", A (V "f", A (V "f", V "x"))))))))))))
val onze : terme =
A (F ("n", F ("f", F ("z", A (V "f", A (A (V "n", V "f"), V "z"))))),
F ("f",
F ("x",
A (V "f",
A (V "f",
A (V "f",
A (V "f",
A (V "f",
A (V "f", A (V "f", A (V "f", A (V "f", A (V "f", V "x")))))))))))))
A noter que ce terme onze ne sera pas le même que celui (plus court) obtenu par terme_of_int 11 :
let onze2 = terme_of_int 11;;
val onze2 : terme =
F ("f",
F ("x",
A (V "f",
A (V "f",
A (V "f",
A (V "f",
A (V "f",
A (V "f",
A (V "f", A (V "f", A (V "f", A (V "f", A (V "f", V "x")))))))))))))
Mais ils s'exécutent de la même façon :
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme dix));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme onze));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme onze2));;
10
- : int = 0
11
- : int = 0
11
- : int = 0
La somme s'écrit $\mathrm{somme} = \lambda n. \lambda m. \lambda f. \lambda z. n(f)(m(f)(z))$.
let somme = F("n", F("m", F("f", F("z", A((A(V("n"), V("f"))), A((A(V("m"), V("f"))), V("z")) )))));;
val somme : terme =
F ("n",
F ("m",
F ("f", F ("z", A (A (V "n", V "f"), A (A (V "m", V "f"), V "z"))))))
print_endline (string_of_terme somme);;
λ n. (λ m. (λ f. (λ z. (((n)(f))(((m)(f))(z))))))
- : unit = ()
let trois = A(A(somme, un), deux);;
val trois : terme =
A
(A
(F ("n",
F ("m",
F ("f", F ("z", A (A (V "n", V "f"), A (A (V "m", V "f"), V "z")))))),
F ("f", F ("x", A (V "f", V "x")))),
F ("f", F ("x", A (V "f", A (V "f", V "x")))))
Comme pour le successeur, ce terme est bien plus compliqué que l'encodage de Church, mais ils s'exécutent de la même manière.
let trois2 = terme_of_int 3;;
val trois2 : terme = F ("f", F ("x", A (V "f", A (V "f", A (V "f", V "x")))))
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme trois));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme trois2));;
3
- : int = 0
3
- : int = 0
La multiplication est $\mathrm{mul} = \lambda n. \lambda m. \lambda f. \lambda z. m(n(f))(z)$.
let mul = F("n", F("m", F("f", F("z", A(A(V("m"), A(V("n"), V("f"))), V("z"))))));;
val mul : terme =
F ("n", F ("m", F ("f", F ("z", A (A (V "m", A (V "n", V "f")), V "z")))))
let trois = terme_of_int 3 ;;
let six = A(A(mul, trois), deux);;
let six2 = A(A(mul, deux), trois);;
val trois : terme = F ("f", F ("x", A (V "f", A (V "f", A (V "f", V "x")))))
val six : terme =
A
(A
(F ("n",
F ("m", F ("f", F ("z", A (A (V "m", A (V "n", V "f")), V "z"))))),
F ("f", F ("x", A (V "f", A (V "f", A (V "f", V "x")))))),
F ("f", F ("x", A (V "f", A (V "f", V "x")))))
val six2 : terme =
A
(A
(F ("n",
F ("m", F ("f", F ("z", A (A (V "m", A (V "n", V "f")), V "z"))))),
F ("f", F ("x", A (V "f", A (V "f", V "x"))))),
F ("f", F ("x", A (V "f", A (V "f", A (V "f", V "x"))))))
Comme pour le successeur, ce terme est bien plus compliqué que l'encodage de Church, mais ils s'exécutent de la même manière.
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme six));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme six2));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (terme_of_int 6)));;
6
- : int = 0
6
- : int = 0
6
- : int = 0
La représentation de la paire est simplement $\mathrm{pair} = \lambda a. \lambda b. \lambda f. f(a)(b)$.
let a = V("a") and b = V("b") and f = V("f");;
let pair = F("a", F("b", F("f", A(A(f, a), b))));;
val a : terme = V "a" val b : terme = V "b" val f : terme = V "f"
val pair : terme = F ("a", F ("b", F ("f", A (A (V "f", V "a"), V "b"))))
Et ensuite les deux extracteurs sont immédiats : $\mathrm{gauche} = \lambda p. p(\lambda a. \lambda b. a)$ et $\mathrm{droite} = \lambda p. p(\lambda a. \lambda b. b)$.
(on retrouve vrai et faux)
let gauche = F("f", A(f, vrai));;
let droite = F("f", A(f, faux));;
val gauche : terme = F ("f", A (V "f", F ("v", F ("f", V "v"))))
val droite : terme = F ("f", A (V "f", F ("v", F ("f", V "f"))))
let exemple_pair = A(A(pair, deux), trois);;
val exemple_pair : terme =
A
(A (F ("a", F ("b", F ("f", A (A (V "f", V "a"), V "b")))),
F ("f", F ("x", A (V "f", A (V "f", V "x"))))),
F ("f", F ("x", A (V "f", A (V "f", A (V "f", V "x"))))))
On vérifie qu'on peut extraire [2] et [3] de cette paire [(2, 3)] :
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (A(gauche, exemple_pair))));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (A(droite, exemple_pair))));;
2
- : int = 0
3
- : int = 0
Avec les paires, c'est possible. Idée de l'algorithme : en ayant
[n], on commence par la paire[(0, 0)]et on itère la fonctionfun (a,b) -> (a+1, a)exactementnfois (et ça c'est facile par définition du codage[n], ce qui donne la paire[(n, n-1)]et en récupérant la deuxième coordonnée on a[n-1]. C'est corrigé en Exercice 12 du poly de Jean Goubault-Larrecqu.
On va découper ça en morceau :
let constructeur_pair u v = A(A(pair, u), v);;
let pi1 u = A(gauche, u);;
let pi2 u = A(droite, u);;
let constructeur_succ u = A(successeur, u);;
let pair_00 = constructeur_pair zero zero;;
val constructeur_pair : terme -> terme -> terme = <fun>
val pi1 : terme -> terme = <fun>
val pi2 : terme -> terme = <fun>
val constructeur_succ : terme -> terme = <fun>
val pair_00 : terme =
A
(A (F ("a", F ("b", F ("f", A (A (V "f", V "a"), V "b")))),
F ("f", F ("x", V "x"))),
F ("f", F ("x", V "x")))
let p = V("p");;
let succ_1 = F("p", constructeur_pair (constructeur_succ(pi1(p))) (pi1(p)));;
val p : terme = V "p"
val succ_1 : terme =
F ("p",
A
(A (F ("a", F ("b", F ("f", A (A (V "f", V "a"), V "b")))),
A (F ("n", F ("f", F ("z", A (V "f", A (A (V "n", V "f"), V "z"))))),
A (F ("f", A (V "f", F ("v", F ("f", V "v")))), V "p"))),
A (F ("f", A (V "f", F ("v", F ("f", V "v")))), V "p")))
let n = V("n");;
let predecesseur = F("n", pi2(A(A(n, succ_1), pair_00)));;
val n : terme = V "n"
val predecesseur : terme =
F ("n",
A (F ("f", A (V "f", F ("v", F ("f", V "f")))),
A
(A (V "n",
F ("p",
A
(A (F ("a", F ("b", F ("f", A (A (V "f", V "a"), V "b")))),
A
(F ("n",
F ("f", F ("z", A (V "f", A (A (V "n", V "f"), V "z"))))),
A (F ("f", A (V "f", F ("v", F ("f", V "v")))), V "p"))),
A (F ("f", A (V "f", F ("v", F ("f", V "v")))), V "p")))),
A
(A (F ("a", F ("b", F ("f", A (A (V "f", V "a"), V "b")))),
F ("f", F ("x", V "x"))),
F ("f", F ("x", V "x"))))))
let cinq = A(predecesseur, (terme_of_int 6));;
let cinq2 = terme_of_int 5;;
val cinq : terme =
A
(F ("n",
A (F ("f", A (V "f", F ("v", F ("f", V "f")))),
A
(A (V "n",
F ("p",
A
(A (F ("a", F ("b", F ("f", A (A (V "f", V "a"), V "b")))),
A
(F ("n",
F ("f", F ("z", A (V "f", A (A (V "n", V "f"), V "z"))))),
A (F ("f", A (V "f", F ("v", F ("f", V "v")))), V "p"))),
A (F ("f", A (V "f", F ("v", F ("f", V "v")))), V "p")))),
A
(A (F ("a", F ("b", F ("f", A (A (V "f", V "a"), V "b")))),
F ("f", F ("x", V "x"))),
F ("f", F ("x", V "x")))))),
F ("f",
F ("x",
A (V "f", A (V "f", A (V "f", A (V "f", A (V "f", A (V "f", V "x")))))))))
val cinq2 : terme =
F ("f",
F ("x", A (V "f", A (V "f", A (V "f", A (V "f", A (V "f", V "x")))))))
Comme pour le successeur, ce terme est bien plus compliqué que l'encodage de Church, mais ils s'exécutent de la même manière.
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme cinq));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme cinq2));;
5
- : int = 0
5
- : int = 0
On vérifie que pred 0 = 0 :
let zero2 = A(predecesseur, zero);;
val zero2 : terme =
A
(F ("n",
A (F ("f", A (V "f", F ("v", F ("f", V "f")))),
A
(A (V "n",
F ("p",
A
(A (F ("a", F ("b", F ("f", A (A (V "f", V "a"), V "b")))),
A
(F ("n",
F ("f", F ("z", A (V "f", A (A (V "n", V "f"), V "z"))))),
A (F ("f", A (V "f", F ("v", F ("f", V "v")))), V "p"))),
A (F ("f", A (V "f", F ("v", F ("f", V "v")))), V "p")))),
A
(A (F ("a", F ("b", F ("f", A (A (V "f", V "a"), V "b")))),
F ("f", F ("x", V "x"))),
F ("f", F ("x", V "x")))))),
F ("f", F ("x", V "x")))
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme zero2));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme zero));;
0
- : int = 0
0
- : int = 0