λ-演算¶

$\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$