Эквивалентность лямбда-исчисления рекурсивным функциям: преобразование рекурсивной функции в лямбда-выражение.
Code
Z (x) = 0
S (x) = x + 1
U (n, m) (x1, ..., xm) = xn
Sup (f, h1, ..., hn) = f (h1 (x1, ..., xm)) (h2 (x1, ..., xm)) ... (hn (x1, ..., xm))
Rec (g, f) (x1, ..., xn, y) =
y = 0 | f (x1, ..., xn)
y > 0 | g (x1, ..., xn, y, Rec (g, f) (x1, ..., xn, y - 1))
Mu (f) (x1, ..., xn) = min y, такой что f (x1, ..., xn) = 0
Code
Z = \x.0
S = \n.\f.\x.n f (f x)
U = \x1.\x2....\xm.xn
Sup = \f.\h1.\h2....\hn.\x1.\x2....\xm.f (h1 x1 x2 ... xm) (h2 x1 x2 ... xm) ... (hn x1 x2 ... xm)
Mu = \f.\x1.\x2....\xn.Y (\r.\y.(IsZero (f x1 x2 ... xn y)) y (r (Inc y) 0))
T = \p.<g x1 x2 ... xn (snd p) (fst p), Inc (snd p)>
Rec = \f.\g.\x1.\x2....\xn.\y.fst (y T <f x1 x2 ... xn, 0>)
Это - перепечатка с моего конспекта. Я не верю в реализацию минимизации, так как до сих пор плохо понимаю, как работает Y-комбинатор. (что, чёрт возьми, значит выражение (r (Inc y) 0)?!) Остальное же выглядит правдоподобно.