λ-演算¶

$\lambda$-演算没有结合律

证：

假设结合律成立，则 $K(II)=(KI)I$，即 $KI=I$。则 $KIM=IM$，即 $I=M$。同理 $I=N$，故 $M=N$，不一致，矛盾。

递归函数的λ-可定义性¶

注意

在定义3.33中，归纳定义了$F^nM$为 $$ \begin{align} F^0M&\equiv M,\\ F^{n+1}M&\equiv F(F^nM); \end{align} $$ 即 $F^nM\equiv F(\cdots(F(FM)))$. 注意和左结合的区别，左结合在约定3.3（4）：$FM_1M_2\cdots M_n\equiv (\cdots((FM_1)M_2)\cdots M_n)$

Church数项

对于 $n\in\mathbb{N}$, Church数项 $\ulcorner n\urcorner$ 定义为 $$ \ulcorner n\urcorner \equiv λfx.f^n x $$

常用性质：

$f^nx=\ulcorner n\urcorner fx$

λ-定义几个常见函数的 λ-term¶

后继函数：$Suc ≡ λxyz.y(xyz)$
清零函数：$Z ≡ λx. \ulcorner 0\urcorner$
投影函数：$U^n_i\equiv \lambda x_1\cdots x_n.x_i$
前驱（by Kleene）：$\text{Pred}\equiv (λx.xC [ \ulcorner 1 \urcorner , \ulcorner 0 \urcorner , \ulcorner 0 \urcorner ] U^3_3$，其中 $C\equiv \lambda z.[S(zU^3_1), zU^3_1, zU^3_2]$
加法(by J. B. Rosser)：$A_+ \equiv λxypq.xp(ypq)$
乘法(by J. B. Rosser)：$A_∗ \equiv λxyz.x(yz)$
幂(by J. B. Rosser)：$\text{Exp} \equiv λxy.yx$
减法：$Sub \equiv λxy.y \text{Pred} x$
真：$\text{True} \equiv K \equiv U^2_1$
真：$\text{False} \equiv K^* \equiv U^2_2$
非：$Not \equiv λx.x \text{False} \text{True}$
IF THEN ELSE：$\text{IF} \equiv λxyz.xyz$
AND：$\text{AND}\equiv λxy.xy\text{False}$
零测试函数（就是书上的 D）：$\text{Zero} \equiv λx.x(K\text{False})\text{True}$
等于：$\text{EQ}\equiv λxy.\text{AND}(\text{Zero}(\text{Sub} xy)) (\text{Zero}(\text{Sub} yx))$
除法(受Kleene Pred启发，此法能解决需要有限个临时变量的问题)：$\text{DIV}\equiv \lambda xy.z(\lambda z.\text{EQ}(\text{Suc}(zU^2_2))y[\text{Suc}(zU^2_1),\ulcorner 0\urcorner][zU^2_1,\text{Suc}(zU^2_2)])[\ulcorner 0\urcorner,\ulcorner 0\urcorner]U^2_1$
取模（很类似于除法，一处不同）：$\text{MOD}\equiv \lambda xy.z(\lambda z.\text{EQ}(\text{Suc}(zU^2_2))y[\text{Suc}(zU^2_1),\ulcorner 0\urcorner][zU^2_1,\text{Suc}(zU^2_2)])[\ulcorner 0\urcorner,\ulcorner 0\urcorner]U^2_2$