《计算模型导引》第三章习题

12

习题3.12

证明：对于任何 $M,N\in \Lambda$，若 $M =_{\beta} N$，则存在 $T$ 使 $M\twoheadrightarrow_{\beta} T$ 且 $N \twoheadrightarrow_{\beta} T$. 这就是对于 $=_{\beta}$ 的CR性质.

证：

设 $M=_{\beta} N$，由习题3.9知，存在 $P_0,\cdots, P_n\in\nabla$ 使得 $M\equiv P_0$ 且 $N\equiv P_n$ 且 $\forall i < n, P_i\rightarrow_{\beta} P_{i+1}$ 或 $P_i\leftarrow_{\beta} P_{i+1}$.

以下对 $i$ 归纳证明，存在 $T_i$ 使得 $P_0\twoheadrightarrow_{\beta} T_i$ 且 $P_n\twoheadrightarrow_{\beta} T_i$.

奠基：$i=0$，取 $T_0$ 为 $M$ 即可.

假设 $i=k$ 时结论成立.

$i=k+1 < n$ 时，由归纳假设，$P_0\twoheadrightarrow_{\beta} T_k$ 且 $P_k\twoheadrightarrow_{\beta} T_k$.

当 $P_k\rightarrow_{\beta} P_{k+1}$，从而由CR性质，存在 $T_{k+1}$ 使得 $T_k\twoheadrightarrow_{\beta} T_{k+1}$ 且 $P_{k+1}\twoheadrightarrow_{\beta} T_{k+1}$，从而结论成立.

当 $P_k\leftarrow_{\beta} P_{k+1}$，取 $T_{k+1}$ 为 $P_k$ 即可，这时结论成立。

综上，有 $T_n$ 使得 $P_0\twoheadrightarrow_{\beta} T_n$ 且 $P_n\twoheadrightarrow_{\beta} T_n$. 取 $T$ 为 $T_0$，即有 $M\twoheadrightarrow_{\beta} T$ 且 $N \twoheadrightarrow_{\beta} T$.

13

习题3.13

证明：若在系统 $\lambda\beta$ 中加入下述公理 $$ (A)\qquad \lambda xy. x = \lambda xy. y, $$ 则对任何$M,N\in \Lambda$，$\lambda\beta + (A) \vdash M = N$.

证：

对任何 $M,N\in\Lambda$，

$$\begin{align} (\lambda xy. x) MN &=(\lambda xy. y) MN \\\\ M &= N \end{align}$$

14

习题3.14

证明命题3.14：

设 $R$ 是 $\nabla$ 上的一个二元关系，$M\in NF_R$，则

(1) 不存在 $N\in\nabla$ 使得 $M\rightarrow_R N$;

(2) $M\twoheadrightarrow_R N \Rightarrow M\equiv N$.

证：

(1)

若存在 $N\in\nabla, M\rightarrow_R N$，则由定义知 $M$ 为 R-可约式，矛盾.

(2)

假设 $M\not\equiv N$，$M\twoheadrightarrow_R N$ 表示存在 $M = P_0\rightarrow_R P_1\rightarrow_R\cdots\rightarrow_R P_n = N$，使得对于 $i < n$，$P_i\rightarrow_R P_{i+1}$. 因为 $M\not\equiv N$，我们有 $n\geq 1$，但是这样存在 $N$，使得 $M\rightarrow_R N$，与(1)结论矛盾.

15

习题3.15

证明引理3.16：

若 $M\vartriangleright_{mcd} M'$ 且 $N\vartriangleright_{mcd} N'$，则 $M'N' \vartriangleright_{mcd} M'N'$.

证：

设 $M$ 通过 $P_1, P_2, \cdots, P_{n1}$ 收缩到 $M′$, $N$ 通过 $R_1, R_2, \cdots, R_{n2}$ 收缩到 $N′$, 如果将这种极小规约过程看成大小关系的话, 那么 $P_1,P_2,\cdots, P_{n1}$ 与 $R_1, R_2, \cdots, R_{n2}$ 都可以视为按照非降序来排列. 那么现在只需要用任意一种排序算法将 $P_1, P_2, \cdots, P_{n2}, R_1, R_2, \cdots, R_{n2}$, 按照非降序排列, 则可以通过该序列将 $MN$ 收缩到 $M′N′$.

16

习题3.16

试找出 $A\in\Lambda^{\circ}$使$A$ $\lambda$-定义函数 $f(x,y)=x+y$.

解：

解法一：

$$\begin{align} \ulcorner x+y \urcorner &=S^y\ulcorner x\urcorner \\\\ &=\ulcorner y\urcorner S \ulcorner x\urcorner \\\\ &=(\lambda uv. vSu)\ulcorner x\urcorner\ulcorner y\urcorner \end{align}$$

其中 $S$ 为后继函数，定义在引理3.30，为$\lambda xyz.y(xyz)$.

解法二：

$$\begin{align} \ulcorner x+y \urcorner &=\lambda uv. u^{x+y}v \\\\ &=\lambda uv. u^{x}(u^yv) \\\\ &=\lambda uv. u^{x}(\ulcorner y\urcorner uv) \\\\ &=\lambda uv. \ulcorner x\urcorner u(\ulcorner y\urcorner uv) \\\\ &=(\lambda abuv. a u(b uv))\ulcorner x\urcorner\ulcorner y\urcorner \end{align}$$

解法三：

$$f(x,y)=\text{if }y=0\text{ then }x\text{ else }f(x+1,y-1)$$

故定义 $F\in\Lambda^{\circ}$为

$$\begin{align} F\ulcorner x\urcorner\ulcorner y\urcorner &=D(\ulcorner y\urcorner)\ulcorner x\urcorner(F\ulcorner x+1\urcorner\ulcorner y-1\urcorner)\\\\ &=(\lambda zxy. D(y)x(z(Sx)(\text{pred } y)))F\ulcorner x\urcorner\ulcorner y\urcorner \end{align}$$

故 $F=\mathbb{Y}(\lambda zxy. D(y)x(z(Sx)(\text{pred } y)))$

17

习题3.17

试找出 $F\in\Lambda^{\circ}$使$F$ $\lambda$-定义函数 $f(x)=3x$.

解：

$$\begin{align} \ulcorner 3x \urcorner &=\lambda uv. u^{x+x+x}v \\\\ &=\lambda uv. u^{x}(u^x(u^xv)) \\\\ &=\lambda uv. u^{x}(u^x(\ulcorner x\urcorner uv)) \\\\ &=\lambda uv. u^{x}(\ulcorner x\urcorner u(\ulcorner x\urcorner uv)) \\\\ &=\lambda uv. \ulcorner x\urcorner u(\ulcorner x\urcorner u(\ulcorner x\urcorner uv)) \\\\ &=(\lambda xuv. x u(x u(x uv)))\ulcorner x\urcorner \end{align}$$

18

习题3.18

令 $D\equiv \lambda xyz.z(Ky)x$，证明：对于任意的 $X,Y\in\Lambda$， $$ \begin{align} DXY\ulcorner 0\urcorner &= X,\\ DXY\ulcorner n+1\urcorner &= Y. \end{align} $$ 这里$K\equiv \lambda xy.x$， $\ulcorner n\urcorner\equiv \lambda fx.f^n x$.

证：

$$\begin{align} DXY\ulcorner 0\urcorner &=(\lambda xyz. z(Ky)x)XY\ulcorner 0\urcorner \\\\ &=\ulcorner 0\urcorner(KY)X \\\\ &=(\lambda fx. x)(KY)X \\\\ &=X \end{align}$$

$$\begin{align} DXY\ulcorner n+1\urcorner &=(\lambda xyz. z(Ky)x)XY\ulcorner n+1\urcorner \\\\ &=\ulcorner n+1\urcorner(KY)X \\\\ &=(\lambda fx.f^{n+1} x)(KY)X \\\\ &=(KY)^{n+1}X \\\\ &=(KY)^nY \\\\ &\cdots \\\\ &=Y \end{align}$$