◇ Untyped λ-Calcs ◇
完全ベータ簡約です. 最も内側の式から評価されます.
よって不動点コンビネーターは停止しません.
記号に"="で式を代入できます.
0 = λf x. x 1 = succ 0 2 = succ 1 3 = succ 2 succ = λn f x. f (n f x) plus = λm n f x. m f (n f x) pred = λn f x. n (λg h. h (g f)) (λu. x) (λu. u) mult = λm n f. m (n f) tru = λx y. x fls = λx y. y ∧ = λp q. p q fls ∨ = λp q. p tru q ￢ = λp. p fls tru if = λp x y. p x y iszero = λn. n (λx. fls) tru succ 2
result: