用户:CaffeineP/笔记/λ演算

      SUCC :=         λnfx.f ( n       f x)
0 :=                            λfx.x      ,    0 f x =      x
1 := SUCC 0 =          λfx.f ((λfx.x) f x)
             =          λfx.f        x      ,    1 f x =    f x
2 := SUCC 1 = λfx.f ((λfx.f        x) f x)
             = λfx.f (      f        x     ),    2 f x = f (f x)
...