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

第20章

章节20.1

练习20.1.1

题目：

One presentation of labeled binary trees defines a tree to be either a leaf (with no label) or else an interior node with a numeric label and two child trees. Define a type \( \text{NatTree} \) and suitable operations for constructing, destructing, and testing trees. Write a function that performs a depth-first traversal of a tree and returns a list of the labels it finds. Use the \( \text{fullequirec} \) checker to test your code.

解答：

类型定义如下：

\[ \text{NatTree} = \mu \text{X. } \langle \text{leaf}: \text{Unit}, \text{inode}: \{ \text{Nat}, \text{X}, \text{X} \} \rangle \]

这里\( \text{inode} \)标签对应的类型为tuple而不像\( \text{NatList} \)为pair。

首先定义构造二元树的值和函数，这包括：叶子单例值、一个接受数值标签和左右子树以构造二元树的函数：

\[ \text{leaf} = \langle \text{leaf} = \text{unit} \rangle \text{ as NatTree} \]

\[ \text{btree} = \lambda \text{n}: \text{Nat. } \lambda \text{l}: \text{NatTree. } \lambda \text{r}: \text{NatTree. } \langle \text{inode} = \{ \text{n}, \text{l}, \text{r} \} \rangle \text{ as NatTree} \]

接下来定义二元树相关的操作，这包括：判断二元树是否为叶子（空树）、提取数值标签以及左右子树：

\[ \text{isleaf} = \lambda \text{t}: \text{NatTree. } \text{case t of } \langle \text{leaf} = \text{u} \rangle \Rightarrow \text{true} \mid \langle \text{inode} = \text{p} \rangle \Rightarrow \text{false} \]

\[ \text{value} = \lambda \text{t}: \text{NatTree. } \text{case t of } \langle \text{leaf} = \text{u} \rangle \Rightarrow 0 \mid \langle \text{inode} = \text{p} \rangle \Rightarrow \text{p}.1 \]

\[ \text{ltree} = \lambda \text{t}: \text{NatTree. } \text{case t of } \langle \text{leaf} = \text{u} \rangle \Rightarrow \text{leaf} \mid \langle \text{inode} = \text{p} \rangle \Rightarrow \text{p}.2 \]

\[ \text{rtree} = \lambda \text{t}: \text{NatTree. } \text{case t of } \langle \text{leaf} = \text{u} \rangle \Rightarrow \text{leaf} \mid \langle \text{inode} = \text{p} \rangle \Rightarrow \text{p}.3 \]

注意这里我们将叶子的数值标签定义成\( 0 \)，另一种处理方法就是抛出异常，其他函数也类似，下面就不再赘述了。

最后我们写函数对二元树进行深度遍历并将访问到的数值标签以数值列表形式返回，这里需要先定义一个辅助函数\( \text{append} \)，用于合并两个列表为一个列表（元素顺序不变），如下：

\[ \begin{aligned} \text{append} = &\text{ fix } (\lambda \text{f}: \text{NatList} \to \text{NatList} \to \text{NatList.} \\ &\hphantom{fix \lambda \text{f}} \lambda \text{l}_1: \text{NatList.} \\ &\hphantom{fix \lambda \text{f} \lambda \text{l}_1} \lambda \text{l}_2: \text{NatList.} \\ &\hphantom{fix \lambda \text{f} \lambda \text{l}_1 \lambda \text{l}_2} \text{if } (\text{isnil } \text{l}_1) \text{ } \text{l}_2 \\ &\hphantom{fix \lambda \text{f} \lambda \text{l}_1 \lambda \text{l}_2} \text{else } (\text{cons } (\text{hd } \text{l}_1) \text{ } (\text{f } (\text{tl } \text{l}_1) \text{ } \text{l}_2))) \end{aligned} \]

现在可以开始定义深度遍历函数了，如下：

\[ \begin{aligned} \text{df} = &\text{ fix } (\lambda \text{f}: \text{NatTree} \to \text{NatList.} \\ &\hphantom{fix \lambda \text{f}} \lambda \text{t}: \text{NatTree.} \\ &\hphantom{fix \lambda \text{f} \lambda \text{t}} \text{if } (\text{isleaf t}) \text{ } \text{nil} \\ &\hphantom{fix \lambda \text{f} \lambda \text{t}} \text{else } (\text{cons } (\text{value t}) \\ &\hphantom{fix \lambda \text{f} \lambda \text{t} \text{else } \text{acons }} (\text{append } (\text{f } (\text{ltree t})) \text{ } (\text{f } (\text{rtree t}))))) \end{aligned} \]

练习20.1.2

题目：

Define a stream that yields successive elements of the Fibonacci sequence \( (1, 1, 2, 3, 5, 8, 13, \dots) \).

解答：

仿照\( \text{upfrom0} \)就行了，不过\( \text{upfrom0} \)的定义中会接收一个自然数作为流的下一个自然数，我们这边则得接收两个参数：数列当前位置的前两个数字作为参数，以构造数列的下一个数字。

\[ \begin{aligned} \text{fib} = &\text{ fix } (\lambda \text{f}: \text{Nat} \to \text{Nat} \to \text{Stream.} \\ &\hphantom{\text{fix } \lambda \text{f}} \lambda \text{ppn}: \text{Nat.} \\ &\hphantom{\text{fix } \lambda \text{f} \lambda \text{p}} \lambda \text{pn}: \text{Nat.} \\ &\hphantom{\text{fix } \lambda \text{f} \lambda \text{p} \lambda \text{p}} \lambda \text{\_}: \text{Unit.} \\ &\hphantom{\text{fix } \lambda \text{f} \lambda \text{p} \lambda \text{p} \lambda \text{p}} \{ \text{ppn}, \text{f } \text{pn} \text{ } (\text{plus } \text{ppn} \text{ } \text{pn}) \}) \text{ } 1 \text{ } 1 \end{aligned} \]

练习20.1.3

题目：

Extend the \( \text{Counter} \) type and the counter \( \text{c} \) above to include \( \text{backup} \) and \( \text{reset} \) operations (as we did in \( \S \text{18.7} \)): invoking \( \text{backup} \) causes the counter to store its current value in a separate internal register; calling \( \text{reset} \) causes the counter’s value to be reset to the value in this register.

解答：

类型定义如下：

\[ \begin{aligned} \text{ResetCounter} = &\ \mu \text{X. } \{ \text{get}: \text{Nat}, \\ &\hphantom{\ \mu \text{X. } a} \text{inc}: \text{Unit} \to \text{X}, \\ &\hphantom{\ \mu \text{X. } a} \text{dec}: \text{Unit} \to \text{X}, \\ &\hphantom{\ \mu \text{X. } a} \text{backup}: \text{Unit} \to \text{X}, \\ &\hphantom{\ \mu \text{X. } a} \text{reset}: \text{Unit} \to \text{X} \} \end{aligned} \]

构造函数如下：

\[ \begin{aligned} \text{newResetCounter} = &\text{ fix } (\lambda \text{f}: \{ \text{x}: \text{Nat}, \text{b}: \text{Nat} \} \to \text{ResetCounter. } \\ &\hphantom{\text{fix } \lambda \text{f}} \lambda \text{s}: \{ \text{x}: \text{Nat}, \text{b}: \text{Nat} \} \text{. } \\ &\hphantom{\text{fix } \lambda \text{f} \lambda \text{s}} \{ \text{get} = \text{s}.\text{x}, \\ &\hphantom{\text{fix } \lambda \text{f} \lambda \text{s} a} \text{inc} = \lambda \text{\_}: \text{Unit. } \text{f } \{ \text{x} = \text{succ } (\text{s}.\text{x}), \text{b} = \text{s}.\text{b} \}, \\ &\hphantom{\text{fix } \lambda \text{f} \lambda \text{s} a} \text{dec} = \lambda \text{\_}: \text{Unit. } \text{f } \{ \text{x} = \text{pred } (\text{s}.\text{x}), \text{b} = \text{s}.\text{b} \}, \\ &\hphantom{\text{fix } \lambda \text{f} \lambda \text{s} a} \text{backup} = \lambda \text{\_}: \text{Unit. } \text{f } \{ \text{x} = \text{s}.\text{x}, \text{b} = \text{s}.\text{x} \}, \\ &\hphantom{\text{fix } \lambda \text{f} \lambda \text{s} a} \text{reset} = \lambda \text{\_}: \text{Unit. } \text{f } \{ \text{x} = \text{s}.\text{b}, \text{b} = \text{s}.\text{b} \} \}) \text{ } \{ \text{x} = 0, \text{b} = 0 \} \end{aligned} \]

练习20.1.4

题目：

Extend this encoding with booleans and conditionals, and encode the terms \( \text{if false then 1 else 0} \) and \( \text{if false then 1 else false} \) as elements of \( \text{D} \). What happens when we evaluate these terms?

解答：

首先拓展类型\( \text{D} \)，需要额外添加种类布尔，如下：

\[ \text{D} = \mu \text{X. } \langle \text{nat}: \text{Nat}, \text{bool}: \text{Bool}, \text{fn}: \text{X} \to \text{X} \rangle \]

接着，类似\( \text{zro} \)，我们编码布尔值，为了避免和宿主语言（带递归类型的简单类型化lambda演算）的\( \text{true}, \text{false} \)混淆，我们将编码的布尔值命名为\( \text{tru}, \text{fls} \)，它们在宿主语言中分别通过\( \text{true}, \text{false} \)表示，当然，得包裹在variant中，如下：

\[ \text{tru} = \langle \text{bool} = \text{true} \rangle \text{ as D} \]

\[ \text{fls} = \langle \text{bool} = \text{false} \rangle \text{ as D} \]

这里的\( \text{as D} \)算是给类型检查器的提示，同时也简化了类型检查器的算法，不然即使不加\( \text{as D} \)，\( \langle \text{bool} = \text{true} \rangle \)的类型也是\( \text{D} \)。

额外的，我们编码一下自然数\( 1 \)对应的\( \text{one} \)，如下：

\[ \text{one} = \langle \text{nat} = 1 \rangle \text{ as D} \]

接着，我们编码下条件运算，同\( \text{tru}, \text{fls} \)，这里为了避免和宿主语言中的对应构造混淆，命名成\( \text{ifd} \)，函数\( \text{ifd} \)接受条件表达式、真分支表达式、假分支表达式，三个参数的编码（用编译原理的术语来说就是IR）作为参数，解释执行对应的条件运算语句，将解释执行的结果通过编码（IR）的形式返回（结果要么是真分支表达式的编码，要么是假分支表达式的编码），其中，解释执行是通过宿主语言中的\( \text{if} \)来模拟的，如下：

\[ \begin{aligned} \text{ifd} &= \lambda \text{c}: \text{D. } \lambda \text{t}: \text{D. } \lambda \text{f}: \text{D. } \\ &\hphantom{= \lambda \text{c}} \text{case c of} \\ &\hphantom{= \lambda \text{c} c \mid} \langle \text{nat} = \text{n} \rangle \Rightarrow \text{diverge}_D \text{ } \text{unit} \\ &\hphantom{= \lambda \text{c} c} \mid \langle \text{bool} = \text{b} \rangle \Rightarrow \text{if b then t else f} \\ &\hphantom{= \lambda \text{c} c} \mid \langle \text{fn} = \text{f} \rangle \Rightarrow \text{diverge}_D \text{ } \text{unit} \end{aligned} \]

\( \text{lam} \)不需要改，如下：

\[ \text{lam} = \text{f}: \text{D} \to \text{D. } \langle \text{fn} = \text{f} \rangle \text{ as D} \]

\( \text{ap} \)需要添加布尔类型的情况，如下：

\[ \begin{aligned} \text{ap} &= \lambda \text{f}: \text{D. } \lambda \text{a}: \text{D. } \\ &\hphantom{= \lambda \text{f}} \text{case f of} \\ &\hphantom{= \lambda \text{f} c \mid} \langle \text{nat} = \text{n} \rangle \Rightarrow \text{diverge}_D \text{ } \text{unit} \\ &\hphantom{= \lambda \text{f} c} \mid \langle \text{bool} = \text{b} \rangle \Rightarrow \text{diverge}_D \text{ } \text{unit} \\ &\hphantom{= \lambda \text{f} c} \mid \langle \text{fn} = \text{f}_2 \rangle \Rightarrow \text{f}_2 \text{ a} \end{aligned} \]

综上，\( \text{if false then 1 else 0} \)的编码为\( \text{ifd fls one zro} \)， \( \text{if false then 1 else false} \)的编码则为\( \text{ifd fls one fls} \)，

求值\( \text{ifd fls one zro} \)，过程如下：

\[ \begin{aligned} &\hphantom{\rightarrow^*} \text{ifd fls one zro} \\ &\rightarrow^* \text{if false then one else zro} \\ &\rightarrow^* \text{zro} = \langle \text{nat} = 0 \rangle \text{ as D} \end{aligned} \]

最后求值\( \text{ifd fls one fls} \)，过程如下：

\[ \begin{aligned} &\hphantom{\rightarrow^*} \text{ifd fls one fls} \\ &\rightarrow^* \text{if false then one else fls} \\ &\rightarrow^* \text{fls} = \langle \text{bool} = \text{false} \rangle \text{ as D} \end{aligned} \]

至于为什么像\( \text{if false then 1 else false} \)这种在宿主语言中非类型良好（真分支表达式和假分支表达式类型不一样）的项，编码后却是类型良好的项，这是因为我们编码后的系统将所有目标语言构造都统一成一个variant类型\( \text{D} \)了，所以编码后的真假分支表达式的类型都是\( \text{D} \)，类型是相同的。

练习20.1.5

题目：

Extend the datatype \( \text{D} \) to include records

\[ \text{D} = \mu \text{X. } \langle \text{nat}: \text{Nat}, \text{fn}: \text{X} \to \text{X}, \text{rcd}: \text{Nat} \to \text{X} \rangle \]

and implement record construction and field projection. For simplicity, use natural numbers as field labels—i.e., records are represented as functions from natural numbers to elements of \( \text{D} \). Use the \( \text{fullequirec} \) checker to test your extension.

解答：

过程基本类似练习20.1.4。

首先是record构造函数\( \text{rcd} \)，其参数为类型\( \text{Nat} \to \text{D} \)的函数，该函数为标签到值的映射，给定自然数\( \text{n} \)，它会返回record内标签为\( \text{n} \)的值，如下：

\[ \text{rcd} = \lambda \text{map}: \text{Nat} \to \text{D. } \langle \text{rcd = \text{map}} \rangle \text{ as D} \]

取域的函数\( \text{prj} \)就很简单了，如下：

\[ \begin{aligned} \text{prj} &= \lambda \text{r}: \text{D. } \lambda \text{n}: \text{Nat. } \\ &\hphantom{= \lambda \text{r}} \text{case r of} \\ &\hphantom{= \lambda \text{r} c \mid} \langle \text{nat} = \text{n} \rangle \Rightarrow \text{diverge}_D \text{ } \text{unit} \\ &\hphantom{= \lambda \text{r} c} \mid \langle \text{fn} = \text{f}_2 \rangle \Rightarrow \text{diverge}_D \text{ } \text{unit} \\ &\hphantom{= \lambda \text{r} c} \mid \langle \text{rcd} = \text{map} \rangle \Rightarrow \text{map n} \end{aligned} \]

\( \text{lam} \)不需要改，如下：

\[ \text{lam} = \text{f}: \text{D} \to \text{D. } \langle \text{fn} = \text{f} \rangle \text{ as D} \]

\( \text{ap} \)需要添加record的情况，如下：

\[ \begin{aligned} \text{ap} &= \lambda \text{f}: \text{D. } \lambda \text{a}: \text{D. } \\ &\hphantom{= \lambda \text{r}} \text{case r of} \\ &\hphantom{= \lambda \text{r} c \mid} \langle \text{nat} = \text{n} \rangle \Rightarrow \text{diverge}_D \text{ } \text{unit} \\ &\hphantom{= \lambda \text{r} c} \mid \langle \text{fn} = \text{f}_2 \rangle \Rightarrow \text{f}_2 \text{ } \text{a} \\ &\hphantom{= \lambda \text{r} c} \mid \langle \text{rcd} = \text{map} \rangle \Rightarrow \text{diverge}_D \text{ } \text{unit} \end{aligned} \]

最后，作为一个例子，我们创建一个record（用到了练习20.1.4定义的\( \text{one} \)），需要注意处理非法域的情况，如下：

\[ \begin{aligned} \text{map}_1 &= \lambda \text{n}: \text{Nat.} \\ &\hphantom{= \lambda \text{n}} \text{if iszero 0 then zro} \\ &\hphantom{= \lambda \text{n}} \text{else if iszero (pred n) then one} \\ &\hphantom{= \lambda \text{n}} \text{else } \text{diverge}_D \text{ } \text{unit} \\ \text{r}_1 &= \text{rcd } \text{map}_1 \end{aligned} \]

求值下\( \text{prj } \text{r}_1 \text{ } 1 \)，过程如下：

\[ \begin{aligned} &\hphantom{\rightarrow^*} \text{prj } \text{r}_1 \text{ } 1 \\ &\rightarrow^* \text{map}_1 \text{ } 1 \\ &\rightarrow^* \text{one} \end{aligned} \]

章节20.2

练习20.2.1

题目：

Reformulate some of the other examples in \( \S \text{20.1} \) (in particular, the \( \text{fix}_T \) example on page 273) with explicit \( \text{fold} \) and \( \text{unfold} \) annotations. Check them using the \( \text{fullisorec} \) checker.

解答：

先考虑\( \text{fix}_T \)，原定义如下：

\[ \begin{aligned} \text{fix}_T &= \lambda \text{f}: \text{T} \to \text{T. } \\ &\hphantom{= \lambda \text{f}} (\lambda \text{x}: (\mu \text{A. } \text{A} \to \text{T}) \text{. } \text{f } (\text{x x})) \\ &\hphantom{= \lambda \text{f}} (\lambda \text{x}: (\mu \text{A. } \text{A} \to \text{T}) \text{. } \text{f } (\text{x x})) \end{aligned} \]

几个问题，首先就是\( \text{x} \)的类型为\( \mu \text{A. } \text{A} \to \text{T} \)非函数类型，故\( \text{x x} \)中第一个\( \text{x} \)被当成函数使用是非类型良好的，因此我们需要\( \text{unfold } [\mu \text{A. } \text{A} \to \text{T}] \text{ x} \)，以得到函数类型\( (\mu \text{A. } \text{A} \to \text{T}) \to \text{T} \)，其他就问题比较简单了，比如说第二个\( \lambda \text{x}: (\mu \text{A. } \text{A} \to \text{T}) \text{. } \text{f } (\text{x x}) \)的结果需要被\( \text{fold} \)以匹配参数类型，完整定义如下：

\[ \begin{aligned} \text{fix}_T &= \lambda \text{f}: \text{T} \to \text{T. } \\ &\hphantom{= \lambda \text{f}} (\lambda \text{x}: (\mu \text{A. } \text{A} \to \text{T}) \text{. } \text{f } ((\text{unfold } [\mu \text{A. } \text{A} \to \text{T}] \text{ x}) \text{ } \text{x})) \\ &\hphantom{= \lambda \text{f}} (\text{fold } [\mu \text{A. } \text{A} \to \text{T}] \text{ } (\lambda \text{x}: (\mu \text{A. } \text{A} \to \text{T}) \text{. } \text{f } ((\text{unfold } [\mu \text{A. } \text{A} \to \text{T}] \text{ x}) \text{ } \text{x}))) \end{aligned} \]

接着考虑章节20.1对非类型化lambda演算的编码，处理类似上面，没有新东西，对应的定义如下：

\[ \text{D} = \mu \text{X. } \text{X} \to \text{X} \]

\[ \text{lam} = \lambda \text{f}: \text{D} \to \text{D. } \text{fold } [\text{D}] \text{ f} \]

\[ \text{ap} = \lambda \text{f}: \text{D. } \lambda \text{a}: \text{D. } (\text{unfold } [\text{D}] \text{ f}) \text{ a} \]

最后考虑一个稍微长点的例子，即章节20.1中给出来的\( \text{Counter} \)的例子，其定义如下：

\[ \text{Counter} = \mu \text{C. } \{ \text{get}: \text{Nat}, \text{inc}: \text{Unit} \to \text{C}, \text{dec}: \text{Unit} \to \text{C} \} \]

\[ \begin{aligned} \text{newCounter} = &\text{ fix } (\lambda \text{f}: \{ \text{x}: \text{Nat} \} \to \text{Counter. } \\ &\hphantom{\text{fix } \lambda \text{f}} \lambda \text{s}: \{ \text{x}: \text{Nat} \} \text{. } \\ &\hphantom{\text{fix } \lambda \text{f} \lambda \text{s}} \text{fold } [\text{Counter}] \\ &\hphantom{\text{fix } \lambda \text{f} \lambda \text{s} a} \{ \text{get} = \text{s}.\text{x}, \\ &\hphantom{\text{fix } \lambda \text{f} \lambda \text{s} aa} \text{inc} = \lambda \text{\_}: \text{Unit. } \text{f } \{ \text{x} = \text{succ } (\text{s}.\text{x}) \}, \\ &\hphantom{\text{fix } \lambda \text{f} \lambda \text{s} aa} \text{dec} = \lambda \text{\_}: \text{Unit. } \text{f } \{ \text{x} = \text{pred } (\text{s}.\text{x}) \}, \end{aligned} \]

需要注意的是，创建出来的计数器\( \text{c} \)得\( \text{unfold} \)后才能使用，如下：

\[ \text{c} = \text{newCounter } \{ \text{x}: 0 \} \]

\[ \text{c}_1 = (\text{unfold } [\text{Counter}] \text{ c}).\text{inc } \text{unit} \]

练习20.2.2

题目：

Sketch proofs of the progress and preservation theorems for the iso-recursive system.

解答：

注： 如下证明框架只能说是思路，没有验证，实际进行完整证明可能会发现错误的地方，需要修正。

首先是定理9.3.5，即PROGRESS定理，内容如下：

如果\( \text{t} \)为closed的、类型良好的项，则\( \text{t} \)为值或者\( \exists \text{t}' \)满足\( \text{t} \rightarrow \text{t}' \)。

证明过程基本不变，但是需要额外考虑最后使用的类型规则是T-FLD、T-UNFLD的情况，如果最后使用的类型规则是T-FLD，则\( \text{t} = \text{fold } [\text{T}] \text{ } \text{t}_1 \quad \vdash \text{t}_1: [\text{X} \to \mu \text{X. } \text{T}_1] \text{ } \text{T}_1 \)，这种情况比较简单，通过归纳假设可得，要么\( \text{t}_1 \)是值，要么\( \text{t}_1 \rightarrow \text{t}'_1 \)，如果\( \text{t}_1 \)是值，则\( \text{t} \)也是值，如果\( \text{t}_1 \rightarrow \text{t}'_1 \)，则可以使用E-FLD，最后使用的类型规则是T-UNFLD的情况则麻烦点，此时有\( \text{t} = \text{unfold } [\text{T}] \text{ } \text{t}_1 \quad \vdash \text{t}_1: \mu \text{X. } \text{T}_1 \)，通过归纳假设可得，要么\( \text{t}_1 \)是值，要么\( \text{t}_1 \rightarrow \text{t}'_1 \)，如果\( \text{t}_1 \rightarrow \text{t}'_1 \)，那可以使用E-UNFLD，但是如果\( \text{t}_1 \)是值，则我们需要canonical forms引理（引理9.3.4）保证：如果\( \vdash \text{t}_1: \mu \text{X. } \text{T}_1 \)且\( \text{t}_1 \)为值，则\( \text{t}_1 = \text{fold } [\text{S}] \text{ } \text{v}_1 \)，进而可以使用E-UNFLDFLD。

就像上面说的，canonical forms引理要额外保证：如果\( \vdash \text{t}_1: \mu \text{X. } \text{T}_1 \)且\( \text{t}_1 \)为值，则\( \text{t}_1 = \text{fold } [\text{S}] \text{ } \text{v}_1 \)。证明也比较简单，因为\( \vdash \text{t}_1: \mu \text{X. } \text{T}_1 \)唯一可用的规则就是T-FLD了，直接可得结论成立。

为了证明PRESERVATION定理（定理9.3.9），还需要引理9.3.8，即变量代入后的项的类型不变，为了证明引理9.3.8，我们需要PERMUTATION引理（引理9.3.6）以及WEAKENING引理（引理9.3.7），三个引理的证明基本不变，也只是需要额外考虑使用T-FLD、T-UNFLD的情况。

最后就可以证明PRESERVATION定理了，同样的，证明基本不变，也只是需要额外考虑使用T-FLD、T-UNFLD的情况。