open List;;
type lambda = Var of string | Abs of string * lambda | App of lambda * lambda;;
type recurs = Z | S | U of int * int | Sup of recurs * recurs list |
Rec of recurs * recurs | M of recurs;;
let rec n_vars r = match r with
Z -> 1
|S -> 1
|U (n,m) -> n
|Sup (g,fl) -> n_vars (hd fl)
|Rec (g,f) -> (n_vars f) + 1
|M f -> (n_vars f) - 1;;
let abs n x z = let rec abs' n m x z = if n>=m then Abs (x^(string_of_int m),
abs' n (m+1) x z) else z in abs' n 1 x z;;
let app n x z = let rec app' n m x z = if n>m then app' n (m+1) x
(App (z,Var (x^(string_of_int m)))) else
App (z,Var (x^(string_of_int m))) in app' n 1 x z;;
let app3 x z = let rec app2' n x z = if (length x)>(n+1) then
app2' (n+1) x (App (z,nth x n)) else (App (z,nth x n))
in app2' 0 x z;;
let rec laml r f = let rec f' r f acc = if (length r)>0 then
f' (tl r) f ((f^(string_of_int (length r)))::acc)
else acc in f' r f [];;
let app2 fl x = let n = n_vars (hd fl) in
map (fun y -> app n x (Var y)) (laml fl "f");;
let ycomb = Abs ("f",App (Abs ("x",(App (Var "f", App (Var "x", Var "x")))),
(Abs ("x",(App (Var "f", App (Var "x", Var "x")))))));;
let s = Abs ("x", Abs ("f", Abs ("t", App (App (Var "x", Var "f"),
App (Var "f", Var "t")))));;
let truel = Abs ("a", Abs ("b", Var "a"));;
let falsel = Abs ("a", Abs ("b", Var "b"));;
let snd = Abs ("p", App (Var "p", truel));;
let fst = Abs ("p", App (Var "p", falsel));;
let ifl = Abs ("c", Abs ("d", Abs ("h", App (App (Var "c", Var "d"), Var "h"))));;
let iszero = Abs ("n", App (App (Var "n", Abs ("x", falsel)), truel));;
let rec lambda_of_recurs r =
match r with
Z -> Abs ("x", Abs ("y", Abs ("t", Var "t")))
|S -> s
|U (n,m) -> abs n "x" (Var ("x"^(string_of_int m)))
|Sup (g,fl) -> Abs ("g",abs (length fl) "f" (abs (n_vars (hd fl))
"x" (app3 (app2 fl "x") (Var "g"))))
|Rec (g,f) -> let trec = Abs ("p", Abs ("s", App (App (Var "s", App (App (
app (n_vars f) "x" (Var "g"), App (snd, Var "p")), App (fst, Var "p"))),
App (s, App (snd, Var "p"))))) in
abs (n_vars f) "x" (Abs ("y", App (fst, App (App (Var "y", trec),
Abs ("s", App (App (Var "s", app (n_vars f) "x" (Var "f")),
falsel)) ))))
|M f -> Abs ("f", abs (n_vars f - 1) "x" (App (ycomb, Abs ("r", Abs ("y",
App (App (App (App (ifl, (App (iszero, App (app (n_vars f - 1) "x"
(Var "f"),Var "y")))), (Var "y")),(App (Var "r",
App (s,Var "y")))),falsel)))))) ;;
let rec string_of_lambda l =
match l with
Var x -> x
|Abs (x,y) -> "(\\"^x^"."^(string_of_lambda y)^")"
|App (x,y) -> "("^(string_of_lambda x)^" "^(string_of_lambda y)^")";;
let print_lambda x = print_string (string_of_lambda x);;
print_lambda (lambda_of_recurs (M Z));;