《计算模型导引》第三章习题
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}
\]