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

19

习题3.19

设 $\text{Exp}\equiv \lambda xy.yx$，证明：对于任意的 $n\in\mathbb{N}$和$m\in\mathbb{N}^*$， $$ \text{Exp}\ulcorner n\urcorner\ulcorner m\urcorner =_{\beta} \ulcorner n^m\urcorner. $$ (Exp由Rosser教授作出)

证：

对$m$作数学归纳。

当 $m=1$ 时，

$$\begin{align} \text{Exp}\ulcorner n\urcorner\ulcorner 1\urcorner &= \ulcorner 1\urcorner\ulcorner n\urcorner \\\\ &= (\lambda fx. fx)\ulcorner n\urcorner \\\\ &= \lambda x. \ulcorner n\urcorner x \\\\ &= \lambda x. (\lambda fy. f^ny) x \\\\ &= \lambda x. (\lambda y. x^ny) \\\\ &= \lambda xy. x^ny\\\\ &= \ulcorner n\urcorner \end{align}$$

假设 $m=k$ 时成立，

$$\begin{align} {}&{}& \text{Exp}\ulcorner n\urcorner\ulcorner k\urcorner &= \ulcorner n^k\urcorner\\\\ \Rightarrow&& \ulcorner k\urcorner\ulcorner n\urcorner &= \lambda fy. f^{n^k}y \\\\ \Rightarrow&& (\lambda fy. f^ky)\ulcorner n\urcorner &= \lambda fy. f^{n^k}y \\\\ \Rightarrow&& \lambda y. \ulcorner n\urcorner^ky &= \lambda fy. f^{n^k}y \\\\ \Rightarrow&& (\lambda y. \ulcorner n\urcorner^ky)x &= (\lambda fy. f^{n^k}y)x \\\\ \Rightarrow&& \ulcorner n\urcorner^kx &= \lambda y. x^{n^k}y \\\\ \end{align}$$

当 $m=k+1$ 时，

$$\begin{align} \text{Exp}\ulcorner n\urcorner\ulcorner k+1\urcorner &= \ulcorner k+1\urcorner\ulcorner n\urcorner \\\\ &= (\lambda fx. f^{k+1}x)\ulcorner n\urcorner \\\\ &= \lambda x. \ulcorner n\urcorner^{k+1} x \\\\ &= \lambda x. \ulcorner n\urcorner(\ulcorner n\urcorner^{k} x) \\\\ &= \lambda x. \ulcorner n\urcorner(\lambda y. x^{n^k}y) \\\\ &= \lambda x. (\lambda fz. f^nz)(\lambda y. x^{n^k}y) \\\\ &= \lambda x. (\lambda z. (\lambda y. x^{n^k}y)^nz) \\\\ &= \lambda xz. (\lambda y. x^{n^k}y)^nz \\\\ &= \lambda xz. (\lambda y. x^{n^k}y)^{n-1} x^{n^k}z \\\\ &= \lambda xz. (\lambda y. x^{n^k}y)^{n-2} x^{n^k}x^{n^k}z \\\\ &\cdots \\\\ &= \lambda xz. (x^{n^k})^nz \\\\ &= \lambda xz. x^{n^{k+1}}z \\\\ &= \ulcorner n^{k+1}\urcorner \end{align}$$

20

习题3.20

构造 $F\in\Lambda^{\circ}$，使得对于任意 $n\in\mathbb{N}$， $$ F\ulcorner n\urcorner =_{\beta} \ulcorner 2^n\urcorner. $$

解：

解法一：

易见 $F$ 对应的数论函数为：

$$\begin{cases} f(0) &=1,\\\\ f(n+1) &=2f(n). \end{cases}$$

故首先构造 $G\in\Lambda^{\circ}$，使得 $G\ulcorner n\urcorner =\ulcorner 2n\urcorner$，则 $\begin{cases}F\ulcorner 0\urcorner&=\ulcorner 1\urcorner\\ F\ulcorner n+1\urcorner&=G(F\ulcorner n\urcorner) \end{cases}$.

$$\begin{align} \ulcorner 2n\urcorner &=\lambda fx. f^{2n}x \\\\ &=\lambda fx. f^n(f^nx)\\\\ &=\lambda fx. f^n(\ulcorner n\urcorner fx) \\\\ &=\lambda fx. \ulcorner n\urcorner f(\ulcorner n\urcorner fx) \\\\ &=(\lambda afx. a f(a fx))\ulcorner n\urcorner \end{align}$$

故 $G\equiv \lambda afx. a f(a fx)$.

$$ F\ulcorner n\urcorner=G^{n}\ulcorner 1\urcorner=\ulcorner n\urcorner G\ulcorner 1\urcorner=(\lambda x. xG\ulcorner 1\urcorner)\ulcorner n\urcorner $$ 故 $F\equiv \lambda x. xG\ulcorner 1\urcorner$.

解法二：

利用习题3.19中的Exp函数，有

$$\ulcorner 2^n\urcorner= \begin{cases} \ulcorner 1\urcorner,&n=0\\\\ \text{Exp}\ulcorner 2\urcorner\ulcorner n\urcorner,&n>0 \end{cases}$$

即

$$\ulcorner 2^n\urcorner=D\ulcorner n\urcorner \ulcorner 1\urcorner (\text{Exp}\ulcorner 2\urcorner\ulcorner n\urcorner)$$

故 $F\equiv \lambda x.Dx \ulcorner 1\urcorner (\text{Exp}\ulcorner 2\urcorner x)$

21

习题3.21

设 $f,g:\mathbb{N}\rightarrow\mathbb{N}$, $f=\text{Itw}[g]$，即 $$ \begin{align} f(0)&=0,\\ f(n+1)&=g(f(n)), \end{align} $$ 且 $G\in\Lambda^{\circ}$ $\lambda$-定义函数 $g$. 试求 $F\in\Lambda^{\circ}$ 使得$F$ $\lambda$-定义函数 $f$.

解：

$$F\ulcorner n\urcorner=G^n\ulcorner 0\urcorner=\ulcorner n\urcorner G \ulcorner 0\urcorner$$

故 $F\equiv \lambda x. xG\ulcorner 0\urcorner$.

22

习题3.22

证明引理3.39：

存在一般递归函数var, app, abs, num: $\mathbb{N}\rightarrow \mathbb{N}$使得：

(1) $\forall n\in \mathbb{N}. \text{var}(n) = \sharp (v^P={(n)})$;

(2) $\forall M, N \in \Lambda. \text{app}(\sharp M, \sharp N) = \sharp (MN)$;

(3) $\forall x \in \nabla, M\in\Lambda. \text{abs}(\sharp x, \sharp M) = \sharp (\lambda x. M)$;

(4) $\forall n \in \mathbb{N}. \text{num}(n) = \sharp \ulcorner n \urcorner$.

证：

我们取 $[x,y]=2^{x}\cdot 3^y, \Pi_1=\text{ep}_0, \Pi_2=\text{ep}_1$， 从而$[\cdot, \cdot], \Pi_1, \Pi_2\in\mathcal{EF}$.

(1)

$\forall x\in\mathbb{N}$, $\text{var}(x)=[0,x]$.

故var是一般递归函数。

(2)

$\forall x,y\in\mathbb{N}$, $\text{app}(x, y)=[1, [x, y]]$.

故app是一般递归函数。

(3)

$\forall x,y\in\mathbb{N}$, $\text{abs}(x, y)=[2, [\text{var}(x), y]]$.

故abs是一般递归函数。

(4)

$\forall n\in\mathbb{N}$,

$$\begin{align} \text{num}(n+1) &=\sharp \ulcorner n+1 \urcorner \\\\ &=\sharp (\lambda fx. f^{n+1} x)\\\\ &=[2, [\sharp f, \sharp (\lambda x. f^{n+1}x)]] \\\\ &=[2, [\sharp f, [2, [\sharp x, \sharp f^{n+1}x]]]] \\\\ &=[2, [\sharp f, [2, [\sharp x, [1, [\sharp f, \sharp f^{n}x]]]]]] \end{align}$$

同理可得$\sharp \ulcorner n \urcorner = [2, [\sharp f, [2, [\sharp x, \sharp f^{n}x]]]]$.

故$\sharp f^{n}x=\Pi^4_2(\sharp \ulcorner n \urcorner)$

因此$\sharp \ulcorner n+1 \urcorner=[2, [\sharp f, [2, [\sharp x, [1, [\sharp f, \Pi^4_2(\sharp \ulcorner n \urcorner)]]]]]]$

令$h(z)=[2, [\sharp f, [2, [\sharp x, [1, [\sharp f, \Pi^4_2(z)]]]]]]$

取$x$为$v^{(0)}$, $f$为$v^{(1)}$时，$h(z)\in\mathcal{EF}$.

令

$$\begin{cases} \text{num}(0) = \sharp \ulcorner 0 \urcorner,\\\\ \text{num}(n+1) = h(\text{num}(n)). \end{cases}$$

故有$\text{num}(n)=\sharp \ulcorner n \urcorner$.

易见$\text{num}\in\mathcal{PRF}$

23

习题3.23

设 $f(n)$ 为习题1.16中定义的函数，试构造 $F\in\Lambda^{\circ}$使 $F\ulcorner n\urcorner = \ulcorner f(n)\urcorner$ 对 $n\in\mathbb{N}^+$成立.

解：

对于 $n\in\mathbb{N}^+$,

$$\begin{align} f(1) &= 1, \\\\ f(2) &= 2^2, \\\\ f(3) &= 3^{3^3}, \\\\ \cdots & \cdots \\\\ f(n) &= \underbrace{n^{\cdot^{\cdot^{\cdot^n}}}}_{n个n}, \end{align}$$

令 $g(m,n)=\underbrace{n^{\cdot^{\cdot^{\cdot^n}}}}_{m个n}$，其中 $m,n\in\mathbb{N}^+$则

$$\begin{cases} g(1,n)&=n\,,\\\\ g(m+1,n)&=n^{g(m,n)}\,. \end{cases}$$

构造 $G\ulcorner m\urcorner\ulcorner n\urcorner=\ulcorner g(m,n)\urcorner=\ulcorner \underbrace{n^{\cdot^{\cdot^{\cdot^n}}}}_{m个n}\urcorner$.

$$\begin{align} G\ulcorner m\urcorner\ulcorner n\urcorner &= \text{IF } \ulcorner m\urcorner=\ulcorner 1\urcorner \text{ THEN } \ulcorner n\urcorner \text{ ELSE } \ulcorner n^{g(m-1, n)}\urcorner\\\\ &= \text{IF } \ulcorner m\urcorner=\ulcorner 1\urcorner \text{ THEN } \ulcorner n\urcorner \text{ ELSE Exp} \ulcorner n\urcorner\ulcorner g(m-1, n)\urcorner\\\\ &= \text{IF } \ulcorner m\urcorner=\ulcorner 1\urcorner \text{ THEN } \ulcorner n\urcorner \text{ ELSE Exp} \ulcorner n\urcorner(G\ulcorner m-1\urcorner\ulcorner n\urcorner)\\\\ &= D(\text{Pred}\ulcorner m\urcorner)\ulcorner n\urcorner (\text{Exp} \ulcorner n\urcorner(G(\text{Pred}\ulcorner m\urcorner)\ulcorner n\urcorner))\\\\ &= (\lambda fxy. D(\text{Pred}x)y (\text{Exp} y(f(\text{Pred}x)y)))G\ulcorner m\urcorner\ulcorner n\urcorner\\\\ \end{align}$$

故 $G\equiv \mathbb{Y}(\lambda fxy. D(\text{Pred}x)y (\text{Exp} y(f(\text{Pred}x)y)))$.

由 $F\ulcorner n\urcorner=G\ulcorner n\urcorner\ulcorner n\urcorner$,故 $F\equiv \lambda x. Gxx$.

24

习题3.24

构造 $H\in\Lambda^{\circ}$，使得对于任意 $n\in\mathbb{N}$,$x_1,\cdots,x_n\in\Lambda$，有 $$ H\ulcorner n\urcorner x_1\cdots x_n=_{\beta} \lambda z.zx_1\cdots x_n. $$

解：

令 $M_n\equiv \lambda x_1\cdots x_nz.zx_1\cdots x_n$，易见 $g(n)=\sharp M_n$ 是递归的. 设 $G\in\Lambda^{\circ}$ $\lambda$-定义了 $g$，从而 $G\ulcorner n\urcorner =_{\beta}\ulcorner M_n \urcorner$，因此

$$E(G\ulcorner n\urcorner)=_{\beta} E\ulcorner M_n \urcorner=_{\beta}M_n.$$

取 $H\equiv \lambda x.E(Gx)$即可。

25

习题3.25

证明：存在 $\varTheta_2\in\Lambda^{\circ}$，使得对于任意 $F\in\Lambda^{\circ}$，有 $$ \varTheta_2\ulcorner F\urcorner =_{\beta} F\ulcorner \varTheta_2\ulcorner F\urcorner\urcorner. $$

证：

令 $A\equiv \lambda xy. (Ey)(\text{App}x(\text{App}(\text{Num}x)(\text{Num}y)))$，其中 App，Num在命题3.40中定义，E在定理3.41中定义。

令 $\varTheta_2\equiv A\ulcorner A\urcorner$.

则

$$\begin{align} \varTheta_2\ulcorner F\urcorner &=A\ulcorner A\urcorner\ulcorner F\urcorner \\\\ &=(\lambda xy. (Ey)(\text{App}x(\text{App}(\text{Num}x)(\text{Num}y))))\ulcorner A\urcorner\ulcorner F\urcorner \\\\ &=(E\ulcorner F\urcorner)(\text{App}\ulcorner A\urcorner(\text{App}(\text{Num}\ulcorner A\urcorner)(\text{Num}\ulcorner F\urcorner))) \\\\ &=F(\text{App}\ulcorner A\urcorner(\text{App}\ulcorner\ulcorner A\urcorner\urcorner\ulcorner\ulcorner F\urcorner\urcorner)) \\\\ &=F(\text{App}\ulcorner A\urcorner\ulcorner\ulcorner A\urcorner\ulcorner F\urcorner\urcorner) \\\\ &=F\ulcorner A\ulcorner A\urcorner\ulcorner F\urcorner\urcorner \\\\ &=F\ulcorner \varTheta_2\ulcorner F\urcorner\urcorner \end{align}$$