Types and Programming Languages习题的参考解答及思考（第5章）

第5章

章节5.2

练习5.2.1

题目：

Define logical \( \text{or} \) and \( \text{not} \) functions.

解答：

逻辑或函数：\( \text{or} = \lambda \text{b. } \lambda \text{c. } \text{b tru c} \)

逻辑非函数：\( \text{not} = \lambda \text{b. } \text{b fls tru} \)

练习5.2.2

题目：

Find another way to define the successor function on Church numerals.

注，关于Church数字的理解：

注意下Church数字中的每个数都是二元函数，针对某个Church数字，我们是通过“观察”它在接收到两个参数后的行为，来确定这个Church数字对应我们熟悉的自然数中哪个数。举个例子，Church数字中对应自然数\( 0 \)的是二元函数\( \text{c}_0 = \lambda \text{s. } \lambda \text{z. } \text{z} \)，这里\( \text{c}_0 \)的行为是：接收两个参数，并无条件返回第二个参数，由于书中使用符号\( \text{z} \)作为第二个参数，也就是zero的首字母，容易让人认为传进来的第二个参数\( \text{z} \)才是Church数字中的\( 0 \)，然而不是（或者说不一定，得看传进来的具体参数），所有有着“接收参数，并无条件返回第二个参数”行为的函数才是Church数字中的\( 0 \)，我们是通过函数行为区分Church数字的，跟第二个参数传什么没有任何关系，个人认为书中将该符号改成\( \text{b} \)表示base或者其他符号会更不容易误解，但\( \text{b} \)一般又表示Church布尔，故接下来我会用符号\( \text{o} \)作为第二个参数，也就是origin的首字母。

解答：

\( \text{scc} = \lambda \text{n. } \lambda \text{s. } \text{o. } \text{n s } (\text{s o}) \)

即给\( \text{scc} \)一个Church数字\( \text{n} \)，\( \text{scc} \)会返回一个二元函数，它具有行为：“首先用\( \text{o} \)调用一次函数\( \text{s} \)，将该结果作为\( \text{n} \)的第二个参数，让\( \text{n} \)自己再补上其对应次数调用（取决于它是Church数字几）”。令\( n_0 \)为\( \text{n} \)对应的迭代调用\( \text{s} \)的次数（即它是Church数字中对应自然数\( n_0 \)的数字），则我们得出结论，\( \text{scc} \)返回的二元函数的行为是：“以\( \text{b} \)作为初始参数，迭代调用\( \text{s} \)共\( n_0 + 1 \)次”，这个行为刚好是\( \text{n} \)后继的行为，故\( \text{scc} \)返回的二元函数是\( \text{n} \)的后继。

练习5.2.3

题目：

Is it possible to define multiplication on Church numerals without using plus?

解答：

\( \text{times} = \lambda \text{m. } \lambda \text{n. } \lambda \text{s. } \lambda \text{o. } \text{m } (\text{n s}) \text{ o} \)

\( \text{times} \)接收两个Church数字\( \text{m, n} \)并返回一个二元函数，令\( m_0, n_0 \)为\( \text{m, n} \)对应的自然数，我们分析下返回的二元函数行为：传递给\( \text{n} \)第一个参数\( \text{s} \)，我们得到一个一元函数\( \text{f} \)， \( \text{f} \)函数接收一个参数，并会用该参数作为初始参数，迭代调用\( \text{s} \)共\( n_0 \)次 (a) ，将\( \text{f, o} \)作为\( \text{m} \)的第1、2个参数， \( \text{m} \)会以\( \text{o} \)作为初始参数，迭代调用\( \text{f} \)共\( m_0 \)次，第一次调用\( \text{f o} \)，由(a)可知，会产生\( n_0 \)次对\( \text{s} \)的迭代调用，类似的，迭代两次调用，\( \text{f } (\text{f o}) \)会产生\( n_0 + n_0 \)次对\( \text{s} \)的迭代调用，由于迭代调用\( \text{f} \)共\( m_0 \)次，以此类推，最终会产生\( m_0 \times n_0 \)次对\( \text{s} \)的迭代调用，这刚好是对应自然数\( m_0 + n_0 \)的Church数字的行为，因此该返回的二元函数确实是我们要的和Church数字。

上面函数可以进一步简写成 \( \text{times} = \lambda \text{m. } \lambda \text{n. } \lambda \text{s. } \text{m } (\text{n s}) \)，针对该定义，传递两个参数\( \text{m, n} \)后，会返回一个函数\( \lambda \text{s. } \text{m } (\text{n s}) \)，这个函数和前一个定义返回的函数的行为基本相同，只不过传递\( \text{s} \)迭代调用的初始参数的手段不同，前一个定义是由返回的二元函数在接收到第二个参数后，间接传递给\( \text{m} \)的，现在这个定义是由\( \text{m} \)直接接收该参数，前一个定义要多一次参数代入的过程，但是它们行为的最终效果均是：以\( \text{s} \)后的下一个参数作为初始参数，产生对\( \text{s} \)的迭代调用共\( m_0 + n_0 \)次，且没有做额外的事情（不考虑参数代入过程的话），这是我们唯一关心的事情，故它们的行为以我们关心的角度来看是等价的，因此可以认为它们是同一个Church数字。

练习5.2.4

题目：

Define a term for raising one number to the power of another.

解答：

\( \text{power} = \lambda \text{m. } \lambda \text{n. } \text{n } (\text{times m}) \text{ } \text{c}_1 \)

令\( m_0, n_0 \)为\( \text{m, n} \)对应的自然数，迭代1次，\( \text{times m } \text{c}_1 \)得到自然数\( m_0 \)对应的Church数字，迭代2次，\( \text{times m } (\text{times m } \text{c}_1) \)得到自然数\( (m_0)^2 \)对应的Church数字，以此类推，迭代\( n_0 \)次，得到自然数\( (m_0)^{n_0} \)对应的Church数字，这刚好是我们想要的。

还有个更紧凑的定义，如下：

\( \text{power} = \lambda \text{m. } \lambda \text{n. } \text{n m} \)

这个定义第一眼看上去就很奇怪，传递两个Church数字\( \text{m, n} \)给\( \text{power} \)，得到项\( \text{n m} \)，而传递\( \text{m} \)给\( \text{n} \)返回的项直觉上都不一定是Church数字，更不用说它返回的到底是不是正确的Church数字了。

为了验证该定义的正确性，我们首先看几个简单的例子。

首先，如果该定义真的正确，那当第二个参数\( \text{n} \) 为自然数\( 0 \)对应的Church数字\( \text{c}_0 \)时，返回值\( \text{n m} \)应该是自然数1对应的Church数字\( \text{c}_1 \)，为了验证这点，我们传递两个参数\( \text{s, o} \)给返回的结果\( \text{n m} \)， \( (\text{n m}) \text{ s o} = (\text{c}_0 \text{ m}) \text{ s o} = ((\text{c}_0 \text{ m}) \text{ s}) \text{ o} = (\text{c}_0 \text{ m} \text{ s}) \text{ o} \rightarrow \text{ s} \text{ o} \)，可以看到\( \text{n} = \text{c}_0 \)时， \( \text{n m} \)针对两个传入参数的行为确实和\( \text{c}_1 \)一致，因此\( \text{n m} \)和\( \text{c}_1 \)等价，返回值是正确的。

那针对\( \text{n} = \text{c}_1 \)呢，结果是否正确？如果结果正确，那么我们是否能看出什么规律？试下， \( (\text{n m}) \text{ s o} = (\text{c}_1 \text{ m}) \text{ s o} = ((\text{c}_1 \text{ m}) \text{ s}) \text{ o} = (\text{c}_1 \text{ m} \text{ s}) \text{ o} \rightarrow (\text{m} \text{ s}) \text{ o} = \text{m s o} \)，结果是正确的。那\( \text{n} = \text{c}_2 \)呢？ \( (\text{n m}) \text{ s o} = (\text{c}_2 \text{ m}) \text{ s o} = ((\text{c}_2 \text{ m}) \text{ s}) \text{ o} = (\text{c}_2 \text{ m} \text{ s}) \text{ o} \rightarrow^* (\text{m } (\text{m} \text{ s})) \text{ o} \)，先不管这个结果是不是对的，进一步易得，一般的， \( (\text{n m}) \text{ s o} \rightarrow^* (\text{m } (\text{m } \dots (\text{m} \text{ s} \underbrace{)) \dots )}_{n_0\text{个右括号}} \text{o} \)，这里\( n_0 \)为Church数字\( \text{n} \)对应的自然数，我们想证明当\( n_0 \geq 1 \)时，\( (\text{m } (\text{m } \dots (\text{m} \text{ s} \underbrace{)) \dots )}_{n_0\text{个右括号}} \) 为函数，且该函数具有行为“接收一个参数\( \text{o} \)，最终效果是以\( \text{o} \)作为初始参数迭代调用\( \text{s} \)共\( (m_0)^{n_0} \)次（这里\( m_0 \)为Church数字\( \text{m} \)对应的自然数）”，我们对\( n_0 \)进行数学归纳，当\( n_0 = 1 \)时， \( (\text{m } (\text{m } \dots (\text{m} \text{ s} \underbrace{)) \dots )}_{n_0\text{个右括号}} = (\text{m s}) \)，确实为函数，且具有行为“接收一个参数\( \text{o} \)后，最终效果确实是以\( \text{o} \)作为初始参数迭代调用\( \text{s} \)共\( (m_0)^1 \)次”，基础情况成立，归纳假设当\( n_0 = k \)时结论成立，当\( n_0 = k + 1 \)时， \( (\text{m } (\text{m } \dots (\text{m} \text{ s} \underbrace{)) \dots )}_{k + 1\text{个右括号}} = (\text{m } (\text{m } \dots (\text{m} \text{ s} \underbrace{)) \dots )}_{k\text{个右括号}} ) \)，这里将\( k \)个右括号的部分提取出来，即\( (\text{m } \dots (\text{m} \text{ s} \underbrace{)) \dots )}_{k\text{个右括号}} \)，根据归纳假设，\( (\text{m } \dots (\text{m} \text{ s} \underbrace{)) \dots )}_{k\text{个右括号}} \)为函数，且具有行为“接收一个参数\( \text{o} \)后，最终效果确实是以\( \text{o} \)作为初始参数迭代调用\( \text{s} \)共\( (m_0)^k \)次”，令\( (\text{m } \dots (\text{m} \text{ s} \underbrace{)) \dots )}_{k\text{个右括号}} \)为\( \text{f}^k \)，则\( (\text{m } (\text{m } \dots (\text{m} \text{ s} \underbrace{)) \dots )}_{k + 1\text{个右括号}} = (\text{m } (\text{m } \dots (\text{m} \text{ s} \underbrace{)) \dots )}_{k\text{个右括号}} ) = (\text{m} \text{f}^k) \)，这里\( (\text{m} \text{f}^k) \)为函数，且具有行为“接收一个参数\( \text{o} \)后，最终效果是以\( \text{o} \)作为初始参数迭代调用\( \text{f}^k \)共\( m_0 \)次”，故总迭代次数是\( (m_0)^k \times m_0 = (m_0)^{k + 1} \)次，归纳完毕，结论成立。于是，针对\( (\text{n m}) \text{ s o} \rightarrow^* (\text{m } (\text{m } \dots (\text{m} \text{ s} \underbrace{)) \dots )}_{n_0\text{个右括号}} \text{o} \)，如果\( n_0 \geq 1 \)，则最终得到的\( (\text{m } (\text{m } \dots (\text{m} \text{ s} \underbrace{)) \dots )}_{n_0\text{个右括号}} \text{o} \)的效果是以\( \text{o} \)作为初始参数迭代调用\( \text{s} \)共\( (m_0)^{n_0} \)次，是正确的，而当\( n_0 = 0 \)时，之前已经验证过结果是正确的了。综上，定义\( \text{power} = \lambda \text{m. } \lambda \text{n. } \text{n m} \)确实是正确的，证明不太严格，不过应该可以说服读者它是正确的，遗憾的是，该定义仍然很不直观，我现在仍不清楚想出该定义的人的思路是怎样的。

练习5.2.5

题目：

Use \( \text{prd} \) to define a subtraction function.

解答：

\( \text{subtract} = \lambda \text{m. } \lambda \text{n. } \text{n prd m} \)

令\( m_0, n_0 \)为\( \text{m, n} \)对应的自然数，当\( n_0 \leq m_0 \)时，结果明显是正确的，当\( n_0 > m_0 \)时，第\( m_0 + 1 \)次迭代调用\( \text{prd} \)参数会是\( \text{c}_0 \)，而\( \text{prd } \text{c}_0 = \text{c}_0 \)，之后的迭代结果会一直保持是\( \text{c}_0 \)，故当\( n_0 > m_0 \)时，\( \text{subtract m n} \)的结果会是\( \text{c}_0 \)。

练习5.2.6

题目：

Approximately how many steps of evaluation (as a function of \( \text{n} \)) are required to calculate \( \text{prd } \text{c}_n \)?

解答：

先从\( \text{c}_0 \)自增到\( \text{c}_n \)，生成共\( n + 1 \)个Church数字对，每次自增得到新的Church数字对需要一步，最后再对最后一个Church数字对进行\( \text{fst} \)操作又需要一步，故总共需要\( O(n) \)步。

练习5.2.7

题目：

Write a function equal that tests two numbers for equality and returns a Church boolean. For example,

\[ \begin{aligned} &\text{equal} \text{ } \text{c}_3 \text{ } \text{c}_3\text{;} \\ \blacktriangleright \text{ } &(\lambda \text{t. } \lambda \text{f. } \text{t}) \end{aligned} \]

\[ \begin{aligned} &\text{equal} \text{ } \text{c}_3 \text{ } \text{c}_2\text{;} \\ \blacktriangleright \text{ } &(\lambda \text{t. } \lambda \text{f. } \text{f}) \end{aligned} \]

解答：

首先读者容易想到直接\( \text{equal} = \text{iszro (subtract m n)} \)，但这个不行，根据我们练习5.2.5中的讨论，当\( \text{n} \)比\( \text{m} \)大时，结果仍然是\( \text{c}_0 \)，\( \text{iszro} \)仍然返回\( \text{tru} \)，然而两者不相等，但是进一步可以判断是否\( \text{iszro (subtract n m)} \)也为\( \text{tru} \)，于是我们得到了如下定义：

\( \text{equal} = \lambda \text{m. } \lambda \text{n. } \text{and} \text{ } (\text{iszro (subtract m n)}) \text{ } (\text{iszro (subtract n m)}) \)

练习5.2.8

题目：

A list can be represented in the lambda-calculus by its \( \text{fold} \) function. (OCaml’s name for this function is \( \text{fold\_right} \); it is also sometimes called \( \text{reduce} \).) For example, the list \( [x,y,z] \) becomes a function that takes two arguments \( \text{c} \) and \( \text{n} \) and returns \( \text{c x (c y (c z n))} \). What would the representation of \( \text{nil} \) be? Write a function \( \text{cons} \) that takes an element \( \text{h} \) and a list (that is, a fold function) \( \text{t} \) and returns a similar representation of the list formed by prepending \( \text{h} \) to \( \text{t} \). Write \( \text{isnil} \) and \( \text{head} \) functions, each taking a list parameter. Finally, write a \( \text{tail} \) function for this representation of lists (this is quite a bit harder and requires a trick analogous to the one used to define \( \text{prd} \) for numbers).

解答：

模仿下Church数字就行了，没什么难度。

\[ \begin{aligned} \text{nil} &= \lambda \text{c. } \lambda \text{n. } \text{n} \\ \text{cons} &= \lambda \text{h. } \lambda \text{t. } \lambda \text{c. } \lambda \text{n. } \text{c h (t c n)} \\ \text{isnil} &= \lambda \text{l. } \text{l } (\lambda \text{h. } \lambda \text{t. } \text{fls}) \text{ tru} \\ \text{head} &= \lambda \text{l. } \text{l } (\lambda \text{h. } \lambda \text{t. } \text{h}) \text{ nil} \end{aligned} \]

注意，这里当\( \text{l} \)为空列表时，\( \text{head} \)返回\( \text{nil} \)，选择返回其他值，比如\( \text{fls} \)等也是OK的。

最后，我们定义\( \text{tail} \)，如下：

\[ \begin{aligned} \text{nn} &= \text{pair nil nil} \\ \text{cc} &= \lambda \text{h. } \lambda \text{t. } \text{pair (snd t) (cons h (snd t))} \\ \text{tail} &= \lambda \text{l. } \text{fst (l cc nn)} \end{aligned} \]

还有一个用嵌套pair来表示列表的，pair的第一个分量记录当前列表是否为空列表，第二个分量为另外一个pair，该pair的第一个分量记录当前的头元素，第二个分量记录尾列表，如下：

\[ \begin{aligned} \text{nil} &= \text{pair tru tru} \\ \text{cons} &= \lambda \text{h. } \lambda \text{t. } \text{pair fls (pair h t)} \\ \text{isnil} &= \lambda \text{l. } \text{fst l} \\ \text{head} &= \lambda \text{l. } \text{fst (snd l)} \\ \text{tail} &= \lambda \text{l. } \text{snd (snd l)} \end{aligned} \]

类似的，如果我们有3元组，则可以用第1个分量记录当前列表是否为空列表，第2个分量记录头元素，第3个分量记录尾列表。

附注，如何一步步推导出用于定义递归函数的组合器

书上给出了用于定义递归函数的不动点组合器（fixed-point combinator），如下：

\[ \text{fix} = \lambda \text{f. } (\lambda \text{x. } \text{f } (\lambda \text{y. } \text{x x y})) \text{ } (\lambda \text{x. } \text{f } (\lambda \text{y. } \text{x x y})) \]

并且书上给出了使用\( \text{fix} \)定义阶乘函数\( \text{factorial} \)的例子以及对应求值\( \text{factorial } \text{c}_3 \)的过程，一步步看，发现其确实能实现阶乘的递归计算，但是不清楚\( \text{fix} \)这个组合器是怎么想出来的，下面，我们尝试还原这个推导过程。

为了使书写简洁点，我们这里选择使用原子布尔和原子数字，而不选择Church布尔和Chuch数字，并且判等直接用\( \text{n} = 0 \)，减法直接用\( \text{n} - 1 \)等。

正常情况下，我们会这样定义\( \text{factorial} \)：

\[ \text{factorial}(\text{n}) = \text{if } \text{n} = 0 \text{ then } 1 \text{ else } \text{n} * \text{ factorial} (\text{n} - 1) \]

这里的问题在于，在纯lambda演算系统中，是不允许像\( \text{factorial} \)这样自己引用自己的，那在像纯lambda演算系统这样不支持自己引用自己的系统中，如何定义递归函数呢？容易想到，既然不能自己引用/调用自己，那我把自己调用自己的地方改成完整拷贝一份自己的代码，然后传递参数给拷贝的这份代码不就行了，如下：

\[ \text{factorial} = \lambda \text{n. } \text{if } \text{n} = 0 \text{ then } 1 \text{ else } \text{n} * (\text{自己代码的拷贝} (\text{n} - 1)) \]

这里的问题在于如何实现拷贝一份自己的代码，毕竟不支持自引用，我们自己是看不到自己的，但是外界看得到我们，于是想到让外界帮我们拷贝自己，然后传递这份拷贝的代码给我们，这需要\( \text{factorial} \)多一个参数用于接收自己代码的拷贝，我们用符号\( \text{c} \)，也就是copy的首字母来代表该参数，如下：

\[ \text{factorial} = \lambda \text{c. } \lambda \text{n. } \text{if } \text{n} = 0 \text{ then } 1 \text{ else } \text{n} * (\text{c c } (\text{n} - 1)) \]

注意定义中的\( \text{else} \)分支的\( \text{c c } (\text{n} - 1) \)，不能改成\( \text{c } (\text{n} - 1) \)，因为\( \text{factorial} \)已经改成接收两个参数的函数了，如果\( \text{c} \)真的是\( \text{factorial} \)代码的拷贝，那它也应该接收两个参数。

那怎么调用新的定义来计算阶乘呢？很简单，给一个新的定义：

\[ \text{realfactorial} = \lambda \text{n. } \text{factorial factorial n} \]

然后我们改调用\( \text{realfactorial} \)，以计算\( 2 \)的阶乘为例，如下：

\[ \begin{aligned} &\text{realfactorial 2} = \text{factorial factorial } 2 \\ &\rightarrow \text{if } 2 = 0 \text{ then } 1 \text{ else } 2 * (\text{factorial factorial }(2 - 1)) \\ &\rightarrow 2 * (\text{factorial factorial }(2 - 1)) \\ &\rightarrow 2 * (\text{factorial factorial }1) \\ &\rightarrow 2 * (\text{if } 1 = 0 \text{ then } 1 \text{ else } 1 * (\text{factorial factorial }(1 - 1))) \\ &\rightarrow 2 * (1 * (\text{factorial factorial }(1 - 1))) \\ &\rightarrow 2 * (1 * (\text{factorial factorial }0)) \\ &\rightarrow 2 * (1 * (\text{if } 0 = 0 \text{ then } 1 \text{ else } 0 * (\text{factorial factorial }(0 - 1)))) \\ &\rightarrow 2 * (1 * 1) \\ &\rightarrow^* 2 \end{aligned} \]

上面是通过变量代入来实现代码的拷贝，具体的，\( \text{realfactorial} \) 调用\( \text{factorial} \)并传递\( \text{factorial} \)作为第一个参数，第一个参数对应的变量\( \text{c} \)在\( \text{factorial} \)函数体中出现了两次，故会拷贝两份\( \text{factorial} \)代码。

这样确实可以定义递归函数了，但是有个小瑕疵，就是定义中针对自身的调用，我们需要额外传递自身的拷贝作为第一个参数，就像\( \text{factorial} \)中的\( \text{c c } (\text{n} - 1) \)一样，理想的情况下，我们希望直接写成类似 \( \text{c } (\text{n} - 1) \)的形式，这样在概念上会更接近于“自己调用自己”，而不是“传递自己以调用自己”。为了实现能直接写成类似\( \text{c } (\text{n} - 1) \)的形式，容易想到不要让调用者直接传递我们代码的拷贝\( \text{c} \)，而改成传递一个特殊参数\( \text{c}' \)，于是调用就变成\( \text{c}' \text{ } (\text{n} - 1) \)，然后这个特殊的\( \text{c}' \)在接收到参数\( \text{n} - 1 \)后，再展开成\( \text{c c } (\text{n} - 1) \)，也就和我们原本一样了，但是等一下，这里\( \text{c} \)是我们代码的拷贝，而我们已经把第一个参数改成传递特殊参数\( \text{c}' \)，这里却仍然传递第一个参数为\( \text{c} \)，这是有问题的，应该展开成\( \text{c } \text{c}' \text{ } (\text{n} - 1) \)才对。到此，思路是有了，但是如何实现这个特殊参数\( \text{c}' \)呢？注意到\( \text{c}' \text{ } (\text{n} - 1) \)会展开成 \( \text{c } \text{c}' \text{ } (\text{n} - 1) \)，这里\( \text{c}' \)似乎在接收到参数\( \text{n} - 1 \)展开后，不仅拷贝了\( \text{c} \)，还自己拷贝了自己，也就是\( \text{c}' \)需要有自拷贝能力，那如何实现自拷贝呢？书上给出的\( \text{omega} \)就是自拷贝的一个很好的例子，如下：

\[ \text{omega} = (\lambda \text{x. } \text{x x}) \text{ } (\lambda \text{x. } \text{x x}) \]

易验证\( \text{omega} \)在完成一次对\( \lambda \text{x. } \text{x x} \)调用后，得到的仍是\( \text{omega} \)，它实现了自我拷贝，我们希望借由\( \text{omega} \)，想到实现\( \text{c}' \)自我拷贝的思路。

注意到这里\( \text{x x} \)似乎是被拷贝的部分，那我们把要拷贝的代码\( \text{c} \)也放在这部分会怎样？比如放在\( \text{x x} \)的前面或者后面，\( \text{c} \)也会跟着被拷贝吗？试试把\( \text{c} \)放在\( \text{x x} \)的前面，于是得到：

\[ (\lambda \text{x. } \text{c (x x)}) \text{ } (\lambda \text{x. } \text{c (x x)}) \]

展开一次调用，得到：

\[ \text{c } ((\lambda \text{x. } \text{c (x x)}) \text{ } (\lambda \text{x. } \text{c (x x)})) \]

确实得到了\( \text{c} \)的一份拷贝，而且继续展开调用还能继续得到\( \text{c} \)的拷贝，展开几次得到几份拷贝，这点请读者自行验证。我们称函数\( \lambda \text{x. } \text{c (x x)} \)的函数体\( \text{c (x x)} \)为 拷贝模板 ，拷贝模板是可以按需改变的。这里如果把\( \text{c}' \)看成 \( (\lambda \text{x. } \text{c (x x)}) \text{ } (\lambda \text{x. } \text{c (x x)}) \)的话，则\( \text{c}' \rightarrow \text{c} \text{c}' \)，也就是它拷贝了一份\( \text{c} \)，还自己拷贝了自己，和之前说的很像，我们称\( \text{c}' \)为 拷贝器 （注，拷贝器\( \text{c}' \)不仅会拷贝递归代码\( \text{c} \)，还会拷贝自身，容易忽略它会拷贝自身这点），把\( \text{c}' = (\lambda \text{x. } \text{c (x x)}) \text{ } (\lambda \text{x. } \text{c (x x)}) \) 代到之前的\( \text{c}' \text{ } (\text{n} - 1) \)试试，看看能不能实现我们想要的效果，然而我们会发现，\( \text{c}' \text{ } (\text{n} - 1) \)展开一次会得到如下的东西：

\[ \begin{aligned} \text{c}' \text{ } (\text{n} - 1) &\rightarrow \text{c } \text{c}' \text{ } (\text{n} - 1) \\ &= \text{c } ((\lambda \text{x. } \text{c (x x)}) \text{ } (\lambda \text{x. } \text{c (x x)})) \text{ } (\text{n} - 1) \end{aligned} \]

这里由于我们用的是call-by-value求值策略，故所有参数必须求值到范式才能执行函数调用，故上面的\( \text{c} \)要想被调用，它的两个参数必须先求值到范式才行，而这里第一个参数\( (\lambda \text{x. } \text{c (x x)}) \text{ } (\lambda \text{x. } \text{c (x x)}) \)就不是范式，得继续求值，于是有：

\[ \begin{aligned} \text{c}' \text{ } (\text{n} - 1) &\rightarrow \text{c } \text{c}' \text{ } (\text{n} - 1) \\ &= \text{c } ((\lambda \text{x. } \text{c (x x)}) \text{ } (\lambda \text{x. } \text{c (x x)})) \text{ } (\text{n} - 1) \\ &\rightarrow \text{c (c } ((\lambda \text{x. } \text{c (x x)}) \text{ } (\lambda \text{x. } \text{c (x x)})) \text{) } (\text{n} - 1) \end{aligned} \]

这里可以无限展开下去，始终轮不到\( \text{c} \)的调用（如果我们用的是full beta-reduction求值策略，即可以任意选择展开的地方的话，那就有其他选择可以避免无限展开的情况），那如何避免这个无限展开的情况呢？注意到上面在\( \text{c}' \text{ } (\text{n} - 1) \)展开一次后，得到\( \text{c } ((\lambda \text{x. } \text{c (x x)}) \text{ } (\lambda \text{x. } \text{c (x x)})) \text{ } (\text{n} - 1) \)，我们希望把中间的拷贝器\( \text{c}' = (\lambda \text{x. } \text{c (x x)}) \text{ } (\lambda \text{x. } \text{c (x x)}) \) 保护在\( \lambda \)-抽象里面，变成范式，然后再在我们需要拷贝时，传递参数给保护性的\( \lambda \)-抽象，按需触发拷贝，问题在于该传递什么参数？先传一个没用的参数试试（即参数仅用于触发拷贝，在函数体中不使用该参数），注意到中间的拷贝器\( \text{c}' = (\lambda \text{x. } \text{c (x x)}) \text{ } (\lambda \text{x. } \text{c (x x)}) \) 是由拷贝模板\( \text{c (x x)} \)中的\( \text{x x} \)拷贝而来的，故我们修改拷贝模板，把\( \text{x x} \)包裹在\( \lambda \)-抽象中，于是我们得到了如下的新定义：

\[ \text{c}' = (\lambda \text{x. } \text{c } (\lambda \text{t. } \text{x x})) \text{ } (\lambda \text{x. } \text{c } (\lambda \text{t. } \text{x x})) \]

再次把新拷贝器\( \text{c}' \)的定义代入到\( \text{c}' \text{ } (\text{n} - 1) \)试试，如下：

\[ \begin{aligned} \text{c}' \text{ } (\text{n} - 1) &= ((\lambda \text{x. } \text{c } (\lambda \text{t. } \text{x x})) \text{ } (\lambda \text{x. } \text{c } (\lambda \text{t. } \text{x x}))) \text{ } (\text{n} - 1) \\ &\rightarrow (\text{c } (\lambda \text{t. } (\lambda \text{x. } \text{c } (\lambda \text{t. } \text{x x})) \text{ } (\lambda \text{x. } \text{c } (\lambda \text{t. } \text{x x})))) \text{ } (\text{n} - 1) \\ &= (\text{c } (\lambda \text{t. } \text{c}')) \text{ } (\text{n} - 1) \\ &= \text{c } (\lambda \text{t. } \text{c}') \text{ } (\text{n} - 1) \end{aligned} \]

可以看到，展开后拷贝器\( \text{c}' \)就被保护在\( \lambda \)-抽象中了，这个\( \lambda \)-抽象会作为我们被拷贝的递归函数代码\( \text{c} \)的第一个参数，供\( \text{c} \)按需得到它自己的拷贝，而在下一次递归调用中，需要随便传递一个参数给该\( \lambda \)-抽象\( \lambda \text{t. } \text{c}' \)以触发拷贝，既然可以随便传参数，那我们就传递\( \text{tru} \)。

我们参数化下\( \text{c}' \)拷贝的函数体\( \text{c} \)，从而允许它用于其他递归函数的定义，如下：

\[ \text{call\_with\_copier}' = \lambda \text{c. } (\lambda \text{x. } \text{c } (\lambda \text{t. } \text{x x})) \text{ } (\lambda \text{x. } \text{c } (\lambda \text{t. } \text{x x})) \]

我们用这个新的\( \text{call\_with\_copier}' \)重新演示一遍如何定义递归函数\( \text{factorial} \)：

\[ \begin{aligned} \text{factorial}' &= \lambda \text{c. } \lambda \text{n. } \text{if } \text{n} = 0 \text{ then } 1 \text{ else } \text{n} * (\text{c tru } (\text{n} - 1)) \\ \text{factorial} &= \lambda \text{n. } (\text{call\_with\_copier}' \text{ } \text{factorial}') \text{ n} = \text{call\_with\_copier}' \text{ } \text{factorial}' \end{aligned} \]

注意到，原本的\( \text{c c } (\text{n} - 1) \)变成了\( \text{c } \text{tru } (\text{n} - 1) \)，这是因为我们接收的第一个参数\( \text{c} \)不再是自身代码的拷贝，而是一个保护拷贝器\( \text{c}' \)的\( \lambda \)-抽象，需要随便传递一个参数给这个\( \lambda \)-抽象，才能得到其保护的拷贝器\( \text{c}' \)，拷贝器\( \text{c}' \)进一步展开，得到我们自身代码的拷贝以及一个新的、被保护在\( \lambda \)-抽象中的拷贝器，具体的，传递\( \text{tru} \)给保护拷贝器的\( \lambda \)-抽象\( \text{c} \)， \( \text{c tru} \)便会展开成\( \text{c} \)保护的拷贝器\( \text{c}' \)， \( \text{c}' \)进一步展开成 \( \text{我们代码的拷贝 } (\lambda \text{t. } \text{c}') \)，注意到拷贝器\( \text{c}' \)不仅拷贝了我们的代码，还拷贝了自身并将其保护在\( \lambda \)-抽象中，故下一次递归调用也能拿到受\( \lambda \)-抽象保护的拷贝器。

我们调用新的\( \text{factorial} \)定义看看：

\[ \begin{aligned} \text{factorial 2} &= (\text{call\_with\_copier}' \text{ } \text{factorial}') \text{ } 2 \\ &\rightarrow ((\lambda \text{x. } \text{factorial}' \text{ } (\lambda \text{t. } \text{x x})) \text{ } (\lambda \text{x. } \text{factorial}' \text{ } (\lambda \text{t. } \text{x x}))) \text{ } 2 \end{aligned} \]

令\( \text{c}' = (\lambda \text{x. } \text{factorial}' \text{ } (\lambda \text{t. } \text{x x})) \text{ } (\lambda \text{x. } \text{factorial}' \text{ } (\lambda \text{t. } \text{x x})) \)，则接着上面进一步往下推：

\[ \begin{aligned} &((\lambda \text{x. } \text{factorial}' \text{ } (\lambda \text{t. } \text{x x})) \text{ } (\lambda \text{x. } \text{factorial}' \text{ } (\lambda \text{t. } \text{x x}))) \text{ } 2 \\ &= \text{c}' \text{ } 2 \\ &\rightarrow \text{factorial}' \text{ } (\lambda \text{t. } \text{c}') \text{ } 2 \\ &\rightarrow \text{if } 2 = 0 \text{ then } 1 \text{ else } 2 * ((\lambda \text{t. } \text{c}') \text{ tru } (2 - 1)) \\ &\rightarrow 2 * ((\lambda \text{t. } \text{c}') \text{ tru } (2 - 1)) \\ &\rightarrow 2 * (\text{c}' \text{ } (2 - 1)) \\ &\rightarrow 2 * (\text{factorial}' \text{ } (\lambda \text{t. } \text{c}') \text{ } (2 - 1)) \\ &\rightarrow 2 * (\text{factorial}' \text{ } (\lambda \text{t. } \text{c}') \text{ } 1) \\ &\rightarrow 2 * (\text{if } 1 = 0 \text{ then } 1 \text{ else } 1 * ((\lambda \text{t. } \text{c}') \text{ tru } (1 - 1))) \\ &\rightarrow 2 * (1 * ((\lambda \text{t. } \text{c}') \text{ tru } (1 - 1))) \\ &\rightarrow 2 * (1 * (\text{c}' \text{ } (1 - 1))) \\ &\rightarrow 2 * (1 * (\text{factorial}' \text{ } (\lambda \text{t. } \text{c}') \text{ } (1 - 1))) \\ &\rightarrow 2 * (1 * (\text{factorial}' \text{ } (\lambda \text{t. } \text{c}') \text{ } 0)) \\ &\rightarrow 2 * (1 * (\text{if } 0 = 0 \text{ then } 1 \text{ else } 0 * ((\lambda \text{t. } \text{c}') \text{ tru } (0 - 1)))) \\ &\rightarrow 2 * (1 * 1) \\ &\rightarrow^* 2 \end{aligned} \]

可以看到，新实现是可以用于定义递归函数的，但是新实现还是有瑕疵，就是我们得刻意随便传递一个参数（比如\( \text{tru} \)）以触发拷贝，能不能省略掉这个步骤？考虑到我们在语法上限制了每个\( \lambda \)-抽象必须有一个参数，特别的，我们的递归函数在递归调用自己时，也必会传递参数给自身，比如我们上面的例子中会传递参数\( \text{n} - 1 \)给自身，可以用该必要参数作为拷贝的触发器，我们就不用额外刻意传递无用的参数以触发拷贝了，于是我们得到了如下\( \text{c}' \)的新定义：

\[ \text{c}' = (\lambda \text{x. } \text{c } (\lambda \text{y. } \text{(x x) y})) \text{ } (\lambda \text{x. } \text{c } (\lambda \text{y. } \text{(x x) y})) \]

注意，这里触发拷贝的参数\( \text{y} \)是被拷贝的递归函数代码\( \text{c} \)的实际参数（也就是上面例子中的\( \text{n} - 1 \)），故我们在拷贝模板\( \text{c } (\lambda \text{y. } \text{(x x) y}) \)中把\( \text{y} \)放在\( \text{x x} \)后面，下次递归调用传递递归函数实际参数以触发拷贝后，\( \text{x x} \)会对应拷贝出新的拷贝器\( \text{c}' \)，而形参\( \text{y} \)对应的实参则会在这新的拷贝器\( \text{c}' \)后面，新的\( \text{c}' \)进一步展开成 \( \text{c } (\lambda \text{y. } \text{c}') \text{ 递归函数实际参数} \)，刚好，被拷贝的递归函数代码\( \text{c} \)第一个参数接收被\( \lambda \)-抽象保护的拷贝器，第二个参数接收递归函数的实际参数。说的有点绕，我们看个实际的例子，再次把新的\( \text{c}' \)的定义代入到\( \text{c}' \text{ } (\text{n} - 1) \)，结果如下：

\[ \begin{aligned} \text{c}' \text{ } (\text{n} - 1) &= ((\lambda \text{x. } \text{c } (\lambda \text{y. } \text{(x x) y})) \text{ } (\lambda \text{x. } \text{c } (\lambda \text{y. } \text{(x x) y}))) \text{ } (\text{n} - 1) \\ &\rightarrow (\text{c } (\lambda \text{y. } ((\lambda \text{x. } \text{c } (\lambda \text{y. } \text{(x x) y})) \text{ } (\lambda \text{x. } \text{c } (\lambda \text{y. } \text{(x x) y}))) \text{ y})) \text{ } (\text{n} - 1) \\ &= (\text{c } (\lambda \text{y. } \text{c}' \text{ y})) \text{ } (\text{n} - 1) \\ &= \text{c } (\lambda \text{y. } \text{c}' \text{ y}) \text{ } (\text{n} - 1) \end{aligned} \]

可以看到，展开后拷贝器\( \text{c}' \)和之前一样被保护在\( \lambda \)-抽象中，不过触发拷贝参数不再是刻意传递的无用参数，而是递归函数的实际参数，保护拷贝器的\( \lambda \)-抽象会作为我们被拷贝的递归函数代码\( \text{c} \)的第一个参数，供\( \text{c} \)按需得到它自己的拷贝，而在下一次递归调用中，该\( \lambda \)-抽象，也就是\( \lambda \text{y. } \text{c}' \text{ y} \)，会被传递下一次递归调用的实际参数\( \text{n} - 2 \)，展开成\( \text{c}' \text{ } (\text{n} - 2) \)，情况就和我们展开\( \text{c}' \text{ } (\text{n} - 1) \)类似了，以此类推（注，既然递归调用自身的第一个实际参数（比如上面的\( \text{n} - 1, \text{n} - 2 \)）会被用于触发拷贝过程，那如果定义的递归函数无参数呢？或者有不止一个参数呢？这个问题我们之后再讨论，虽然目前我们语法上禁止\( \lambda \)-抽象没有参数，不过这个讨论还是有意义的）。

类似前面，我们参数化下\( \text{c}' \)拷贝的函数体\( \text{c} \)，从而允许它用于其他递归函数的定义，如下：

\[ \text{call\_with\_copier} = \lambda \text{c. } (\lambda \text{x. } \text{f } (\lambda \text{y. } \text{(x x) y})) \text{ } (\lambda \text{x. } \text{c } (\lambda \text{y. } \text{(x x) y})) \]

最后，我们用这个新的\( \text{call\_with\_copier} \)再演示一遍如何定义递归函数\( \text{factorial} \)：

\[ \begin{aligned} \text{factorial}' &= \lambda \text{c. } \lambda \text{n. } \text{if } \text{n} = 0 \text{ then } 1 \text{ else } \text{n} * (\text{c } (\text{n} - 1)) \\ \text{factorial} &= \lambda \text{n. } (\text{call\_with\_copier } \text{factorial}') \text{ n} = \text{call\_with\_copier } \text{factorial}' \end{aligned} \]

我们调用新的\( \text{factorial} \)定义看看：

\[ \begin{aligned} \text{factorial 2} &= (\text{call\_with\_copier} \text{ } \text{factorial}') \text{ } 2 \\ &\rightarrow ((\lambda \text{x. } \text{factorial}' \text{ } (\lambda \text{y. } \text{(x x) y})) \text{ } (\lambda \text{x. } \text{factorial}' \text{ } (\lambda \text{y. } \text{(x x) y}))) \text{ } 2 \end{aligned} \]

令\( \text{c}' = (\lambda \text{x. } \text{factorial}' \text{ } (\lambda \text{y. } \text{(x x) y})) \text{ } (\lambda \text{x. } \text{factorial}' \text{ } (\lambda \text{y. } \text{(x x) y})) \)，则接着上面进一步往下推：

\[ \begin{aligned} &((\lambda \text{x. } \text{factorial}' \text{ } (\lambda \text{y. } \text{(x x) y})) \text{ } (\lambda \text{x. } \text{factorial}' \text{ } (\lambda \text{y. } \text{(x x) y}))) \text{ } 2 \\ &= \text{c}' \text{ } 2 \\ &\rightarrow \text{factorial}' \text{ } (\lambda \text{y. } \text{c}' \text{ y}) \text{ } 2 \\ &\rightarrow \text{if } 2 = 0 \text{ then } 1 \text{ else } 2 * ((\lambda \text{y. } \text{c}' \text{ y}) \text{ } (2 - 1)) \\ &\rightarrow 2 * ((\lambda \text{y. } \text{c}' \text{ y}) \text{ } (2 - 1)) \\ &\rightarrow 2 * ((\lambda \text{y. } \text{c}' \text{ y}) \text{ } 1) \\ &\rightarrow 2 * (\text{c}' \text{ } 1) \\ &\rightarrow 2 * (\text{factorial}' \text{ } (\lambda \text{y. } \text{c}' \text{ y}) \text{ } 1) \\ &\rightarrow 2 * (\text{if } 1 = 0 \text{ then } 1 \text{ else } 1 * ((\lambda \text{y. } \text{c}' \text{ y}) \text{ } (1 - 1))) \\ &\rightarrow 2 * (1 * ((\lambda \text{y. } \text{c}' \text{ y}) \text{ } (1 - 1))) \\ &\rightarrow 2 * (1 * ((\lambda \text{y. } \text{c}' \text{ y}) \text{ } 0)) \\ &\rightarrow 2 * (1 * (\text{c}' \text{ } 0)) \\ &\rightarrow 2 * (1 * (\text{factorial}' \text{ } (\lambda \text{y. } \text{c}' \text{ y}) \text{ } 0)) \\ &\rightarrow 2 * (1 * (\text{if } 0 = 0 \text{ then } 1 \text{ else } 0 * ((\lambda \text{y. } \text{c}' \text{ y}) \text{ } (0 - 1)))) \\ &\rightarrow 2 * (1 * 1) \\ &\rightarrow^* 2 \end{aligned} \]

可以看到，这个改进后的新实现也是可以用于定义递归函数的。

这里\( \text{call\_with\_copier} \)就是书上定义的\( \text{fix} \)了。

以上就是\( \text{fix} \)定义的推导过程。

那回去讨论之前抛出的问题：递归调用自身的第一个实际参数（比如上面的\( \text{n} - 1, \text{n} - 2 \)）会被用于触发拷贝过程，那如果定义的递归函数无参数呢？或者有不止一个参数呢？

先讨论定义的递归函数无参数的情况，虽然目前我们语法上禁止\( \lambda \)-抽象没有参数，不过考虑到我们的\( \lambda \)-演算系统目前是没有副作用的，因此函数的行为完全由参数决定的，如果没有参数，则函数每次被调用（包括递归调用）会执行完全一样的动作，此时分两种情况：

1. 函数不会调用自身，比如递归调用在\( \text{if} \)语句的\( \text{else} \)中，而我们始终执行\( \text{then} \)分支，这种函数本质上非递归函数，可以改写成没有递归的函数。
2. 函数会调用自身，这种递归函数每次最终都会调用自身，故函数会一直递归，始终不会停止，加上我们的\( \lambda \)-演算系统没有副作用，故该函数的调用对外完全没有可见的行为/效果（我们始终等不到返回值，也没有副作用可以看到其他效果），可以直接将这种函数替换成无限循环的\( \text{omega} \)。

接着讨论定义的递归函数有不止一个参数的情况，这里的问题在于触发拷贝只用了递归调用自身的第一个实际参数，其他参数似乎被“不平等对待”了，直觉上可能会出问题，我们尝试定义一个假想的双参数递归函数，看看会不会出问题，它的定义大概会长这样：

\[ \text{twoarg} = \lambda \text{c. } \lambda \text{x. } \lambda \text{y. } \text{if 基础情况 then 基础值 else } \text{c } \text{x}' \text{ } \text{y}' \]

这里重点关注下一次递归调用\( \text{c } \text{x}' \text{ } \text{y}' \)，这里\( \text{c } \text{x}' \)触发了拷贝，变成\( \text{自身代码的拷贝 c } \text{x}' \)，完整就是\( \text{自身代码的拷贝 c } \text{x}' \text{ } \text{y}' \)，可以看到，递归调用的第二个参数\( \text{y}' \)正确地传递给了自身代码的拷贝作为第二个参数（不考虑第一个拷贝器参数的话，\( \text{y}' \)就是第二个参数，否则就是第三个参数），以此类推，易得即使定义的递归函数有2个以上的参数也没问题。

练习5.2.9

题目：

Why did we use a primitive \( \text{if} \) in the definition of \( \text{g} \), instead of the Church-boolean \( \text{test} \) function on Church booleans? Show how to define the \( \text{factorial} \) function in terms of \( \text{test} \) rather than \( \text{if} \).

解答：

为什么在\( \text{g} \)的定义中用了原子\( \text{if} \)而没有使用\( \text{test} \)：

如果改用\( \text{test} \)，则\( \text{g} = \lambda \text{fct. } \lambda \text{n. } \text{test } (\text{equal } \text{n } \text{c}_0) \text{ } \text{c}_1 \text{ } (\text{times n } (\text{fct } (\text{prd n}))) \)，由于\( \text{test} \)为函数，因此在调用\( \text{test} \)函数之前，会先将它的三个参数均求值成范式，而不像原子\( \text{if} \)具有根据条件的真假选择性求值某个分支的能力，故不管条件真假，假分支的代码\( \text{fct } (\text{prd n}) \)始终会被求值，这里求值又会得到一个\( \text{test} \)语句，同理，针对该新得到的\( \text{test} \)语句，它的三个参数又都必须求值成范式，才能求值该新\( \text{test} \)语句，这整个过程可以不断进行，停不下来，这是我们选择用原子\( \text{if} \)的原因。

用\( \text{test} \)定义\( \text{factorial} \)：

上面说了\( \text{test} \)不像原子\( \text{if} \)具有选择性求值的能力，这导致了整个计算过程可以不断进行，得不到范式，发散，为了避免这点，我们可以把参数包裹在\( \lambda \)-抽象里以避免参数被无条件求值，这意味着\( \text{g} \)返回的不再是Church数字，而是被\( \lambda \)-抽象保护的Church数字，得传递参数给这个\( \lambda \)-抽象，才能得到其保护的Church数字，传递什么参数可以随便选，我们这里选择用\( \text{tru} \)，故包裹函数\( \text{factorial} \)在调用\( \text{g} \)得到被\( \lambda \)-抽象保护的Church数字后，需要进一步传递参数\( \text{tru} \)给这个\( \lambda \)-抽象，得到最终的Church数字，定义如下：

\[ \begin{aligned} \text{g} &= \lambda \text{fct. } \lambda \text{n. } \text{test } (\text{iszro n}) \text{ } (\lambda \text{t. } \text{c}_1) \text{ } (\lambda \text{t. } (\text{times n } (\text{fct } (\text{prd n}) \text{ tru}))) \\ \text{factorial} &= \lambda \text{n. } \text{fix g n tru} \end{aligned} \]

上面写法中，包裹函数\( \text{factorial} \)调用\( \text{g} \)得到是 \( \lambda \)-抽象保护的Church数字，因此它需要通过传递\( \text{tru} \)来得到最终结果，另一种写法就是在\( \text{g} \)返回之前先传递 \( \text{tru} \)将\( \lambda \)-抽象转换成Church数字后再返回，这样 \( \text{factorial} \)就不用转换了，如下：

\[ \begin{aligned} \text{g} &= \lambda \text{fct. } \lambda \text{n. } (\text{test } (\text{iszro n}) \text{ } (\lambda \text{t. } \text{c}_1) \text{ } (\lambda \text{t. } (\text{times n } (\text{fct } (\text{prd n}))))) \text{ tru} \\ \text{factorial} &= \lambda \text{n. } \text{fix g n} = \text{fix g} \end{aligned} \]

练习5.2.10

题目：

Define a function \( \text{churchnat} \) that converts a primitive natural number into the corresponding Church numeral.

解答：

用递归来进行转换，刚好我们又有\( \text{fix} \)以定义递归函数，比较简单，这里为了避免练习5.2.9的问题，还是使用原子\( \text{if} \)，如下：

\[ \begin{aligned} \text{g} &= \lambda \text{f. } \lambda \text{n. } \text{if iszero n then } \text{c}_0 \text{ else } \text{scc (f (pred n))} \\ \text{churchnat} &= \text{fix g} \end{aligned} \]

练习5.2.11

题目：

Use \( \text{fix} \) and the encoding of lists from Exercise 5.2.8 to write a function that sums lists of Church numerals.

解答：

练习5.2.8中我们给出两种列表的实现，这里我们只讨论第一种列表实现。

递归实现方法如下：

\[ \begin{aligned} \text{g} &= \lambda \text{f. } \lambda \text{l. } \text{if isnil \text{l} then } \text{c}_0 \text{ else } \text{plus (head \text{l}) (f (tail \text{l}))} \\ \text{sumlist} &= \text{fix g} \end{aligned} \]

注意到列表是个函数，它的第一个参数\( \text{c} \)会不断接收当前列表头元素\( \text{h} \)以及上一次\( \text{c} \)调用的返回值，我们可以利用这点来实现\( \text{sumlist} \)而不需要用到递归，如下：

\[ \text{sumlist} = \lambda \text{l. } \text{l } (\lambda \text{h. } \lambda \text{t. } \text{plus h t}) \text{ } \text{c}_0 = \lambda \text{l. } \text{l plus } \text{c}_0 \]

章节5.3

练习5.3.3

题目：

Give a careful proof that \( |FV(\text{t})| \leq \mathit{size}(\text{t}) \) for every term \( \text{t} \).

\( \forall \)项\( \text{t} \)，使用结构归纳法证明，归纳假设命题对所有\( \text{t} \)的直接子项成立，我们要证明命题对\( \text{t} \)成立，对\( \text{t} \)的形式进行分情况讨论：

1. 如果\( \text{t} \in \mathcal{V} \)，即\( \text{t} \)为变量，则\( FV(\text{t}) = \{ \text{t} \}, \mathit{size}(\text{t}) = 1 \)，满足\( |FV(\text{t})| \leq \mathit{size}(\text{t}) \)。
2. 如果\( \text{t} = \lambda \text{x. } \text{t}_1 \)，则\( FV(\text{t}) = FV(\text{t}_1) \setminus \{ \text{x} \} \)，可得\( |FV(\text{t})| \leq |FV(\text{t}_1)| \)，这里\( \text{t}_1 \)为\( \text{t} \)的直接子项，可以使用归纳假设，根据归纳假设，可得\( |FV(\text{t}_1)| \leq \mathit{size}(\text{t}_1) \)，进而可得\( |FV(\text{t})| < |FV(\text{t}_1)| + 1 \leq \mathit{size}(\text{t}_1) + 1 = \mathit{size}(\text{t}) \)。
3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则\( FV(\text{t}) = FV(\text{t}_1) \cup FV(\text{t}_2) \)，可得\( |FV(\text{t})| = |FV(\text{t}_1) \cup FV(\text{t}_2)| \leq |FV(\text{t}_1)| + |FV(\text{t}_2)| \)，这里\( \text{t}_1, \text{t}_2 \)均为\( \text{t} \)的直接子项，可以使用归纳假设，根据归纳假设，可得\( |FV(\text{t}_1)| \leq \mathit{size}(\text{t}_1) \)， \( |FV(\text{t}_2)| \leq \mathit{size}(\text{t}_2) \)，进而可得\( |FV(\text{t})| < |FV(\text{t}_1)| + |FV(\text{t}_2)| + 1 \leq \mathit{size}(\text{t}_1) + \mathit{size}(\text{t}_2) + 1 = \mathit{size}(\text{t}) \)。

归纳完毕，命题对所有项均成立。

练习5.3.6

题目：

Adapt these rules to describe the other three strategies for evaluation—full beta-reduction, normal-order, and lazy evaluation.

解答：

修改求值规则以适应full beta-reduction求值策略：

由于full beta-reduction可以选择任意位置的redex，因此不需要像E-APP2这样限制必须把函数位置的项求值成值后，才去求值参数位置的项，同理，也不需要像E-APPABS这样限制参数位置的项为值，故我们修改下规则E-APP2，E-APPABS，最终所有规则如下：

\[ \begin{aligned} \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{\text{t}_1 \text{ } \text{t}_2 \rightarrow \text{t}'_1 \text{ } \text{t}_2} &\qquad (\text{E-APP1}) \\ \dfrac{\text{t}_2 \rightarrow \text{t}'_2}{\text{t}_1 \text{ } \text{t}_2 \rightarrow \text{t}_1 \text{ } \text{t}'_2} &\qquad (\text{E-NEW-APP2}) \\ (\lambda \text{x. } \text{t}_{11}) \text{ } \text{t}_2 \rightarrow [\text{x} \mapsto \text{t}_2]\text{t}_{11} &\qquad (\text{E-NEW-APPABS}) \end{aligned} \]

修改求值规则以适应normal-order求值策略：

我们删除所有现有的规则，分情况讨论不同形式下的项该如何求值以满足normal-order求值策略，并添加对应的规则。由于之后我们可以使用大小归纳法来证明使用我们的规则进行求值是满足normal-order 求值策略的约束的，因此我们在添加新规则的过程中，针对大小比较小的项的求值关系，可以使用归纳假设，举个例子：如果我们有添加规则\( \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{ \lambda \text{x. } \text{t}_1 \rightarrow \lambda \text{x. } \text{t}'_1} \)，则我们在脑中可以想象，我们要证明一个形如\( \lambda \text{x. } \text{t}_1 \)的项在我们的规则下进行求值满足normal-order求值策略的约束，而且适用形如\( \lambda \text{x. } \text{t}_1 \)规则的只有\( \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{ \lambda \text{x. } \text{t}_1 \rightarrow \lambda \text{x. } \text{t}'_1} \)，则由于\( \text{t}_1 \)的大小比\( \lambda \text{x. } \text{t}_1 \)小，可以使用归纳假设，根据归纳假设，求值关系\( \text{t}_1 \rightarrow \text{t}'_1 \) 符合normal-order求值策略的约束，又\( \lambda \text{x. } \text{t}_1 \)最左边、最外层只有一个\( \lambda \)-抽象，即\( \lambda \text{x. } \text{t}_1 \)本身，最左边、最外层只有一个函数，没有对应的参数，故在最左边、最外层无法进行求值，能进行求值的只有函数体\( \text{t}_1 \)了，又根据归纳假设，求值关系\( \text{t}_1 \rightarrow \text{t}'_1 \)符合normal-order求值策略的约束，因此求值关系\( \lambda \text{x. } \text{t}_1 \rightarrow \lambda \text{x. } \text{t}'_1 \)也符合normal-order求值策略。OK，思路讲到这里，下面，我们开始分不同形式的情况进行讨论。

给定项\( \text{t} \)，对\( \text{t} \)的形式进行分情况讨论：

1. 如果\( \text{t} \)无法被拆成\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)的形式，则根据语法，我们知道\( \text{t} \)要么是变量，要么是\( \lambda \)-抽象，我们分情况讨论：
   1. 如果\( \text{t} = \text{x} \)为变量，则这种情况没有redex，无法求值，不需要考虑在我们的规则下进行求值是否满足normal-order求值策略的约束。
   2. 如果\( \text{t} = \lambda \text{x. } \text{t}_1 \)，则此时\( \text{t} \)的最左边、最外层只有一个\( \lambda \)-抽象，没有参数，故在最左边、最外层无法进行求值，假设\( \text{t} \)在我们的规则下能求值成\( \text{t}' \)，唯一的可能就是函数体\( \text{t}_1 \)能求值到某个\( \text{t}'_1 \)，即\( \text{t}_1 \rightarrow \text{t}'_1 \)，此时\( \text{t} = \lambda \text{x. } \text{t}_1 \rightarrow \lambda \text{x. } \text{t}'_1 = \text{t}' \)，由于\( \text{t}_1 \)的大小比\( \text{t} \)小，可以使用归纳假设（ 注： 严格来讲，不一定能使用大小归纳法进行证明，不过我们现在仅处于规则设计阶段，我们可以想象我们能使用大小归纳法，之后设计完规则再验证是否真的行得通就行了），根据归纳假设，求值关系\( \text{t}_1 \rightarrow \text{t}'_1 \)满足normal-order求值策略的约束，进而如果我们添加新规则\( \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{ \lambda \text{x. } \text{t}_1 \rightarrow \lambda \text{x. } \text{t}'_1} \)，以允许\( \text{t} = \lambda \text{x. } \text{t}_1 \)在这种情况下求值成\( \text{t}' = \lambda \text{x. } \text{t}'_1 \)，则由于\( \text{t} = \lambda \text{x. } \text{t}_1 \)最左边、最外层的redex和\( \text{t}_1 \)最左边、最外层的redex是一样的，因此求值关系\( \text{t} = \lambda \text{x. } \text{t}_1 \rightarrow \lambda \text{x. } \text{t}'_1 = \text{t}' \) 也是满足normal-order求值策略的约束的，综上，我们添加新规则： \[ \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{ \lambda \text{x. } \text{t}_1 \rightarrow \lambda \text{x. } \text{t}'_1} \qquad (\text{E-ABS}) \]
2. 如果\( \text{t} \)能被拆成\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)的形式，分情况讨论：
   1. 如果\( \text{t}_1 \)是个\( \lambda \)-抽象，即\( \text{t} = (\lambda \text{x. } \text{t}_{11}) \text{ } \text{t}_2 \)，则此时最左边、最外层的redex就是\( \text{t} \)本身，故这种情况下直接\( \text{t} = (\lambda \text{x. } \text{t}_{11}) \text{ } \text{t}_2 \rightarrow [\text{x} \mapsto \text{t}_2]\text{t}_{11} \)就完事了，故添加新规则： \[ (\lambda \text{x. } \text{t}_{11}) \text{ } \text{t}_2 \rightarrow [\text{x} \mapsto \text{t}_2]\text{t}_{11} \qquad (\text{E-APPABS}) \]
   2. 如果\( \text{t}_1 \)不是个\( \lambda \)-抽象，则此时要对\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)进行求值，首先要考虑的就是什么时候能对左侧部分\( \text{t}_1 \)进行求值，什么时候能对右侧部分\( \text{t}_2 \)进行求值，分情况讨论：

      1. 如果要对左侧部分\( \text{t}_1 \)进行求值，则直觉上可以添加规则\( \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{ \text{t}_1 \text{ } \text{t}_2 \rightarrow \text{t}'_1 \text{ } \text{t}_2} \)，类似前面，使用归纳假设，得到求值关系\( \text{t}_1 \rightarrow \text{t}'_1 \)满足normal-order求值策略的约束，然后尝试进一步推出求值关系\( \text{t}_1 \text{ } \text{t}_2 \rightarrow \text{t}'_1 \text{ } \text{t}_2 \) 满足normal-order求值策略的约束，但是问题在于推不出来，举个简单的反例，如果\( \text{t}_1 \)是个\( \lambda \)-抽象，即\( \text{t}_1 = \lambda \text{x. } \text{t}_{11} \)，假设此时能使用前面新增的规则E-ABS得到\( \text{t}_1 = \lambda \text{x. } \text{t}_{11} \rightarrow \lambda \text{x. } \text{t}'_{11} = \text{t}'_1 \)，则进一步使用规则\( \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{ \text{t}_1 \text{ } \text{t}_2 \rightarrow \text{t}'_1 \text{ } \text{t}_2} \)，能得到\( \text{t} = \text{t}_1 \text{ } \text{t}_2 = (\lambda \text{x. } \text{t}_{11}) \text{ } \text{t}_2 \rightarrow (\lambda \text{x. } \text{t}'_{11}) \text{ } \text{t}_2 = \text{t}'_1 \text{ } \text{t}_2 = \text{t}' \)，这就出问题了，最左边、最外层的redex并不在\( \text{t}_{11} \)中，而是整个\( \text{t} = (\lambda \text{x. } \text{t}_{11}) \text{ } \text{t}_2 \)，应该使用新增规则E-APPABS才对。那具体什么时候对左侧部分\( \text{t}_1 \)进行求值才是安全的呢？答案是左侧\( \text{t}_1 \)非\( \lambda \)-抽象的时候，只要\( \text{t}_1 \)非\( \lambda \)-抽象，那\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)的最左边、最外层的redex就会和\( \text{t}_1 \)的一样（注意，我们现在讨论的是要对左侧\( \text{t}_1 \)求值，即\( \text{t}_1 \)有redex的情况），进而配合归纳假设就可以完成证明，剩下的问题在于我们怎么表达左侧\( \text{t}_1 \)非\( \lambda \)-抽象了，目前我们\( \lambda \)-演算系统中就只有三种形式的项：变量、\( \lambda \)-抽象、\( \lambda \)-应用，故所有非\( \lambda \)-抽象的项要么是变量，要么是\( \lambda \)-应用，于是我们引入如下语法类别： \[ \begin{aligned} \text{na} &::= \qquad \textit{non-abstractions:} \\ &\text{x} \\ &\text{t} \text{ } \text{t} \end{aligned} \] 进一步添加新规则： \[ \dfrac{\text{na}_1 \rightarrow \text{na}'_1}{ \text{na}_1 \text{ } \text{t}_2 \rightarrow \text{na}'_1 \text{ } \text{t}_2} \qquad (\text{E-REDUCE-LEFT}) \]

      2. 如果要对右侧部分\( \text{t}_2 \)进行求值，则我们至少需要保证\( \text{t}_2 \)的最左边、最外层的redex和\( \text{t} \)的最左边、最外层的redex一样，这要求\( \text{t}_1 \)没有redex，不仅如此，\( \text{t}_1 \)还不能是\( \lambda \)-抽象，否则\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)整个就是最左边、最外层redex，问题在于我们怎么定义一个语法类别用于表达\( \text{t}_1 \)没有redex且非\( \lambda \)-抽象了，我们命名该语法类别为non-abstraction-no-redexes，它的定义实际上还是比较简单的，应该包含：变量、满足“函数位置没有redex且非\( \lambda \)-抽象，参数位置没有redex”的\( \lambda \)-应用，重点关注后者，即满足“函数位置没有redex且非\( \lambda \)-抽象，参数位置没有redex”的\( \lambda \)-应用，它包含了两个语法类别：

         1. 没有redex且非\( \lambda \)-抽象
         2. 没有redex

         第一个语法类别是我们正在尝试定义的non-abstraction-no-redexes，第二个语法类别我们命名为no-redexes，和non-abstraction-no-redexes类似，但是并不禁止\( \lambda \)-抽象，故no-redexes在包含non-abstraction-no-redexes所有项的基础上，还额外包含函数体没有redex的\( \lambda \)-抽象，综上，我们给出non-abstraction-no-redexes、no-redexes的定义，如下： \[ \begin{aligned} \text{nanr} &::= \qquad \textit{non-abstraction-no-redexes:} \\ &\text{x} \\ &\text{nanr} \text{ } \text{nr} \\ \text{nr} &::= \qquad \textit{no-redexes:} \\ &\text{nanr} \\ &\lambda \text{x. } \text{nr} \end{aligned} \] （注：上面两个语法类别定义相互引用，理解这两个定义的关键在于，当\( \text{nanr} \)出现在\( \text{nr} \)定义右侧时，抽象地把\( \text{nanr} \)看成所有满足“没有redex且非\( \lambda \)-抽象”，且同时满足“大小比被定义项\( \text{nr} \)更小或者一样大”的项，类似的，当\( \text{nr} \)出现在\( \text{nanr} \)定义右侧，抽象地把\( \text{nr} \)看成所有满足“没有redex”，且同时满足“大小比被定义项\( \text{nanr} \)更小或者一样大”的项，由于当一个语法类别A引用到另外一个语法类别B时，这B对应的项要么比A对应的项小，要么一样大（比如\( \text{nr} = \text{nanr} \)就是一样大），故很容易用大小归纳法来证明上述两个语法类别的定义是正确的）现在，我们已经有语法类别non-abstraction-no-redexes用于保证\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)的左侧\( \text{t}_1 \)没有redex且非\( \lambda \)-抽象，进而保证了\( \text{t}_2 \)的最左边、最外层的redex和\( \text{t} \)的最左边、最外层的redex一样，于是我们可以新增规则E-REDUCE-RIGHT了，如下： \[ \dfrac{\text{t}_2 \rightarrow \text{t}'_2}{ \text{nanr}_1 \text{ } \text{t}_2 \rightarrow \text{nanr}_1 \text{ } \text{t}'_2} \qquad (\text{E-REDUCE-RIGHT}) \]

综上，我们所有的语法类别定义如下：

\[ \begin{aligned} \text{na} &::= \qquad \textit{non-abstractions:} \\ &\text{x} \\ &\text{t} \text{ } \text{t} \\ \text{nanr} &::= \qquad \textit{non-abstraction-no-redexes:} \\ &\text{x} \\ &\text{nanr} \text{ } \text{nr} \\ \text{nr} &::= \qquad \textit{no-redexes:} \\ &\text{nanr} \\ &\lambda \text{x. } \text{nr} \end{aligned} \]

所有的求值规则定义如下：

\[ \begin{aligned} \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{ \lambda \text{x. } \text{t}_1 \rightarrow \lambda \text{x. } \text{t}'_1} &\qquad (\text{E-ABS}) \\ (\lambda \text{x. } \text{t}_{11}) \text{ } \text{t}_2 \rightarrow [\text{x} \mapsto \text{t}_2]\text{t}_{11} &\qquad (\text{E-APPABS}) \\ \dfrac{\text{na}_1 \rightarrow \text{na}'_1}{ \text{na}_1 \text{ } \text{t}_2 \rightarrow \text{na}'_1 \text{ } \text{t}_2} &\qquad (\text{E-REDUCE-LEFT}) \\ \dfrac{\text{t}_2 \rightarrow \text{t}'_2}{ \text{nanr}_1 \text{ } \text{t}_2 \rightarrow \text{nanr}_1 \text{ } \text{t}'_2} &\qquad (\text{E-REDUCE-RIGHT}) \end{aligned} \]

易使用大小归纳法证明上述规则满足normal-order求值策略的约束，这里就省略了。

修改求值规则以适应lazy evaluation求值策略：

lazy evaluation求值策略类似call-by-value求值策略，不过不同于call-by-value，lazy evaluation在求值具有\( \text{v}_1 \text{ } \text{t}_2 \)形式的项时，不会把\( \text{t}_2 \)求值成值，而是不求值，直接把整个\( \text{t}_2 \)原封不动代入到\( \text{v}_1 \)的函数体中，之后在函数体中实际要用到该代入的参数时，才对该参数进行求值，而我们目前的\( \lambda \)-演算系统中只有函数、也就是\( \lambda \)-抽象这一种对象， \( \lambda \)-抽象唯一的作用就是作为函数被应用，故我们只有在一个项要作为函数被应用时，才去求值该项，这实际上就是E-APP1规则，故该规则保留。规则E-APP2则删除，它的作用是限制必须在函数位置的项求值成值后，才去求值参数位置的项， lazy evaluation不需要该规则，因为在不知道参数位置的项有没有被使用时，我们是不会求值一个项的。规则E-APPABS需要修改下， lazy evaluation不需要限制参数位置的项为值。最终所有规则如下：

\[ \begin{aligned} \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{\text{t}_1 \text{ } \text{t}_2 \rightarrow \text{t}'_1 \text{ } \text{t}_2} &\qquad (\text{E-APP1}) \\ (\lambda \text{x. } \text{t}_{11}) \text{ } \text{t}_2 \rightarrow [\text{x} \mapsto \text{t}_2]\text{t}_{11} &\qquad (\text{E-NEW-APPABS}) \end{aligned} \]

规则E-APP1确保了我们只有在一个项实际被使用时，才去求值该项，规则E-NEW-APPABS则确保了我们可以实际进行求值。

练习5.3.7

题目：

Exercise 3.5.16 gave an alternative presentation of the operational semantics of booleans and arithmetic expressions in which stuck terms are defined to evaluate to a special constant \( \text{wrong} \). Extend this semantics to \( \lambda \textbf{NB} \).

解答：

我们在练习3.5.16的基础上进行修改就行了，关键在于要额外处理错误：进行\( \lambda \)-应用时，函数位置的值非\( \lambda \)-抽象。

先引入一些新的语法类别：

\[ \begin{aligned} \text{badnat} &::= &\qquad \textit{non-numeric normal forms:} \\ &\text{wrong} &\qquad \textit{run-time error} \\ &\text{true} &\qquad \textit{constant true} \\ &\text{false} &\qquad \textit{constant false} \\ &\lambda \text{x. } \text{t} &\qquad \textit{abstraction value} \\ \text{badbool} &::= &\qquad \textit{non-boolean normal forms:} \\ &\text{wrong} &\qquad \textit{run-time error} \\ &\text{nv} &\qquad \textit{numeric value} \\ &\lambda \text{x. } \text{t} &\qquad \textit{abstraction value} \\ \text{badabs} &::= &\qquad \textit{non-abstraction normal forms:} \\ &\text{wrong} &\qquad \textit{run-time error} \\ &\text{true} &\qquad \textit{constant true} \\ &\text{false} &\qquad \textit{constant false} \\ &\text{nv} &\qquad \textit{numeric value} \end{aligned} \]

接着额外加入如下规则：

\[ \begin{aligned} \text{if badbool then } \text{t}_1 \text{ else } \text{t}_2 \rightarrow \text{ wrong} &\qquad \text{(E-IF-WRONG)} \\ \text{succ badnat} \rightarrow \text{ wrong} &\qquad \text{(E-SUCC-WRONG)} \\ \text{pred badnat} \rightarrow \text{ wrong} &\qquad \text{(E-PRED-WRONG)} \\ \text{iszero badnat} \rightarrow \text{ wrong} &\qquad \text{(E-ISZERO-WRONG)} \\ \text{badabs } \text{v}_2 \rightarrow \text{ wrong} &\qquad \text{(E-APPABS-WRONG)} \end{aligned} \]

注意下规则E-APPABS-WRONG，我们没有写成：

\[ \text{badabs } \text{t}_2 \rightarrow \text{ wrong} \qquad \text{(E-APPABS-WRONG)} \]

即我们还是在把参数求值为值后，才去求值\( \lambda \)-应用，即使我们已经知道函数位置非\( \lambda \)-抽象，必会发生运行时错误了，我们仍去求值参数，这样做是为了确保拓展新规则后的求值关系仍具有确定性。提前知道会发生运行时错误，仍去求值参数是没问题的，反正之后还是会发生运行时错误，只不过发生时机的早晚罢了，不影响程序的正确性。

还有一个潜在的错误是我们没有处理的，考虑如下项：

\[ \text{x true} \]

该项中有一个自由变量\( \text{x} \)，这里我们并不知道变量\( \text{x} \)的实际值是什么，如果\( \text{x} \)的实际值非\( \lambda \)-抽象，则应该发生运行时错误，问题在于\( \text{x} \)是自由变量，我们无法知道实际值。不过所有合法、有完整意义的程序都是从一个完整的、没有自由变量的项开始求值的（即从closed term开始求值），故这里我们并不关心\( \text{x true} \)是否发生运行时错误的问题，不处理这种情况。

练习5.3.8

题目：

Exercise 4.2.2 introduced a “big-step” style of evaluation for arithmetic expressions, where the basic evaluation relation is “term \( \text{t} \) evaluates to final result \( \text{v} \).” Show how to formulate the evaluation rules for lambda-terms in the big-step style.

解答：

\[ \begin{aligned} \lambda \text{x. } \text{t} \Downarrow \lambda \text{x. } \text{t} &\qquad (\text{B-VALUE}) \\ \dfrac{\text{t}_1 \Downarrow \lambda \text{x. } \text{t}_{11} \quad \text{t}_2 \Downarrow \text{v}_2 \quad [\text{x} \mapsto \text{v}_2]\text{t}_{11} \Downarrow \text{t}'}{ \text{t}_1 \text{ } \text{t}_2 \Downarrow \text{t}'} &\qquad (\text{B-APPABS}) \end{aligned} \]