$\lambda$
概念
函数的应用（application）是左结合的
| 语法 | 名称 |
|---|---|
| x | 变量 |
| ($\lambda$x.M) | 抽象化 |
| (M N) | 应用 |
两种变换
- $\alpha$ 等价 : 变量替换
- $\beta$ 规约 : 代值 如($\lambda$x.t)s 可化简为 t[$x$:= s]
捕获记法
假设 t， s 和 r 是 lambda 项，而 x 和 y 是变量。如果写成 t[x:=r] 是一种避免被捕获的记法方式，表示在 t 这个 lambda 项中，以 r 来替换 x 变量的值。
$\eta$变换
lambda 等价的规则
对于任一给定的参数，当且仅当两个函数得到的结果都一致，则它们将被视同为一个函数
church numerals
0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f x))
1
2
3
4
2
3
4
这里的问题是 0 的定义方法
使用高阶函数是为了与其他数字定义形式形同
f : 后继函数
x : 当前值/定义的 0 值
-- 加法定义
PLUS = λm.λn.λf.λx.m f (n f x)
-- 乘法定义
MULT = λm.λn.λf.m (n f)
1
2
3
4
2
3
4
bool
TRUE = λx.λy.x
FALSE = λx.λy.y -- 与 0 形式相同
1
2
2
这样的定义形式方便 if-else 之类二元形式的定义
AND = λp q.p q FALSE
OR = λp q.p TRUE q
NOT = λp.p FALSE TRUE
IFTHENELSE = λp x y.p x y
1
2
3
4
2
3
4
逻辑运算的理解
可以带入运算 走走流程
AND TRUE FALSE
≡(λp q.p q FALSE) TRUE FALSE =beta> TRUE FALSE FALSE
≡(λx y.x) FALSE FALSE =beta> FALSE
1
2
3
2
3
也可以理解为 每个变量的都是含两个参数的lambda 然后进行短路求值
Y 组合子
引入
lambda calculus 中 不能定义包含自身的函数
利用不动点性质来实现递归
f=g(f) g 的不动点
被表示为 Y
Y = λg.(λx.g(x x))(λx.g(x x))
1
Y g 是 g 的不动点
Y g=g(Y g)可以用代值证明
所有递归定义的函数都可以看作某个其他适当的函数的不动点，因此，使用
Y所有递归定义的函数都可以表达为lambda表达式
(Y Y)=Y(Y Y)
SKI组合子演算
可以将 lambda 演算中的表达式转换为 SKI 组合子演算中的表达式
SKI
I = λx.x
K = λx.λy.x <=> λx.c = Kc
S = λx.λy.λz.xz (yz) <=> λx.(y z) = S (λx.y) (λx.z)
SK
I = SKK
I I = I
K K I = K
S K S K = K
1
2
3
2
3
$ {\rm{I}} = \lambda x.x\ = \lambda x.{\rm K} x _\ => \lambda x.{\rm K} x ({\rm K}x)\ = \lambda x.{\rm SKK}x\ = SKK $
iota
$\iota,=\lambda$f.((f S) K)
I = ιι
K = ι(ιI) = ι(ι(ιι))
S = ι(K) = ι(ι(ι(ιι)))
1
2
3
2
3