在 (lambda (x) (x y…)) 中, x 是绑定的变量, y 是自由变量

在 (lambda (x) (lambda (y) (x y …))) 中, 要分情况
在第一个 lambda 中, x, y 都是绑定的, 在 第二个 lambda中, x是自由变量

(lambda (x) (if (= x 0) 1 0))
;; 等价于
(lambda (y) (if (= y 0) 1 0))

(lambda (x) (x)) = (lambda (t) (t))

用 y 替换 x, 用 [y/x] 表示.
例如

(lambda (x) (x))
==> [y/x]x ==> y

一个测试的地方, 注意写法.

((lambda (x) (+ x 1)) 3)                ; 4

((lambda (y) (lambda (+ x y))) q)       ; (lambda (x) (+ x q))


((lambda (x y) (x y))
 (lambda (z) (* z z)) 3)                ; ((lambda (z) (* z z)) 3)
                                        ; 9

定义 0: (lambda (s z) (z))
定义 1: (lambda (s z) (s z))
定义 2: (lambda (s z) (s (s z)))

加法定义:

let add = (lambda (s z x y) (x s (y s z)))
相当于 let add = (lambda (x y) (lambda (s z) (x s (y s ))))

现在來看一下 (add 2 3):

(add (lambda (s z) (s (s z)))
     (lambda (s z) (s (s (s z)))))

==>

(lambda (s z)
     ((lambda (s2 z2) (s2 (s2 z2))) s
     ((lambda (s3 z3) (s3 (s3 (s3 z3)))) s z)))

先把 s z 搞进 s3 和 z 3
==>

(lambda (s z)
     ((lambda (s2 z2) (s2 (s2 z3))) s
     (s (s (s z)))))

把 s2 换成 s, z2换成 (s (s (s z)))
==>

(lambda (s z)
     (s (s (s (s (s z))))))

==> 5

let TRUE  = (lambda (x y) x)
let FALSE = (lambda (x y) y)

let AND   = (lambda (x y) (x y FALSE)
let OR    = (lambda (x y) (x TRUE y)
let NOT   = (lambda (x) (x FALSE TRUE)

下面你就会看到为什么要这么定义, 但是 哪个变态能想到这么巧合…

我们來试下 (AND TRUE FALSE), 展开

((lambda (xt yt) xt)
 ((lambda (xf yf) yf) FALSE))

來一次 beta, 用 ((lambda (xf yf) yf) FALSE) 代替 (xt yt)
==> (lambda (xf yf) yf) ; 这和 FALSE 的定义一样

(AND FALSE TRUE), 展开

((lambda (xf yf) yf) ((lambda (xt yt) yt) FALSE))

==> FALSE

(AND FALSE FALSE), 展开

((lambda (xf yf) yf) ((lambda (xf yf) yf) FLASE))

==> FLASE

(AND TRUE TRUE), 展开

((lambda (xt yt) xt) ((lambda xt yt) xt) FALSE)

==>

(lambda (xt yt) xt)

==>TRUE ; 这和 TRUE 的定义一样

更多强大的公式也是可以验证的. 为什么有人会想到这些…

let Y = (lambda (y) ((lambda (x) (y (x x)))
                     (lambda (x) (y (x x)))))

现在我们要证明一个变态的东西 Y Y = Y (Y Y)

((lambda (y) ((lambda (x) (y (x x)))
              (lambda (x) (y (x x))))) Y)

==>

((lambda (x) (Y (x x)))
 (lambda (x) (Y (x x))))

把 (lambda (x) (Y (x x)))) 替换 x
==>

(Y ((lambda (x) (Y (x x)))
     (lambda (x) (Y (x x)))))

==> (Y Y) == (Y (Y Y))

展开 第一个Y,
==>

((lambda (y) ((lambda (x) (y (x x)))
              (lambda (x) (y (x x)))))
    ((lambda (x) (Y (x x)))
     (lambda (x) (Y (x x)))))

用 ((lambda (x) (Y (x x))) (lambda (x) (Y (x x)))) 替换 y,
接着我们可以用 (lambda (x) (Y (x x))) 和 (lambda (x) (Y (x x)))
分别替换 y后面的 2个(lambda (x)..), 为避免混乱, 用 a, b去替换
==>

((lambda (a) (((lambda (x) (Y (x x))) (lambda (x) (Y (x x)))) (a a)))
 (lambda (b) (((lambda (x) (Y (x x))) (lambda (x) (Y (x x)))) (b b)))

==> Y Y == YYY… (自己搞…)