OSFVA
所有文章 标签
OSFVA

目录

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

CloseToZero
   约 23637 字   预计阅读 48 分钟 

第21章

章节21.1

练习21.1.7

题目：

Suppose a generating function \( E_2 \) on the universe \( \{ a, b, c \} \) is defined by the following inference rules:

\[ \dfrac{}{a} \quad \dfrac{c}{b} \quad \dfrac{a \quad b}{c} \]

Write out the set of pairs in the relation \( E_2 \) explicitly, as we did for \( E_1 \) above. List all the \( E_2 \)-closed and \( E_2 \)-consistent sets. What are \( \mu E_2 \) and \( \nu E_2 \)?

解答：

显式列出\( E_2 \)关系：

  1. \( E_2(\empty) = \{ a \} \)
  2. \( E_2(\{ a \}) = \{ a \} \)
  3. \( E_2(\{ b \}) = \{ a \} \)
  4. \( E_2(\{ c \}) = \{ a, b \} \)
  5. \( E_2(\{ a, b \}) = \{ a, c \} \)
  6. \( E_2(\{ a, c \}) = \{ a, b \} \)
  7. \( E_2(\{ b, c \}) = \{ a, b \} \)
  8. \( E_2(\{ a, b, c \}) = \{ a, b, c \} \)

所有\( E_2 \)-closed集合：

  1. \( \{ a \} \)
  2. \( \{ a, b, c \} \)

所有\( E_2 \)-consistent集合：

  1. \( \empty \)
  2. \( \{ a \} \)
  3. \( \{ a, b, c \} \)

最小不动点\( \mu E_2 \)：

\( \{ a \} \)

最大不动点\( \nu E_2 \)：

\( \{ a, b, c \} \)

练习21.1.9

题目：

Show that the principles of ordinary induction on natural numbers (2.4.1) and lexicographic induction on pairs of numbers (2.4.4) follow from the principle of induction in 21.1.8.

ordinary induction on natural numbers (2.4.1)的内容：

Suppose that \( P \) is a predicate on the natural numbers. Then:

  • If \( P(0) \)
  • and, for all \( i \), \( P(i) \) implies \( P(i + 1) \),
  • then \( P(n) \) holds for all \( n \).

lexicographic induction on pairs of numbers (2.4.4)的内容：

首先需要定义lexicographic order：

The lexicographic order (or “dictionary order”) on pairs of natural numbers is defined as follows: \( (m, n) \leq (m', n') \) iff either \( m < m' \) or else \( m = m' \) and \( n \leq n' \).

现在就可以讲lexicographic induction的内容了：

Suppose that \( P \) is a predicate on pairs of natural numbers.

  • If for each pair \( (m, n) \) of natural numbers,
    • given \( P(m', n') \) for all \( (m', n') < (m, n) \)
    • we can show \( P(m, n) \),
  • then \( P(m, n) \) holds for all \( m, n \).

principle of induction in 21.1.8的内容：

If \( X \) if \( F \)-closed, then \( \mu F \subseteq X \).

解答：

我们打算用principle of induction去证明ordinary induction on natural numbers以及 lexicographic induction on pairs of numbers，为此，我们先定义characteristic set的概念。

characteristic set：

给定限定域\( U \)（或者称为宇集，反正就是用于限定讨论范围/域的集合）上的predicate \( P \)，我们定义\( P \)的characteristic set为\( P_C = \{ P(x) \mid x \in U \} \)，即\( U \)中所有使得\( P(x) \)为真的对象\( x \)组成的集合。

使用principle of induction证明ordinary induction on natural numbers：

给定一个predicate \( P \)，它满足：

  • If \( P(0) \)
  • and, for all \( i \), \( P(i) \) implies \( P(i + 1) \).

我们想证明\( \forall \)自然数\( n \)，均有\( P(n) \)为真（即ordinary induction on natural numbers成立），根据characteristic set的定义，这等价于证明\( P_C = \mathbf{N} \)。

定义函数\( F: \mathcal{P}(\mathbf{N}) \to \mathcal{P}(\mathbf{N}) \)， \( \forall X \subseteq \mathbf{N} \)，令\( F(X) = \{ 0 \} \cup \{ i + 1 \mid i \in X \} \)，易证\( \forall X \subseteq Y \)，有\( F(X) \subseteq F(Y) \)，即\( F \)为单调函数。

我们首先证明\( \mu F = \mathbf{N} \)，根据定理21.1.4（以及它的证明），这需要证明两点：

  1. \( \mathbf{N} \)为\( F \)-closed集合。
  2. \( \mathbf{N} \)为最小的\( F \)-closed集合。

先证明\( \mathbf{N} \)为\( F \)-closed集合，即证明\( F(\mathbf{N}) \subseteq \mathbf{N} \)，这点可直接由\( F \)的值域为\( \mathcal{P}(\mathbf{N}) \)得到。

再证明\( \mathbf{N} \)为最小的\( F \)-closed集合，要证明这点，我们只需要证明任意严格比\( \mathbf{N} \)“小”的集合均不是\( F \)-closed集合即可：

\( \forall X \subsetneq \mathbf{N} \)，有\( \mathbf{N} \setminus X \)非空，根据well-ordering principle，可得\( \mathbf{N} \setminus X \)存在最小元\( i_0 \)，接下来分情况讨论：

  1. 如果\( i_0 = 0 \)，则有\( 0 \in F(X), 0 \notin X \)，于是有\( F(X) \nsubseteq X \)，即\( X \)非\( F \)-closed集合。
  2. 如果\( i_0 \neq 0 \)，则\( \exists i_1 \in \mathbf{N} \)满足\( i_1 + 1 = i_0 \)，由于\( i_0 \)为\( \mathbf{N} \setminus X \)的最小元，又\( i_1 < i_0 \)，因此\( i_1 \notin \mathbf{N} \setminus X \)，不然\( i_0 \)就不会是最小元了，由\( i_1 \notin \mathbf{N} \setminus X \)以及\( i_1 \in \mathbf{N} \)，可得\( i_1 \in X \)，于是根据\( F \)的定义，可得\( i_0 = i_1 + 1 \in F(X) \)，但\( i_0 \notin X \)，于是有\( F(X) \nsubseteq X \)，即\( X \)非\( F \)-closed集合。

综上，\( \mathbf{N} \)为最小的\( F \)-closed集合，于是有\( \mu F = \mathbf{N} \)，既然有\( \mu F = \mathbf{N} \)了，那么证明\( P_C = \mathbf{N} \)就等价于证明\( P_C = \mu F \)，但是我们已经知道\( P_C \)必定\( \subseteq \mathbf{N} = \mu F \)（因为宇集\( U = \mathbf{N} \)），故我们只需要证明\( \mu F \subseteq P_C \)，就能证明\( P_C = \mu F \)了：

由\( P \)满足：

  • If \( P(0) \)
  • and, for all \( i \), \( P(i) \) implies \( P(i + 1) \).

可得\( 0 \in P_C, \forall i \in P_C, i + 1 \in P_C \)，进而可得\( F(P_C) \subseteq P_C \)，即\( P_C \)为\( F \)-closed集合，而\( \mu F \)为最小的\( F \)-closed集合，于是有\( \mu F \subseteq P_C \)。

综上，有\( P_C = \mu F = \mathbf{N} \)，至此，我们证明了\( P \)对所有自然数均成立，也就是ordinary induction on natural numbers成立。

使用principle of induction证明lexicographic induction on pairs of numbers：

证明方法和上面类似，复制下来改下即可。

给定一个predicate \( P \)，它满足：

  • If for each pair \( (m, n) \) of natural numbers,
    • given \( P(m', n') \) for all \( (m', n') < (m, n) \)
    • we can show \( P(m, n) \),
  • then \( P(m, n) \) holds for all \( m, n \).

我们想证明\( \forall \)自然数\( m, n \)，均有\( P(m, n) \)为真（即lexicographic induction on pairs of numbers成立），根据characteristic set的定义，这等价于证明\( P_C = \mathbf{N} \times \mathbf{N} \)。

定义函数\( F: \mathcal{P}(\mathbf{N} \times \mathbf{N}) \to \mathcal{P}(\mathbf{N} \times \mathbf{N}) \)， \( \forall X \subseteq \mathbf{N} \times \mathbf{N} \)，令\( F(X) = \{ (m, n) \mid \forall (m', n') < (m, n), \text{ we have } (m', n') \in X \} \)，易证\( \forall X \subseteq Y \)，有\( F(X) \subseteq F(Y) \)，即\( F \)为单调函数。

我们首先证明\( \mu F = \mathbf{N} \times \mathbf{N} \)，根据定理21.1.4（以及它的证明），这需要证明两点：

  1. \( \mathbf{N} \times \mathbf{N} \)为\( F \)-closed集合。
  2. \( \mathbf{N} \times \mathbf{N} \)为最小的\( F \)-closed集合。

先证明\( \mathbf{N} \times \mathbf{N} \)为\( F \)-closed集合，即证明\( F(\mathbf{N} \times \mathbf{N}) \subseteq \mathbf{N} \times \mathbf{N} \)，这点可直接由\( F \)的值域为\( \mathcal{P}(\mathbf{N} \times \mathbf{N}) \)得到。

再证明\( \mathbf{N} \times \mathbf{N} \)为最小的\( F \)-closed集合，要证明这点，我们只需要证明任意严格比\( \mathbf{N} \times \mathbf{N} \)“小”的集合均不是\( F \)-closed集合即可：

\( \forall X \subsetneq \mathbf{N} \times \mathbf{N} \)，有\( (\mathbf{N} \times \mathbf{N}) \setminus X \)非空，根据well-ordering principle（需要证明\( \mathbf{N} \times \mathbf{N} \)是well-ordering集合，这里就不证明了，具体参考Is Dictionary order on \( \mathbf{N} \times \mathbf{N} \) a well order?），可得\( (\mathbf{N} \times \mathbf{N}) \setminus X \)存在最小元\( p_0 \)，由此可得\( \forall (m', n') < p_0, (m', n') \in X \)，这是因为：假设\( \exists (m', n') < p_0, (m', n') \notin X \)，则\( (m', n') \in (\mathbf{N} \times \mathbf{N}) \setminus X \)，加上\( (m', n') < p_0 \)，这和\( p_0 \)为\( (\mathbf{N} \times \mathbf{N}) \setminus X \)的最小元相矛盾，因此假设不成立，有\( \forall (m', n') < p_0, (m', n') \in X \)，进而根据\( F \)的定义，可得\( p_0 \in F(X) \)，加上\( p_0 \notin X \)，可得\( F(X) \nsubseteq X \)，即\( X \)非\( F \)-closed集合。

综上，\( \mathbf{N} \times \mathbf{N} \)为最小的\( F \)-closed集合，于是有\( \mu F = \mathbf{N} \times \mathbf{N} \)，既然有\( \mu F = \mathbf{N} \times \mathbf{N} \)了，那么证明\( P_C = \mathbf{N} \times \mathbf{N} \)就等价于证明\( P_C = \mu F \)，但是我们已经知道\( P_C \)必定\( \subseteq \mathbf{N} \times \mathbf{N} = \mu F \) （因为宇集\( U = \mathbf{N} \times \mathbf{N} \)），故我们只需要证明\( \mu F \subseteq P_C \)，就能证明\( P_C = \mu F \)了：

由\( P \)满足：

  • If for each pair \( (m, n) \) of natural numbers,
    • given \( P(m', n') \) for all \( (m', n') < (m, n) \)
    • we can show \( P(m, n) \),
  • then \( P(m, n) \) holds for all \( m, n \).

可得：给定\( (m, n) \in \mathbf{N} \times \mathbf{N} \)，如果\( \forall (m', n') < (m, n), (m', n') \in P_C \)，则有\( (m, n) \in P_C \)，进而可得\( F(P_C) \subseteq P_C \)，即\( P_C \)为\( F \)-closed集合，而\( \mu F \)为最小的\( F \)-closed集合，于是有\( \mu F \subseteq P_C \)。

综上，有\( P_C = \mu F = \mathbf{N} \times \mathbf{N} \)，至此，我们证明了\( P \)对所有自然数对均成立，也就是lexicographic induction on pairs of numbers成立。

章节21.2

练习21.2.2

题目：

Following the ideas in the previous paragraph, suggest a universe \( \mathcal{U} \) and a generating function \( F \in \mathcal{P}(\mathcal{U}) \to \mathcal{P}(\mathcal{U}) \) such that the set of finite tree types \( \mathcal{T}_f \) is the least fixed point of \( F \) and the set of all tree types \( T \) is its greatest fixed point.

附注：

给定一个树类型\( \text{T}: \{ 1, 2 \}^* \to \{ \to, \times, \text{Top} \} \)，这里\( \{ 1, 2 \}^* \)为1、2序列组成的集合，其不包含无限序列，比如令\( (a_i)_{i = 0}^{+\infty}, \forall i \in \mathbf{N}, a_i = 1 \)，则\( (a_i)_{i = 0}^{+\infty} \)为元素全是1的无限序列，这里\( \{ 1, 2 \}^* \)并不包含这种无限序列，这里“1、2序列”均为有限序列，而\( \{ 1, 2 \}^* \)则是所有这些有限序列所组成的集合，和自然数\( \mathbf{N} \)一样，里面的各个元素都是有限的，但是\( \{ 1, 2 \}^* \)本身却可以是无限的。

解答：

宇集\( \mathcal{U} \)应该是在定义21.2.1的基础上，丢弃最后两条限制所产生的所有偏函数的集合，具体的，我们先定义下树类型候补的概念。

树类型候补：

树类型候补为偏函数\( \text{C} \in \{ 1, 2 \}^* \to \{ \to, \times, \text{Top} \} \)，满足如下限制：

  • \( \text{C}(\bullet) \)有定义。
  • 如果\( \text{C}(\pi, \sigma) \)有定义，则\( \text{C}(\pi) \)也有定义。

我们定义宇集\( \mathcal{U} \)为所有树类型候补\( \text{C} \)（偏函数）所组成的集合。

接下来我们考虑如何定义生成函数\( F \in \mathcal{P}(\mathcal{U}) \to \mathcal{P}(\mathcal{U}) \)，想下给定一个集合\( \text{X} \)，里面是已有的树类型候补，我们生成函数\( F \)如何拿这些已有的树类型候补去构建新的树类型候补呢？很简单，以操作符\( \to \)或者\( \times \)构建一个新的根节点，然后任取已有的两个树类型候补\( \text{T}_1, \text{T}_2 \in X \)（注：\( \text{T}_1, \text{T}_2 \)可以相同）分别作为新根节点的左右子树，以此产生一个新的树类型候补，当然，作为基础情况，我们还得包含\( \text{Top} \)，具体的：定义生成函数\( F \in \mathcal{P}(\mathcal{U}) \to \mathcal{P}(\mathcal{U}) \)， \( \forall X \subseteq \mathcal{U} \)，令\( F(X) = \{ \text{Top} \} \cup \{ \text{T}_1 \to \text{T}_2 \mid \text{T}_1, \text{T}_2 \in X \} \cup \{ \text{T}_1 \times \text{T}_2 \mid \text{T}_1, \text{T}_2 \in X \} \)，易证\( F \)为单调函数。

证明\( \mathcal{T}_f \)为\( F \)的最小不动点\( \mu F \)：

为了证明\( \mathcal{T}_f \)为\( F \)的最小不动点\( \mu F \)，需要证明两点：

  1. \( \mu F \subseteq \mathcal{T}_f \)，这仅需要证明\( \mathcal{T}_f \)为\( F \)-closed集合即可，因为\( \mu F \)为最小的\( F \)-closed集合。
  2. \( \mathcal{T}_f \subseteq \mu F \)。

先证明\( \mathcal{T}_f \)为\( F \)-closed集合： \( \forall \text{T} \in F(\mathcal{T}_f) \)，我们有：

  1. \( \text{T} = \text{Top} \)。
  2. \( \exists \text{T}_1, \text{T}_2 \in \mathcal{T}_f, \text{T} = \text{T}_1 \to \text{T}_2 \)。
  3. \( \exists \text{T}_1, \text{T}_2 \in \mathcal{T}_f, \text{T} = \text{T}_1 \times \text{T}_2 \)。

分情况讨论：

  1. 如果\( \text{T} = \text{Top} \)，则直接有\( \text{T} \in \mathcal{T}_f \)。
  2. 如果\( \text{T} = \text{T}_1 \to \text{T}_2 \)，则易验证\( \text{T} \)也满足定义21.2.1，同时\( |dom(\text{T})| = |dom(\text{T}_1)| + |dom(\text{T}_2)| + 1 \)， \( dom(\text{T}) \)仍然是有限的，因此\( \text{T} \)是有限的，综合可得\( \text{T} \in \mathcal{T}_f \)。
  3. 如果\( \text{T} = \text{T}_1 \times \text{T}_2 \)，则同\( \text{T} = \text{T}_1 \to \text{T}_2 \)，可得\( \text{T} \in \mathcal{T}_f \)，这里不再赘述。

综上，我们有\( \forall \text{T} \in F(\mathcal{T}_f), \text{T} \in \mathcal{T}_f \)，即\( F(\mathcal{T}_f) \subseteq \mathcal{T}_f \)，这意味着\( \mathcal{T}_f \)为\( F \)-closed集合。

接着证明\( \mathcal{T}_f \subseteq \mu F \)：由于\( \mathcal{T}_f \)由所有有限的树类型组成，这些树类型的深度均是有限的，因此可以用数学归纳法来证明，我们先定义树类型的深度， \( \forall \text{T} \in \mathcal{T}_f \)，我们定义树类型的深度\( d(\text{T}) = \max(\{ \text{序列} \pi \text{的长度} \mid \pi \text{为1、2序列且} \text{T}(\pi) \text{有定义} \}) \)，也就是\( d(\text{T}) \)为从\( \text{T} \)的根节点到叶子节点的最长路径。

我们证明\( \forall n \in \mathbf{N} \)，给定任意\( \text{T} \in \mathcal{T}_f \)，如果\( d(\text{T}) = n \)，则\( \text{T} \in \mu F \)：归纳假设\( \forall n' < n \)命题成立，我们证明命题对\( n \)成立：

  1. 当\( n = 0 \)时，如果\( d(\text{T}) = n \)，则\( \text{T} = \text{Top} \)，易得\( \text{T} \in \mu F \)（不然\( \mu F \)就不\( F \)-closed，矛盾）。
  2. 当\( n > 0 \)时，如果\( d(\text{T}) = n \)，则\( \text{T} = \text{T}_1 \to \text{T}_2 \)或\( \text{T} = \text{T}_2 \times \text{T}_2 \) （否则会违反定义21.2.1的条件4）：
    1. 如果\( \text{T} = \text{T}_1 \to \text{T}_2 \)，则\( d(\text{T}_1) < n \)，根据归纳假设，可得\( \text{T}_1 \in \mu F \)，同理可得\( \text{T}_2 \in \mu F \)，于是根据\( F \)的定义，可得\( \text{T} = \text{T}_1 \to \text{T}_2 \in F(\mu F) \)，又\( \mu F \)为\( F \)-closed集合，可得\( \text{T} \in \mu F \)。
    2. 如果\( \text{T} = \text{T}_1 \times \text{T}_2 \)，则同上，易得\( \text{T} \in F(\mu F)\)，这里不再赘述。

综上，归纳完毕，有\( \forall n \in \mathbf{N} \)，给定任意\( \text{T} \in \mathcal{T}_f \)，如果\( d(\text{T}) = n \)，则\( \text{T} \in \mu F \)，这意味着\( \mathcal{T}_f \subseteq \mu F \)。

综上，我们有\( \mu F \subseteq \mathcal{T}_f, \mathcal{T}_f \subseteq \mu F \)，可得\( \mathcal{T}_f = \mu F \)。

证明\( \mathcal{T} \)为\( F \)的最大不动点\( \nu F \)：

为了证明\( \mathcal{T} \)为\( F \)的最大不动点\( \nu F \)，需要证明两点：

  1. \( \mathcal{T} \subseteq \nu F \)，这仅需要证明\( \mathcal{T} \)为\( F \)-consistent集合即可，因为\( \nu F \)为最大的\( F \)-consistent集合。
  2. \( \nu F \subseteq \mathcal{T} \)。

先证明\( \mathcal{T} \)为\( F \)-consistent集合： \( \forall \text{T} \in \mathcal{T} \)，我们有：

  1. \( \text{T} = \text{Top} \)。
  2. \( \exists \text{T}_1, \text{T}_2 \in \mathcal{T}, \text{T} = \text{T}_1 \to \text{T}_2 \)。
  3. \( \exists \text{T}_1, \text{T}_2 \in \mathcal{T}, \text{T} = \text{T}_1 \times \text{T}_2 \)。

分情况讨论：

  1. 如果\( \text{T} = \text{Top} \)，则根据\( F \)的定义，直接有\( \text{T} \in F(\mathcal{T}) \)。
  2. 如果\( \text{T} = \text{T}_1 \to \text{T}_2 \)，则易得\( \text{T}_1, \text{T}_2 \)也满足定义21.2.1 （否则\( \text{T} \)就会违反定义21.2.1），于是可得\( \text{T}_1, \text{T}_2 \in \mathcal{T} \)，进而根据\( F \)的定义，可得\( \text{T} = \text{T}_1 \to \text{T}_2 \in F(\mathcal{T}) \)。
  3. 如果\( \text{T} = \text{T}_1 \times \text{T}_2 \)，则同\( \text{T} = \text{T}_1 \to \text{T}_2 \)，这里不再赘述。

综上，我们有\( \forall \text{T} \in \mathcal{T}, \text{T} \in F(\mathcal{T}) \)，即\( \mathcal{T} \subseteq F(\mathcal{T}) \)，这意味着\( \mathcal{T} \)为\( F \)-consistent集合。

接着证明\( \nu F \subseteq \mathcal{T} \)：这里\( \forall \text{C} \in \nu F \)，我们需要证明\( \text{C} \in \mathcal{T} \)，也就是我们要证明\( \text{C} \)满足定义21.2.1，由于宇集\( \mathcal{U} \)中的所有对象均满足定义21.2.1的前两点，因此我们仅需要证明 \( \text{C} \)满足定义21.2.1的后两点即可。我们证明\( \forall n \in \mathbf{N} \)，给定任意树类型候补\( \text{C} \in \nu F \)以及路径\( \pi \)满足\( |\pi| = n \)，则\( \text{C}, \pi \)满足定义21.2.1的后两点，归纳假设\( \forall n' < n \)命题成立，我们证明命题对\( n \)成立：

针对定义21.2.1的最后一点，如果\( \text{C}(\pi) = \text{Top} \)，此时假设\( \text{C}(\pi, 1) \)有定义或者\( \text{C}(\pi, 2) \)有定义，则根据\( F \)的定义，可得\( \text{C} \notin F(\nu F) \) （这是因为\( F \)的定义中，只有一种方法构造根节点为\( \text{Top} \)的树类型候补，构造出来的树类型候补的左右子树都是未定义的），这和\( \nu F \)为\( F \)-consistent集合相矛盾，因此假设不成立，有\( \text{C}(\pi, 1), \text{C}(\pi, 2) \)均未定义，满足21.2.1的最后一点。

剩下的就是证明满足定义21.2.2的倒数第二点。

  1. 当\( n = 0 \)时，此时\( \pi = \bullet \)：针对定义21.2.1的倒数第二点，如果\( \text{C}(\pi) = \to \)或\( \text{C}(\pi) = \times \)，假设\( \text{C}(\pi, 1) \)未定义或\( \text{C}(\pi, 2) \)未定义，则我们断言\( \text{C} \notin F(\nu F) \)，这是因为假设\( \text{C} \in F(\nu F) \)，则根据\( F \)的定义，可得\( \exists C_1, C_2 \in \nu F \)，\( \text{C} = \text{C}_1 \to \text{C}_2 \)或 \( \text{C} = \text{C}_1 \times \text{C}_2 \)，不妨设\( \text{C} = \text{C}_1 \to \text{C}_2 \)，则\( \text{C}(\bullet) = \to, \forall i \in \{ 1, 2 \}, \text{C}(i, \pi') = \text{C}_i(\pi') \)，特别的，当\( \pi' = \bullet \)时，有\( \forall i \in \{ 1, 2 \}, \text{C}(i) = \text{C}_i(\bullet) \)，而\( \text{C}_i(\bullet) \)是有定义的（注：定义21.2.1的第一点），可得\( \forall i \in \{ 1, 2 \}, \text{C}(i) \)是有定义的，这和“\( \text{C}(\pi, 1) = \text{C}(1) \)未定义或\( \text{C}(\pi, 2) = \text{C}(2) \)未定义”矛盾，因此假设不成立，可得\( \text{C} \notin F(\nu F) \)，而\( \text{C} \notin F(\nu F) \)这点和 \( \nu F \)为\( F \)-consistent集合相矛盾，因此一开始的假设也不成立，有\( \text{C}(\pi, 1) \)和\( \text{C}(\pi, 2) \)均有定义，满足21.2.1的倒数第二点。
  2. 当\( n > 0 \)时：针对定义21.2.1的倒数第二点，如果\( \text{C}(\pi) = \to \)或\( \text{C}(\pi) = \times \)，我们剔除\( \text{C} \)的根节点，构造出一个新树类型候补\( \text{C}' \) （\( \text{C}' \)为\( \text{C} \)的左子树或者右子树），具体的，由\( |\pi| = n > 0 \)，可得\( |\pi| = i, \pi' \)，这里\( i = 1 \)或者\( i = 2 \)，针对\( \forall \sigma \)满足\( i, \sigma \in dom(\text{C}) \)，我们令\( \text{C}'(\sigma) = \text{C}(i, \sigma) \)，可得\( \text{C}'(\pi') = \text{C}(i, \pi') = \text{C}(\pi) = \to \text{或} \times \)，而\( |\pi'| < |\pi| = n \)，易证\( \text{C}' \in \nu F \) （这是因为\( \text{C}' \)为\( \text{C} \)的左子树或者右子树，如果\( \text{C}' \notin \nu F \)，则\( \text{C} \notin F(\nu F) \)，违反\( F \)-consistent 性质），根据归纳假设，可得\( \pi', \text{C}' \)满足定义21.2.2的倒数第二点，这意味着\( \text{C}'(\pi', 1), \text{C}'(\pi', 2) \)均有定义，进而可得\( \text{C}(\pi, 1) = \text{C}(i, \pi', 1) = \text{C}'(\pi', 1), \text{C}(\pi, 2) = \text{C}(i, \pi', 2) = \text{C}'(\pi', 2) \)均有定义，满足21.2.1的倒数第二点。

综上，归纳完毕，有\( \forall n \in \mathbf{N} \)，给定任意树类型候补\( \text{C} \in \nu F \)以及路径\( \pi \)满足\( |\pi| = n \)，则\( \text{C}, \pi \)满足定义21.2.1的后两点，这意味着\( \forall \text{C} \in \nu F \)，\( \text{C} \)满足定义21.2.1的后两点，结合上面可得\( \text{C} \)满足定义21.2.1，于是有\( \text{C} \in \mathcal{T} \)，综合可得，\( \nu F \subseteq \mathcal{T} \)。

综上，我们有\( \nu F \subseteq \mathcal{T}, \mathcal{T} \subseteq \nu F \)，可得\( \mathcal{T} = \nu F \)。

章节21.3

练习21.3.3

题目：

Check that \( \nu S \) is not the whole of \( \mathcal{T} \times \mathcal{T} \) by exhibiting a pair \( (\text{S}, \text{T}) \) that is not in \( \nu S \).

解答：

令\( \text{S} = \text{Top}, \text{T} = \text{Top} \times \text{Top} \)，则明显\( (\text{S}, \text{T}) \in \mathcal{T} \times \mathcal{T} \)，我们断言\( (\text{S}, \text{T}) \notin \nu S \)，考虑到\( \nu S \)为所有\( S \)-consistent集合的并集，因此我们只要证明\( (\text{S}, \text{T}) \)不属于任何\( S \)-consistent集合即可证明\( (\text{S}, \text{T}) \notin \nu S \)：

给定任意\( S \)-consistent集合\( X \)，假设\( (\text{S}, \text{T}) \in X \)，则根据\( S \)的定义，明显有\( (\text{S}, \text{T}) \notin S(X) \)，这是因为生成函数生成的所有新pair中，没有一个pair的第一分量是\( \text{Top} \)的，但\( (\text{S}, \text{T}) \in X, (\text{S}, \text{T}) \notin S(X) \)和\( X \)为\( S \)-consistent集合矛盾，因此假设不成立，有\( (\text{S}, \text{T}) \notin X \)。

综上，\( (\text{S}, \text{T}) \)不属于任何\( S \)-consistent集合，进而可得\( (\text{S}, \text{T}) \notin \nu S \)。

练习21.3.4

题目：

Is there a pair of types \( (\text{S}, \text{T}) \) that is related by \( \nu S \), but not by \( \mu S \)? What about a pair of types \( (\text{S}, \text{T}) \) that is related by \( \nu S_f \), but not \( \mu S_f \)?

解答：

是否\( \nu S \)中存在\( \mu S \)中没有的pair：

给定任意一个无限树类型\( \text{U} \)（比如书中Figure 21-1右侧的树类型），我们断言\( (\text{U}, \text{U}) \in \nu S, (\text{U}, \text{U}) \notin \mu S \)。

先证明\( (\text{U}, \text{U}) \in \nu S \)：

由于\( \nu S \)为所有\( S \)-consistent集合的并集，因此我们只需要证明\( (\text{U}, \text{U}) \)属于某个\( S \)-consistent集合即可。

我们首先严格定义下子树类型的概念，不过这里子树类型的定义和图论中的子树是一致的，故读者可以不看该定义，直接依赖于自己对子树的直观理解即可。

定义（子树类型）：

给定树类型\( \text{S}, \text{T} \)，我们称\( \text{S} \)为\( \text{T} \)的子树类型，当且仅当\( \exists \)前缀\( \pi' \in \{ 1, 2 \}^* \)满足：

  1. \( \text{T}(\pi') = \text{S}(\bullet) \)，即从\( \text{T} \)根节点沿着前缀路径\( \pi' \)走到的节点和\( \text{S} \)的根节点类型一样。
  2. \( \forall \pi \in \{ 1, 2 \}^* \)，我们有\( \text{T}(\pi', \pi), \text{S}(\pi) \)均未定义或者\( \text{T}(\pi', \pi) = \text{S}(\pi) \)，即两者在到达\( \text{S} \)的根节点\( \text{T}(\pi') \)之后的节点内容都是一致的。

特别的，取前缀\( \pi' \)为空字符串，则易得\( \text{T} \)是\( \text{T} \)自身的子树类型。

类似图论，容易定义\( \text{T} \)左右子树类型的概念，以及证明子树类型关系的传递性等，这里就不再深入下去了。

定义完毕。

接下来我们回去证明\( (\text{U}, \text{U}) \)属于某个\( S \)-consistent集合\( X \)：

令\( X = \{ (\text{Y}, \text{Y}) \mid \text{Y} \text{为U的子树类型} \} \)，则明显的，我们有\( (\text{U}, \text{U}) \in X \)，我们仅需要证明\( X \)为\( S \)-consistent集合即可证明\( (\text{U}, \text{U}) \in \nu S \), 而这仅需要证明\( \forall \text{Y} \)为\( \text{U} \)的子树类型，我们有\( (\text{Y}, \text{Y}) \in S(X) \)，分\( \text{Y} \)的根节点类型讨论：

  1. 如果\( \text{Y} \)的根节点为\( \text{Top} \)，则由\( S \)的定义可得\( (\text{Y}, \text{Y}) \in S(X) \)。
  2. 如果\( \text{Y} \)的根节点为\( \times \)，则令\( \text{S}_1, \text{S}_2 \)分别为\( \text{Y} \)的左右子树类型，根据定义21.2.1的第3条可得\( \text{S}_1, \text{S}_2 \)存在，易得\( \text{S}_1, \text{S}_2 \)也是\( \text{U} \)的子树类型，于是根据\( X \)的定义，可得\( (\text{S}_1, \text{S}_1) \in X, (\text{S}_2, \text{S}_2) \in X \)，进而根据\( S \)的定义可得\( (\text{Y}, \text{Y}) \in S(X) \)。
  3. 如果\( \text{Y} \)的根节点为\( \to \)，则类似\( \times \)的情况，易得\( (\text{Y}, \text{Y}) \in S(X) \)。

综上，我们证明了\( (\text{U}, \text{U}) \)属于某个\( S \)-consistent集合\( X \)，进而属于\( \nu S \)。

最后证明\( (\text{U}, \text{U}) \notin \mu S \)：

由于\( \mu S \)是所有\( S \)-closed集合的交集，因此我们只需要证明\( (\text{U}, \text{U}) \)不属于某个\( S \)-closed集合即可，令\( X = \mathcal{T} \times \mathcal{T}_f \)，则明显的有\( (\text{U}, \text{U}) \notin X \)（因为\( X \)的成员的第二分量永远会是有限树类型，而我们\( (\text{U}, \text{U}) \)的第二分量\( \text{U} \)为无限树类型），故我们仅需要证明\( X \)为\( S \)-closed集合即可证明“\( (\text{U}, \text{U}) \)不属于某个\( S \)-closed集合”，为了证明\( X \)为\( S \)-closed集合，我们需要证明\( S(X) \subseteq X \)：

\( \forall (\text{U}_1, \text{U}_2) \in S(X) \)，分情况讨论：

  1. 如果\( (\text{U}_1, \text{U}_2) \in \{ (\text{T}, \text{Top}) \mid \text{T} \in \mathcal{T} \} \)，则\( \text{U}_1 \in \mathcal{T}, \text{U}_2 = \text{Top} \in \mathcal{T}_f \)，可得\( (\text{U}_1, \text{U}_2) \in X \)。
  2. 如果\( (\text{U}_1, \text{U}_2) \in \{ (\text{S}_1 \times \text{S}_2, \text{T}_1 \times \text{T}_2) \mid (\text{S}_1, \text{T}_1), (\text{S}_2, \text{T}_2) \in X \} \)，则由\( (\text{S}_1, \text{T}_1), (\text{S}_2, \text{T}_2) \in X \)，可得\( \text{S}_1, \text{S}_2 \in \mathcal{T}, \text{T}_1, \text{T}_2 \in \mathcal{T}_f \)，进而可得\( \text{S}_1 \times \text{S}_2 \in \mathcal{T}, \text{T}_1 \times \text{T}_2 \in \mathcal{T}_f \)，这意味着\( (\text{S}_1 \times \text{S}_2, \text{T}_1 \times \text{T}_2) \in X \)。
  3. 如果\( (\text{U}_1, \text{U}_2) \in \{ (\text{S}_1 \to \text{S}_2, \text{T}_1 \to \text{T}_2) \mid (\text{S}_1, \text{T}_1), (\text{S}_2, \text{T}_2) \in X \} \)，则同上，易得\( (\text{S}_1 \to \text{S}_2, \text{T}_1 \to \text{T}_2) \in X \)。

综上，可得\( S(X) \subseteq X \)，即\( X \)为\( S \)-closed集合，而\( (\text{U}, \text{U}) \notin X \)，可得\( (\text{U}, \text{U}) \notin \mu S \)。

至此，我们得到了“是否\( \nu S \)中存在\( \mu S \)中没有的pair”的答案：存在。

是否\( \nu S_f \)中存在\( \mu S_f \)中没有的pair：

我们断言\( \mu S_f = \nu S_f \)，这意味着\( \nu S_f \)中不存在\( \mu S_f \)中没有的pair。

先证明\( \mu S_f \subseteq \nu S_f \)：

\( \mu S_f \)为最小的不动点，根据不动点的定义可得，\( \mu S_f \)也为\( S_f \)-consistent集合，进而由\( \nu S_f \)为所有\( S_f \)-consistent集合的并集，可得\( \mu S_f \subseteq \nu S_f \)。

最后证明\( \nu S_f \subseteq \mu S_f \)：

\( \forall (\text{S}, \text{T}) \in \nu S_f \)，我们要证明\( (\text{S}, \text{T}) \in \mu S_f \)，在练习21.2.2，我们定义过有限树的深度，这里直接拿来用，不再重新定义，令\( d = \max(d(\text{S}), d(\text{T})) \)，归纳假设命题对\( \forall d' = \max(d(\text{S}'), d(\text{T}')) < d \)成立，我们要证明命题对\( d \)成立：

如果\( d = 0 \)，则\( \text{S} = \text{T} = \text{Top} \)，根据\( S_f \)的定义，易得\( (\text{S}, \text{T}) \in \mu S_f \)。

如果\( d > 0 \)，则有\( d(\text{S}) > 0 \)或\( d(\text{T}) > 0 \)：

  1. 如果\( d(\text{S}) > 0 \)，则\( \text{S} = \text{S}_1 \times \text{S}_2 \) 或\( \text{S} = \text{S}_1 \to \text{S}_2 \)：
    1. 如果\( \text{S} = \text{S}_1 \times \text{S}_2 \)，则由\( (\text{S}, \text{T}) \in \nu S_f, S_f(\nu S_f) = \nu S_f \)以及\( S_f \)的定义，可得\( \text{T} = \text{Top} \)或\( \text{T} = \text{T}_1 \times \text{T}_2, (\text{S}_1, \text{T}_1) \in \nu S_f, (\text{S}_2, \text{T}_2) \in \nu S_f \)：
      1. 如果\( \text{T} = \text{Top} \)，则根据\( S_f \)的定义，易得\( (\text{S}, \text{T}) \in \mu S_f \)。
      2. 如果\( \text{T} = \text{T}_1 \times \text{T}_2, (\text{S}_1, \text{T}_1) \in \nu S_f, (\text{S}_2, \text{T}_2) \in \nu S_f \)，则由\( (\text{S}_1, \text{T}_1) \in \nu S_f, (\text{S}_2, \text{T}_2) \in \nu S_f, \max(d(\text{S}_1), d(\text{T}_1)) < d, \max(d(\text{S}_2), d(\text{T}_2)) < d \)以及归纳假设，可得\( (\text{S}_1, \text{T}_1) \in \mu S_f, (\text{S}_2, \text{T}_2) \in \mu S_f \)，进而根据\( S_f \)的定义，可得\( (\text{S}, \text{T}) \in S_f(\mu S_f) = \mu S_f \)。
    2. 如果\( \text{S} = \text{S}_1 \to \text{S}_2 \)，则同上，易得\( (\text{S}, \text{T}) \in \mu S_f \)。
  2. 如果\( d(\text{T}) > 0 \)，则\( \text{T} = \text{T}_1 \to \text{T}_2 \)，这种情况类似上面，只不过不用考虑\( \text{S} = \text{Top} \)的情况，易得\( (\text{S}, \text{T}) \in \mu S_f \)。

综上，归纳完毕，有\( \forall (\text{S}, \text{T}) \in \nu S_f, (\text{S}, \text{T}) \in \mu S_f \)，可得\( \nu S_f \subseteq \mu S_f \)。

至此，我们有\( \mu S_f \subseteq \nu S_f, \nu S_f \subseteq \mu S_f \)，可得\( \mu S_f = \nu S_f \)。

练习21.3.8

题目：

Show that the subtype relation on infinite tree types is also reflexive.

附注：

为了证明\( \nu S \)满足自反性，我们可以证明\( \forall \text{T} \in \mathcal{T}, (\text{T}, \text{T}) \in \nu S \)，而在练习21.3.4中，我们证明了给定无限树类型\( \text{U} \)，则\( (\text{U}, \text{U}) \in \nu S \)，其中证明用到了新定义的子树类型，仔细看该证明，会发现该证明并不依赖于\( \text{U} \)为无限树类型，也适用于\( \text{U} \)为有限树类型的情况，故可以直接把那边的证明搬过来，不过下面的证明我们并没有直接搬练习21.3.4的证明，而是用了新的证法。

证明：

令\( I = \{ (\text{T}, \text{T}) \mid \text{T} \in \mathcal{T} \} \)，我们只要证明\( I \)为\( S \)-consistent集合即可证明\( I \subseteq \nu S \)，而这意味着\( \nu S \)满足自反性。为了证明\( I \)为\( S \)-consistent集合，\( \forall (\text{U}, \text{U}) \in I \)，我们需要证明\( (\text{U}, \text{U}) \in S(I) \)：

  1. 如果\( \text{U} = \text{Top} \)，则直接根据\( S \)的定义，易得\( (\text{U}, \text{U}) \in S(I) \)。
  2. 如果\( \text{U} = \text{U}_1 \times \text{U}_2 \)，则由\( \text{U}_1, \text{U}_2 \in \mathcal{T} \)，可得\( (\text{U}_1, \text{U}_1), (\text{U}_2, \text{U}_2) \in I \)，进而根据\( S \)的定义可得，\( (\text{U}, \text{U}) \in S(I) \)。
  3. 如果\( \text{U} = \text{U}_1 \to \text{U}_2 \)，则类似上面，易得\( (\text{U}, \text{U}) \in S(I) \)。

证毕。

章节21.4

练习21.4.2

题目：

Suppose \( F \) is a generating function on the universe \( \mathcal{U} \times \mathcal{U} \). Show that the greatest fixed point \( \nu F^{TR} \) of the generating function \[ F^{TR}( R) = F( R) \cup TR( R) \] is the total relation on \( \mathcal{U} \times \mathcal{U} \).

证明：

由于宇集是\( \mathcal{U} \times \mathcal{U} \)，所以明显地有\( \nu F^{TR} \subseteq \mathcal{U} \times \mathcal{U} \)，故为了证明\( \nu F^{TR} = \mathcal{U} \times \mathcal{U} \)，我们仅需要证明\( \mathcal{U} \times \mathcal{U} \subseteq \nu F^{TR} \), 考虑到\( \nu F^{TR} \)为最大的\( F^{TR} \)-consistent集合，故我们仅需要证明\( \mathcal{U} \times \mathcal{U} \)为\( F^{TR} \)-consistent集合即可证明\( \mathcal{U} \times \mathcal{U} \subseteq \nu F^{TR} \)： \( \forall (\text{S}, \text{T}) \in \mathcal{U} \times \mathcal{U} \)，随便找个\( \text{U} \in \mathcal{U} \)，可得\( (\text{S}, \text{U}), (\text{U}, \text{T}) \in \mathcal{U} \times \mathcal{U} \)，进而由\( TR \)的定义，可得\( (\text{S}, \text{T}) \in TR(\mathcal{U} \times \mathcal{U}) \)，再根据\( F^{TR} \)的定义，可得\( (\text{S}, \text{T}) \in F^{TR}(\mathcal{U} \times \mathcal{U}) \)，综上，有\( \mathcal{U} \times \mathcal{U} \subseteq F^{TR}(\mathcal{U} \times \mathcal{U}) \)，这意味着\( \mathcal{U} \times \mathcal{U} \)为\( F^{TR} \)-consistent集合，根据上面的讨论，可得\( \mathcal{U} \times \mathcal{U} \subseteq \nu F^{TR} \)，加上已经有的\( \nu F^{TR} \subseteq \mathcal{U} \times \mathcal{U} \)，可得\( \nu F^{TR} = \mathcal{U} \times \mathcal{U} \)。

证毕。

章节21.5

练习21.5.2

题目：

Verify that \( S_f \) and \( S \), the generating functions for the subtyping relations from Definitions 21.3.1 and 21.3.2, are invertible, and give their support functions.

解答：

证明\( S_f \)为可逆生成函数：

\( \forall (\text{S}, \text{T}) \in \mathcal{T}_f \times \mathcal{T}_f \)，我们对\( (\text{S}, \text{T}) \)的形式进行分情况讨论：

  1. 如果\( \text{T} = \text{Top} \)，则令\( X_m = \empty \)，根据\( S_f \)的定义，我们有\( (\text{S}, \text{T}) \in F(X_m) \)，即\( X_m \in G_{(\text{S}, \text{T})} \)，除此之外，明显可得\( \forall X \in G_{(\text{S}, \text{T})}, X_m \subseteq X \)。
  2. 如果\( (\text{S}, \text{T}) = (\text{S}_1 \times \text{S}_2, \text{T}_1 \times \text{T}_2) \)，则令\( X_m = \{ (\text{S}_1, \text{T}_1), (\text{S}_2, \text{T}_2) \} \)，根据\( S_f \)的定义，可得\( (\text{S}, \text{T}) \in F(X_m) \)，即\( X_m \in G_{(\text{S}, \text{T})} \)，再根据\( S_f \)的定义，还可得\( \forall X \in G_{(\text{S}, \text{T})} \)， \( X \)均得包含\( (\text{S}_1, \text{T}_1), (\text{S}_2, \text{T}_2) \)，这意味着\( \forall X \in G_{(\text{S}, \text{T})}, X_m \subseteq X \)。
  3. 如果\( (\text{S}, \text{T}) = (\text{S}_1 \to \text{S}_2, \text{T}_1 \to \text{T}_2) \)，则令\( X_m = \{ (\text{T}_1, \text{S}_1), (\text{S}_2, \text{T}_2) \} \)，根据\( S_f \)的定义，可得\( (\text{S}, \text{T}) \in F(X_m) \)，即\( X_m \in G_{(\text{S}, \text{T})} \)，再根据\( S_f \)的定义，还可得\( \forall X \in G_{(\text{S}, \text{T})} \)， \( X \)均得包含\( (\text{T}_1, \text{S}_1), (\text{S}_2, \text{T}_2) \)，这意味着\( \forall X \in G_{(\text{S}, \text{T})}, X_m \subseteq X \)。
  4. 如果上述情况不满足，则根据\( S_f \)的定义，可得\( G_{(\text{S}, \text{T})} = \empty \)。

综上，\( S_f \)为可逆生成函数。

给出\( S_f \)的support函数：

定义\( \mathit{support}_{S_f}: \mathcal{S_f} \times \mathcal{S_f} \to \mathcal{P}(\mathcal{S_f} \times \mathcal{S_f}) \)， \( \forall (\text{S}, \text{T}) \in \mathcal{S_f} \times \mathcal{S_f} \)：

  1. 如果\( \text{T} = \text{Top} \)，则令\( \mathit{support}_{S_f}((\text{S}, \text{T})) = \empty \)。
  2. 如果\( (\text{S}, \text{T}) = (\text{S}_1 \times \text{S}_2, \text{T}_1 \times \text{T}_2) \)，则令\( \mathit{support}_{S_f}((\text{S}, \text{T})) = \{ (\text{S}_1, \text{T}_1), (\text{S}_2, \text{T}_2) \} \)。
  3. 如果\( (\text{S}, \text{T}) = (\text{S}_1 \to \text{S}_2, \text{T}_1 \to \text{T}_2) \)，则令\( \mathit{support}_{S_f}((\text{S}, \text{T})) = \{ (\text{T}_1, \text{S}_1), (\text{S}_2, \text{T}_2) \} \)。
  4. 如果上述情况不满足，则\( G_{(\text{S}, \text{T})} = \empty \)，此时令\( \mathit{support}_{S_f}((\text{S}, \text{T})) \)未定义，即\( \mathit{support}_{S_f}((\text{S}, \text{T})) = \ \uparrow \)。

证明\( S \)为可逆生成函数：

类似\( S_f \)，这里不再赘述。

给出\( S \)的support函数：

类似\( S_f \)，这里不再赘述。

练习21.5.4

题目：

Give inference rules corresponding to this function, as we did in Example 21.1.3. Check that \( E(\{ b, c \}) = \{ g, a, d \} \), that \( E(\{ a, i \}) = \{ g, h \} \), and that the sets of elements marked in the figure as \( \mu E \) and \( \nu E \) are indeed the least and the greatest fixed points of \( E \).

解答：

推导规则：

\[ \dfrac{}{g} \quad \dfrac{g}{f} \quad \dfrac{f \quad g}{c} \quad \dfrac{b}{d} \quad \dfrac{d}{e} \quad \dfrac{e}{b} \quad \dfrac{b \quad c}{a} \quad \dfrac{a \quad i}{h} \]

基础检查：

根据上面的推导规则，易得\( E(\{ b, c \}) = \{ g, a, d \}, E(\{ a, i \}) = \{ g, h \} \)。

检查最小不动点为\( \mu E = \{ c, f, g \} \)：

根据推导规则，可得\( \forall X \subseteq \mathcal{P}(\{ a, b, c, d, e, f, g, h, i \}) \)，均有\( g \in E(X) \)，再根据推导规则，为了保持\( E \)-closed性质，必须引入\( f \)元素，进而必须引入\( c \)元素，这意味着所有的\( E \)-closed集合均必须包含\( \{ c, f, g \} \)集合，进而可得所有\( E \)-closed集合的交集为\( \{ c, f, g \} \)，而\( \mu E \)为所有\( E \)-closed集合的交集，于是有\( \mu E = \{ c, f, g \} \)。

检查最大不动点为\( \nu E = \{ a, b, c, d, e, f, g \} \)：

根据推导规则，易得\( \{ a, b, c, d, e, f, g \} \)为\( E \)-consistent集合，而\( \nu E \)为最大的\( E \)-consistent集合，问题在于有没有比 \( \{ a, b, c, d, e, f, g \} \)更大的\( E \)-consistent集合了，比\( \{ a, b, c, d, e, f, g \} \)更大的集合只能再额外包含\( h, i \)中的至少一个元素，但为了保持\( E \)-consistent性质，不能额外包含\( i \)元素，不然\( i \)元素无法推导出来，会违反\( E \)-consistent性质，这意味着也不能额外包含\( h \)元素了，不然为了保持\( E \)-consistent性质，\( h \)必须得可以通过推导规则推出，而为了推出\( h \)，必须包含\( a, i \)两个元素，而前面说了不能包含\( i \)元素。综上，不能额外\( h, i \)中的任意一个元素，进而没有比\( \{ a, b, c, d, e, f, g \} \)更大的\( E \)-consistent集合，即\( \{ a, b, c, d, e, f, g \} \)为最大的\( E \)-consistent集合，于是有\( \nu E = \{ c, f, g \} \)。

练习21.5.6拓展1

题目：

Suppose \( F \) is an invertible generating function on the universe \( \mathcal{U} \). Prove that \( x \) is in the greatest fixed point of \( F \) iff no unsupported element is reachable from \( x \) in the support graph of \( F \).

附注：

书中只是提了这个性质，并没有证明，这里补上对应的证明。

证明：

必要性：

如果\( x \in \nu F \)，则我们要证明\( x \)在\( F \)的support图中不可达任何unsupported元素，这等价于证明 \( \forall x \in \nu F \)，\( \forall n \in \mathbf{N} \)，\( \forall \)路径\( x_0, x_1, \dots, x_n \)满足\( x_0 = x, x_n = u \)，均有\( u \)为supported元素，即\( x \)可达的所有元素均是supported元素，对路径的长度\( n \)进行数学归纳：

（注：即使\( \mathcal{U} \)为无限集合，任意两个元素之间的路径也还是有限的，不存在长度无限的可达路径，虽然涉及环的情况下，一个路径可以无限拓展成更长的路径，但是扩展出来的路径是一条新路径，而且长度仍然是有限的。）

当\( n = 0 \)时， \( \forall x \in \nu F \)，\( \forall \)路径\( x_0, x_1, \dots, x_n \)满足\( x_0 = x, x_n = u \)，我们得证明\( u \)为supported元素，由于路径长度为\( n = 0 \)，因此\( x = u \)，此时假设\( x = u \)为unsupported元素，这意味着\( \forall X \subseteq \mathcal{U} \)，有\( x \notin F(X) \)，进而所有\( F \)-consistent集合都不能包含\( x \)，但\( x \in \nu F \)，而\( \nu F \)为\( F \)-consistent集合，矛盾，故假设不成立，有\( x \)为supported元素。

归纳假设当\( n = k \)时命题成立，当\( n = k + 1 \)时， \( \forall x \in \nu F \)，\( \forall \)路径\( x_0, x_1, \dots, x_n \)满足\( x_0 = x, x_n = u \)，我们得证明\( u \)为supported元素，我们首先证明\( x_1 \in \nu F \)，假设\( x_1 \notin \nu F \)，则我们断言\( (x = x_0) \notin F(\nu F) \)，这是因为根据support图， \( x_1 \)存在于\( x \)的最小生成集\( \mathit{support}_{F}(x) \)中，如果\( x_1 \notin \nu F \)，则\( \mathit{support}_{F}(x) \nsubseteq \nu F\)，进而根据\( \mathit{support}_{F}(x) \)的定义，可得\( x \notin F(\nu F) \)，然而\( x \in \nu F \)，这与\( \nu F \)为\( F \)-consistent集合矛盾，因此假设不成立，有\( x_1 \in \nu F \)，由\( x_1 \in \nu F \)、路径\( x_1, x_2, \dots, x_n \)的长度为\( k \)以及归纳假设可得， \( x_n = u \)为supported元素，归纳完毕。

充分性：

如果\( x \)在\( F \)的support图中不可达任何unsupported元素，则我们要证明\( x \in \nu F \)，只需证明\( x \)存在于某个\( F \)-consistent集合即可，令\( R \)为所有\( x \)可达元素组成的集合，我们断言\( R \)为\( F \)-consistent集合，为此，我们需要证明\( R \subseteq F( R) \)： \( \forall y \in R \)，由于\( x \)不可达任何unsupported元素，这意味着\( \mathit{support}_{F}(y) \)是有定义的，根据\( \mathit{support}_{F}(y) \)以及support图的定义，可得\( \forall z \in \mathit{support}_{F}(y) \)，在support图中会有从\( y \)指向\( z \)的箭头，也就是\( y \)可达\( z \)，又\( x \)可达\( y \)，可得\( x \)可达\( z \)，从而\( z \in R \)，综上可得，\( \mathit{support}_{F}(y) \subseteq R \)，进而根据生成函数的单调性，可得\( F(\mathit{support}_{F}(y)) \subseteq F( R) \)，而\( y \in F(\mathit{support}_{F}(y)) \)，这意味着\( y \in F( R) \)。综上，我们证明了\( \forall y \in R \)有\( y \in F( R) \)，可得\( R \subseteq F( R) \)，也就是\( R \)为\( F \)-consistent集合，于是根据前面的描述，可得\( x \in \nu F \)。

证毕。

练习21.5.6拓展2

Suppose \( F \) is an invertible generating function on the universe \( \mathcal{U} \). Prove that \( x \) is not in the least fixed point of \( F \) if \( x \) participates in a cycle in the support graph of \( F \) or if there is a path from \( x \) to an element that participates in a cycle.

附注：

该练习和下面练习21.5.6阐述了但没证明的性质类似，但是我们这里并不限制\( x \in \nu F \)。

证明：

如果\( F \)的support图中存在路径\( x_0, x_1, \dots, x_n \)满足：

  1. \( n \geq 1 \)
  2. \( x_0 = x_n \)
  3. \( \exists 0 \leq i \leq n \)满足\( x_i = x \)或\( x \)在support图中可达\( x_i \)

则我们要证明\( x \notin \mu F \)：

给定任意一个\( F \)-closed集合\( X \)，如果\( X \)中存在涉及圈的节点，具体就是存在路径\( x_0, x_1, \dots, x_n \)满足：

  1. \( n \geq 1 \)
  2. \( x_0 = x_n \)
  3. \( \{ x_0, x_1, \dots, x_n \} \cap X \neq \empty \)，注意，我们不要求\( \{ x_0, x_2, \dots, x_n \} \subseteq X \)，这是因为我们仅要求\( X \)中存在 涉及 圈的节点。

令\( C = \{ x_0, x_1, \dots, x_n \} \)，令\( C^+ \)为所有可达\( C \)中某个节点的节点组成的集合，明显的，有\( C \subseteq C^+ \)，我们断言\( X \setminus C^+ \)是\( F \)-closed集合，即\( X \)在去掉涉及圈的节点后，仍然是\( F \)-closed集合，想证明这点的原因是因为\( \mu F \)是最小的\( F \)-closed集合，而如果\( X \)在去掉涉及圈的节点后，仍然是\( F \)-closed集合，则说明包含涉及圈节点的集合不会是最小的\( F \)-closed集合\( \mu F \)，进而如果\( x \)可达/涉及某个圈，则\( x \notin \mu F \)。下面我们去证明上述的命题。

由于\( X \setminus C^+ \subseteq X \)，因此根据生成函数的单调性以及\( X \)是\( F \)-closed集合，可得\( F(X \setminus C^+) \subseteq F(X) \subseteq X \)，我们想证明\( F(X \setminus C^+) \subseteq X \setminus C^+ \)，假设这点不成立，那么则有\( \exists y \in F(X \setminus C^+), y \notin X \setminus C^+ \)，由\( y \in F(X \setminus C^+), F(X \setminus C^+) \subseteq X \)，可得\( y \in X \)，加上\( y \notin X \setminus C^+ \)，可得\( y \in C^+ \)，也就是这个导致\( F \)-closed属性不成立的\( y \)出自于删除的节点集\( C^+ \)，我们考虑下\( y \)是怎么生成的，具体的，它是由\( X \setminus C^+ \)中的哪些元素以及\( F \)共同作用生成出来的？用support图的话来说，要想生成\( y \)，\( X \setminus C^+ \)必须包含所有从\( y \)出发的箭头所指向的元素，也就是必须\( \mathit{support}_{F}(y) \subseteq X \setminus C^+ \)，接下来分情况讨论：

  1. 如果\( y \notin C \)，也就是\( y \)本身不在圈\( C \)内，考虑到\( y \)可达\( C \)，那必然存在至少一个从\( y \)出发的箭头，该箭头的目标节点\( z \)可达\( C \) （不然\( y \)到不了\( C \)），当然，根据support图的定义，我们有\( z \in \mathit{support}_{F}(y) \)，由\( z \)可达\( C \)，我们有\( z \in C^+ \)，进而\( z \notin X \setminus C^+ \)，而这与\( z \in \mathit{support}_{F}(y) \)以及\( \mathit{support}_{F}(y) \subseteq X \setminus C^+ \)矛盾，故\( y \notin C \)这种情况是不可能的。
  2. 如果\( y \in C \)，也就是\( y \)本身就在圈\( C \)内，继续分情况讨论：
    1. 如果\( \exists z \in \mathit{support}_{F}(y) \)满足\( z \in C \)，则类似第1种情况，我们有\( z \in C^+ \)，进而\( z \notin X \setminus C^+ \)，而这与\( z \in \mathit{support}_{F}(y) \)以及\( \mathit{support}_{F}(y) \subseteq X \setminus C^+ \)矛盾，故该种情况不可能。
    2. 如果上一种情况不满足，即\( \forall z \in \mathit{support}_{F}(y) \)，均有\( z \notin C \)，则这种情况明显是不可能的，因为\( y \)本身在圈内，它必有箭头指向其他圈内元素，严格点说就是，由\( y \in C \)，可得\( \exist 0 \leq j \leq n \)满足\( x_j = y \)，如果\( j = n \)，则\( x_0 = x_j = x_n = y \)，此时\( x_1 \in \mathit{support}_{F}(y) \)且\( x_1 \in C \)，矛盾如果\( 0 \leq j < n \)，则\( x_{j + 1} \in \mathit{support}_{F}(y) \)且\( x_{j + 1} \in C \)，也矛盾，综上，该种情况也不可能。

综上，所有情况均不可能，矛盾，因此假设不成立，有\( F(X \setminus C^+) \subseteq X \setminus C^+ \)，即\( X \setminus C^+ \)为\( F \)-closed集合。

我们证明了任意一个\( F \)-closed集合\( X \)如果包含涉及圈的节点，则在它去掉涉及圈的节点后，仍然是\( F \)-closed集合，现在可以回去证明题目了，假设\( x \in \mu F \)，我们知道\( x \)可达某个圈\( C \)（这包括\( x \in C \)的情况），令\( C^+ \)为所有可达\( C \)中某个节点的节点组成的集合，我们有\( x \in C^+ \)，由此可得\( \mu F \setminus C^+ \subsetneq \mu F \)（真子集，重点强调两个集合不相等），再由上面证明的命题，可得\( \mu F \setminus C^+ \)是\( F \)-closed集合，但这和\( \mu F \)是最小的\( F \)-closed集合矛盾，故假设不成立，有\( x \notin \mu F \)。

证毕。

练习21.5.6拓展2的推论

Suppose \( F \) is an invertible generating function on the universe \( \mathcal{U} \). Given a \( x \in \nu F \), prove that \( x \) is not in the least fixed point of \( F \) if \( x \) participates in a cycle in the support graph of \( F \) or if there is a path from \( x \) to an element that participates in a cycle.

附注：

该推论即下面练习21.5.6阐述了但没证明的性质。

练习21.5.6

题目：

Another observation that can be made from Figure 21-2 is that an element \( x \) of \( \nu F \) is not a member of \( \mu F \) if \( x \) participates in a cycle in the support graph (or if there is a path from \( x \) to an element that participates in a cycle). Is the converse also true—that is, if \( x \) is a member of \( \nu F \) but not \( \mu F \), is it necessarily the case that \( x \) leads to a cycle?

解答：

如果在support图中\( x \)可达的边的数量是有限的，则答案是肯定的，如果\( x \)可达的边的数量是无限的，则答案是否定的，我们分别讨论。

如果在support图中\( x \)可达的边的数量是有限的：

假设\( x \)不可达任何圈，则从\( x \)出发不停顺着箭头走，每次都向之前没走过的边走（注：你可以想象我们每次走过一条边，就把这条边染成某个颜色，表示走过），由于\( x \)可达的边的数量是有限的，且我们每次都选没走过的边，因此该过程必停止，我们断言该过程最终走到的节点会为一个出度为\( 0 \)的节点\( d \) （注：\( d \)出度为\( 0 \)即没有从\( d \)出发的箭头），就像书中图21-2 中\( g \)一样，这是因为假设该过程最终走到的节点\( d \)的出度不为\( 0 \)，也就是有从\( d \)出发的箭头，那我们为什么不能继续顺着该箭头走？这是因为这条边/箭头已经走过了，易得存在从\( d \)出发，顺着箭头不停走并回到\( d \)的路径，这意味着\( d \)在一个圈内，而\( x \)可达\( d \)，进而\( x \)可达这个圈，这和\( x \)不可达任何圈矛盾，因此假设不成立，有该过程最终走到的节点\( d \)的出度为\( 0 \)。接下来我们分情况讨论：

  1. 如果\( d \)为unsupported元素，则根据上面的练习21.5.6拓展1，可得\( x \notin \nu F \)，这和\( x \in \nu F \)矛盾，故\( d \)不可能为unsupported元素。
  2. 如果上述情况不成立，即\( d \)为supported元素，则由可逆生成函数存在唯一的、对应的support图，而support图又存在唯一的、对应的一组推导规则，可得support图对应的推导规则中存在一条没有前提条件的公理性规则\( \dfrac{}{d} \) （注：这是因为\( d \)的出度为\( 0 \)，也就是support图中没有从\( d \)出发的箭头），进而所有\( F \)-closed集合必包含\( d \)，这意味着\( d \in \mu F \)。

综上，给定元素\( y \in \nu F \)且\( y \)不可达任何圈，则如果从\( y \)出发不停顺着箭头走，每次都向之前没走过的边走，则最终均会到达一个节点\( d \)满足\( d \in \mu F \)。

\( \forall z \in \mathit{support}_{F}(x) \)，令\( l_z \)为从\( x \)出发，一开始顺着箭头走向\( z \)，然后按上述过程一路走到底（注：\( z \)为\( x \)在support图中的后继，故如果\( x \)能走到底（不无限绕圈），则\( z \)也必能走到底），最长路径的长度，（注：路径不唯一，进而长度不唯一，我们取最长的），再令\( l_x = \max(\{ l_z \mid z \in \mathit{support}_{F}(x) \}) + 1 \)，我们称\( l_x \)为\( x \)的最长触底路径长度，下面对最长触底路径长度进行数学归纳，命题为：给定\( y \in \nu F \)且\( y \)不可达任何圈，我们有\( \forall n \in \mathbf{N} \)，如果\( y \)的最长触底路径长度\( l_y = n \)（即路径长度不限），则\( y \in \mu F \)。

归纳假设当\( l_y < n \)时命题成立，当\( l_y = n \)时：

  1. 如果\( l_y = n = 0 \)，则\( y \)本身出度为\( 0 \)，根据上面的讨论，可得\( y \in \mu F \)。
  2. 如果\( l_y = n > 0 \)，则\( \forall z \in \mathit{support}_{F}(y) \)，我们有\( z \)的最长触底路径长度\( l_z < l_y \)，我们再证明下\( z \in \nu F \)就可以使用归纳假设了（注：\( z \)不可达任何圈，否则\( y \)会可达某个圈，矛盾)，由\( y \in \nu F \)，可得\( y \)存在于某个\( F \)-consistent集合\( Y \)中，有\( y \in F(Y) \)，这意味着\( Y \)必须包含所有\( \mathit{support}_{F}(y) \)中的元素，即\( \mathit{support}_{F}(y) \subseteq Y \)，而\( z \in \mathit{support}_{F}(y) \)，可得\( z \in Y \)，进而可得\( z \in \nu F \)，此时可以使用归纳假设了，根据归纳假设可得，\( z \in \mu F \)。综上，我们有\( \forall z \in \mathit{support}_{F}(y), z \in \mu F \)，可得\( y \in F(\mu F) \)，进而由\( \mu F \)为\( F \)-closed集合可得， \( y \in \mu F \)。

归纳完毕，我们有给定\( y \in \nu F \)且\( y \)不可达任何圈， \( \forall n \in \mathbf{N} \)，如果\( y \)的最长触底路径长度\( l_y = n \)，则\( y \in \mu F \)，特别的，我们有\( x \in \mu F \)，而\( x \in \mu F \)与\( x \notin \mu F \)矛盾，因此假设不成立，有\( x \)可达某个圈。

如果在support图中\( x \)可达的边的数量是无限的：

此时\( x \)可以做到不可达任何圈，关键在于构造可以无限往下走的路线，令\( \mathcal{U} = \mathbf{N} \)，令\( F(X) = \{ 0 \} \cup \{ n \mid n + 1 \in X \} \)，则易得\( \mu F = \{ 0 \}, \nu F = \mathbf{N} \)，而针对\( \forall n \in \nu F \setminus \mu F \)（也就是\( \forall n > 0 \)），易得\( \mathit{support}_{F}(n) = \{ n + 1 \} \)，这意味着在support图中，\( \forall n > 0 \)对应的节点都有指向\( n + 1 \)的箭头，可以顺着该箭头无限往下走，永远不会到达某个圈。

练习21.5.13

题目：

Suppose \( F \) is an invertible generating function. Define the function \( \mathit{lfp}_F \) (or just \( \mathit{lfp} \)) as follows:

\[ \begin{aligned} \mathit{lfp}_F(X) = \ &\text{if } \mathit{support}_F(X) \uparrow \text{, then false} \\ &\text{else if } X = \empty \text{, then true} \\ &\text{else } \mathit{lfp}_F(\mathit{support}_F(X)) \end{aligned} \]

Intuitively, \( \mathit{lfp}_F \) works by starting with a set \( X \) and using the support relation to reduce it until it becomes empty. Prove that this algorithm is partially correct, in the sense that

  1. If \( \mathit{lfp}_F(X) = \text{true} \), then \( X \subseteq \mu F \).
  2. If \( \mathit{lfp}_F(X) = \text{false} \), then \( X \nsubseteq \mu F \).

Can you find a class of generating functions for which \( \mathit{lfp}_F \) is guaranteed to terminate on all finite inputs?

附注：

注意到该算法无法正确处理涉及圈的情况，具体的，如果\( \exists x \in X \)，\( x \)可达某个圈，则算法有可能不终止，一直在support图中绕圈，比如针对书上图21-2，令\( X = \{ b \} \)，则算法无法终止，然而根据我们上面的练习21.5.6拓展2，可得\( b \notin \mu F \)，然而该算法无法得出该结论。

解答：

证明如果算法终止，则结果一定是正确的：

给定任意宇集\( \mathcal{U} \)的子集\( X \)，如果\( \mathit{lfp}_F(X) = \text{true} \)，即算法终止且返回结果为\( \text{true} \)，代表着算法认定\( X \subseteq \mu F \)，则我们要证明确实\( X \subseteq \mu F \)，同理，如果\( \mathit{lfp}_F(X) = \text{false} \)，则我们得证明\( X \nsubseteq \mu F \)。

我们证明命题：给定任意宇集\( \mathcal{U} \)的子集\( X \)满足\( \mathit{lfp}_F(X) \)终止，则：

  1. 如果\( \mathit{lfp}_F(X) = \text{true} \)，我们断言\( X \subseteq \mu F \)。
  2. 如果\( \mathit{lfp}_F(X) = \text{false} \)，我们断言\( X \nsubseteq \mu F \)。

由于\( \mathit{lfp}_F(X) \)终止，故\( \mathit{lfp}_F(X) \)的递归调用深度必是有限的，为正整数（注：由于至少会调用一次，故深度\( \geq 1 \)，不会为\( 0 \)，所以说是正整数，而不是自然数），这意味着我们可以换一种方式表述命题，便于使用数学归纳法，以递归调用深度作为termination measure，具体的，上述命题等价于：

\( \forall d \geq 1 \in \mathbf{N} \)， \( \forall X \subseteq \mathcal{U} \)满足\( \mathit{lfp}_F(X) \)终止且\( \mathit{lfp}_F(X) \)递归调用深度为\( d \)，我们有：

  1. 如果\( \mathit{lfp}_F(X) = \text{true} \)，则\( X \subseteq \mu F \)。
  2. 如果\( \mathit{lfp}_F(X) = \text{false} \)，则\( X \nsubseteq \mu F \)。

对递归调用深度\( d \)进行数学归纳：

当\( d = 1 \)时，递归调用深度为\( 1 \)，此时算法必直接返回，只有两种可能，要么\( \mathit{support}_F(X) \uparrow \)，算法返回\( \text{false} \)，要么\( X = \empty \)，算法返回\( \text{true} \)，我们分别讨论两种情况：

  1. 如果\( \mathit{support}_F(X) \uparrow \)，此时算法返回\( \text{false} \)，根据引理21.5.8，我们有\( X \nsubseteq \mu F \)，也就是说算法此时返回\( \text{false} \)是对的。
  2. 如果\( X = \empty \)，此时算法返回\( \text{true} \)，而\( (X = \empty) \subseteq \mu F \)，故算法此时返回\( \text{true} \)也是对的。

归纳假设当\( d = k \)时命题成立，当\( d = k + 1 \)时，分情况讨论：

  1. 如果\( \mathit{lfp}_F(X) = \text{true} \)，此时这个结果\( \text{true} \)必是由\( \text{else if} \)或\( \text{else} \)分支返回的，继续分情况讨论：
    1. 如果结果是由\( \text{else if} \)分支返回的，此时有\( X = \empty \)，则\( (X = \empty) \subseteq \mu F \)，故算法此时返回\( \text{true} \)是对的。
    2. 如果结果是由\( \text{else} \)分支返回的，此时有\( \mathit{lfp}_F(\mathit{support}_F(X)) = \text{true} \)，由于\( \mathit{lfp}_F(\mathit{support}_F(X)) \)的递归调用深度\( d' \)为 \( \mathit{lfp}_F(X) \)的递归调用深度\( d - 1 \)，我们有\( d' = d - 1 = k \)，可以使用归纳假设，根据归纳假设，我们有\( \mathit{support}_F(X) \subseteq \mu F \)，此时根据引理21.5.8，可得\( X \subseteq \mu F \)，故算法此时返回\( \text{true} \)也是对的。
  2. 如果\( \mathit{lfp}_F(X) = \text{false} \)，此时这个结果\( \text{false} \)必是由\( \text{if} \)或\( \text{else} \)分支返回的，继续分情况讨论：
    1. 如果结果是由\( \text{if} \)分支返回的，此时有\( \mathit{support}_F(X) \uparrow \)，则由引理21.5.8，可得\( X \nsubseteq \mu F \)，故算法此时返回\( \text{false} \)是对的。
    2. 如果结果是由\( \text{else} \)分支返回的，此时有\( \mathit{lfp}_F(\mathit{support}_F(X)) = \text{false} \)，根据归纳假设，我们有\( \mathit{support}_F(X) \nsubseteq \mu F \)，此时根据引理21.5.8，可得\( X \nsubseteq \mu F \)，故算法此时返回\( \text{false} \)也是对的。

综上，归纳完毕，命题成立，如果算法终止，则结果一定是正确的。

证毕。

生成函数满足哪些性质能保证\( \mathit{lfp}_F \)对所有有限输入都终止：

只要保证\( \forall x \in \mathcal{U} \)，\( x \)不可达任何圈且\( x \)可达的 边 的数量是有限的就行。

或者换句话来说，只要保证\( \forall x \in \mathcal{U} \)，\( x \)不可达任何圈且\( \mathit{reachable}(x) \)有限即可。

根据定义21.5.11进一步简化就是，只要保证\( F \)有限状态且\( \forall x \in \mathcal{U} \)，\( x \)不可达任何圈即可。

章节21.8

练习21.8.5

题目：

Write down the function \( S_d \) mentioned above, and demonstrate that it is not invertible. Prove that \( \nu S_d = \nu S_m \).

解答：

声明式生成函数\( S_d \)的定义：

把最后一个分支的限制条件去掉就行了，如下：

\[ \begin{aligned} S_d( R) &= \{ (\text{S}, \text{Top}) \mid \text{S} \in \mathcal{T}_m \} \\ &\cup \{ (\text{S}_1 \times \text{S}_2, \text{T}_1 \times \text{T}_2) \mid (\text{S}_1, \text{T}_1), (\text{S}_2, \text{T}_2) \in R \} \\ &\cup \{ (\text{S}_1 \to \text{S}_2, \text{T}_1 \to \text{T}_2) \mid (\text{S}_1, \text{T}_1), (\text{S}_2, \text{T}_2) \in R \} \\ &\cup \{ (\text{S}, \mu \text{X. } \text{T}) \mid (\text{S}, [\text{X} \mapsto \mu \text{X. } \text{T}] \text{T}) \in R \} \\ &\cup \{ (\mu \text{X. } \text{S}, \text{T}) \mid ([\text{X} \mapsto \mu \text{X. } \text{S}] \text{S}, \text{T}) \in R \} \end{aligned} \]

证明\( S_d \)非可逆生成函数：

根据\( S_d \)的定义，可得\( (\mu \text{X. } \text{Top}, \mu \text{Y. } \text{Top}) \)有两个生成集\( \{ (\mu \text{X. } \text{Top}, \text{Top}) \} \)（使用倒数第二个分支）、 \( \{ (\text{Top}, \mu \text{Y. } \text{Top}) \} \)（使用最后一个分支），这两个生成集互相不是对方的子集，从而\( G_{(\mu \text{X. } \text{Top}, \mu \text{Y. } \text{Top})} \)中不存在一个最小的生成集，于是\( \mathit{support}_{S_d}((\mu \text{X. } \text{Top}, \mu \text{Y. } \text{Top})) \)未定义，可得\( S_d \)不可逆。

证毕。

证明\( \nu S_d = \nu S_m \)：

这里把\( S_m \)的定义搬过来，方便看：

\[ \begin{aligned} S_m( R) &= \{ (\text{S}, \text{Top}) \mid \text{S} \in \mathcal{T}_m \} \\ &\cup \{ (\text{S}_1 \times \text{S}_2, \text{T}_1 \times \text{T}_2) \mid (\text{S}_1, \text{T}_1), (\text{S}_2, \text{T}_2) \in R \} \\ &\cup \{ (\text{S}_1 \to \text{S}_2, \text{T}_1 \to \text{T}_2) \mid (\text{S}_1, \text{T}_1), (\text{S}_2, \text{T}_2) \in R \} \\ &\cup \{ (\text{S}, \mu \text{X. } \text{T}) \mid (\text{S}, [\text{X} \mapsto \mu \text{X. } \text{T}] \text{T}) \in R \} \\ &\cup \{ (\mu \text{X. } \text{S}, \text{T}) \mid ([\text{X} \mapsto \mu \text{X. } \text{S}] \text{S}, \text{T}) \in R, \text{T} \neq \text{Top} \text{, and } \text{T} \neq \mu \text{Y. } \text{T}_1 \} \end{aligned} \]

我们需要证明\( \nu S_d \subseteq \nu S_m \)以及\( \nu S_m \subseteq \nu S_d \)：

先证明\( \nu S_m \subseteq \nu S_d \)：

由于\( S_d \)和\( S_m \)的定义基本一致，只是\( S_m \)的最后一个分支多了个限制，故所有\( S_m \)-consistent集合一定是\( S_d \)-consistent集合，而\( \nu S_m \)是\( S_m \)-consistent集合，可得\( \nu S_m \)是\( S_d \)-consistent集合，而\( \nu S_d \)是最大的\( S_d \)-consistent集合，可得\( \nu S_m \subseteq \nu S_d \)。

接着证明\( \nu S_d \subseteq \nu S_m \)：

由于\( \nu S_m \)是最大的\( S_m \)-consistent集合，故我们只需要证明\( \nu S_d \)是\( S_m \)-consistent集合，即可证明\( \nu S_d \subseteq \nu S_m \)，而为了证明\( \nu S_d \)是\( S_m \)-consistent集合，我们得证明\( \forall (\text{S}, \text{T}) \in \nu S_d \)，有\( (\text{S}, \text{T}) \in S_m(\nu S_d) \)：

\( \forall (\text{S}, \text{T}) \in \nu S_d \)，使用字典归纳法（公理2.4.4）来证明，令\( m = \mu \textit{-height}(\text{S}), n = \mu \textit{-height}(\text{T}) \)，归纳假设\( \forall (m', n') < (m, n) \)，如果\( (\text{S}', \text{T}') \in \nu S_d, \mu \textit{-height}(\text{S}') = m', \mu \textit{-height}(\text{T}') = n' \)，则\( (\text{S}', \text{T}') \in S_m(\nu S_d) \)，我们要证明\( (\text{S}, \text{T}) \in S_m(\nu S_d) \)，由\( \nu S_d \)是\( S_d \)-consistent集合，可得\( (\text{S}, \text{T}) \in S_d(\nu S_d) \)，这意味着\( (\text{S}, \text{T}) \)可由\( S_d \)定义中的五条分支中的至少一条分支生成，下面分情况讨论：

  1. 如果\( (\text{S}, \text{T}) \)可由\( S_d \)的分支1，即\( \{ (\text{S}, \text{Top}) \mid \text{S} \in \mathcal{T}_m \} \)生成，则可得\( \text{T} = \text{Top} \)，再由\( S_m \)的分支1，可得\( (\text{S}, \text{T}) \in S_m(\nu S_d) \)。
  2. 如果\( (\text{S}, \text{T}) \)可由\( S_d \)的分支2，即\( \{ (\text{S}_1 \times \text{S}_2, \text{T}_1 \times \text{T}_2) \mid (\text{S}_1, \text{T}_1), (\text{S}_2, \text{T}_2) \in R \} \)生成，则\( \text{S} = \text{S}_1 \times \text{S}_2, \text{T} = \text{T}_1 \times \text{T}_2, (\text{S}_1, \text{T}_1), (\text{S}_2, \text{T}_2) \in \nu S_d \)，再由\( S_m \)的分支2，可得\( (\text{S}, \text{T}) \in S_m(\nu S_d) \)。
  3. 如果\( (\text{S}, \text{T}) \)可由\( S_d \)的分支3，即\( \{ (\text{S}_1 \to \text{S}_2, \text{T}_1 \to \text{T}_2) \mid (\text{T}_1, \text{S}_1), (\text{S}_2, \text{T}_2) \in R \} \)生成，则\( \text{S} = \text{S}_1 \to \text{S}_2, \text{T} = \text{T}_1 \to \text{T}_2, (\text{T}_1, \text{S}_1), (\text{S}_2, \text{T}_2) \in \nu S_d \)，再由\( S_m \)的分支3，可得\( (\text{S}, \text{T}) \in S_m(\nu S_d) \)。
  4. 如果\( (\text{S}, \text{T}) \)可由\( S_d \)的分支4，即\( \{ (\text{S}, \mu \text{X. } \text{T}) \mid (\text{S}, [\text{X} \mapsto \mu \text{X. } \text{T}] \text{T}) \in R \} \)生成，则\( \text{T} = \mu \text{X. } \text{T}_1, (\text{S}, [\text{X} \mapsto \mu \text{X. } \text{T}_1] \text{T}_1) \in \nu S_d \)，再由\( S_m \)的分支4，可得\( (\text{S}, \text{T}) \in S_m(\nu S_d) \)。
  5. 如果\( (\text{S}, \text{T}) \)可由\( S_d \)的分支5，即\( \{ (\mu \text{X. } \text{S}, \text{T}) \mid ([\text{X} \mapsto \mu \text{X. } \text{S}] \text{S}, \text{T}) \in R \} \)生成，则\( \text{S} = \mu \text{X. } \text{S}_1, ([\text{X} \mapsto \mu \text{X. } \text{S}_1] \text{S}_1, \text{T}) \in \nu S_d \)，此时若\( \text{T} \neq \text{Top} \)且\( \text{T} \neq \mu \text{Y. } \text{T}_1 \)，则由\( S_m \)的分支5，可得\( (\text{S}, \text{T}) \in S_m(\nu S_d) \)，还需考虑\( \text{T} = \text{Top} \)或\( \text{T} = \mu \text{Y. } \text{T}_1 \)的情况，继续分情况讨论：
    1. 如果\( \text{T} = \text{Top} \)，则由\( S_m \)的分支1，可得\( (\text{S}, \text{T}) \in S_m(\nu S_d) \)。
    2. 如果\( \text{T} = \mu \text{Y. } \text{T}_1 \)，此时由于\( S_m \)的分支5不允许\( \text{T} \)是fold后的类型，故我们需要在\( \text{T} \)没有被fold之前（注：\( \text{T} \)没被fold之前是另外一个unfold类型，这里用\( \text{T} \)指代该类型仅是为了方便表述），使用\( S_m \)的分支5去fold类型\( \text{S} \)（注：\( \text{S} \)没被fold之前是另外一个unfold类型，这里用\( \text{S} \)指代该类型仅是为了方便表述），直到\( \text{S} \)被fold成现在的类型，再使用\( S_m \)的分支4来fold类型\( \text{T} \)，直到\( \text{T} \)被fold成现在的类型，注意，在\( \text{S} \)没被fold成现在的类型之前，\( \text{T} \)一次都不能被fold，不然直接不能用\( S_m \)的分支5，最终也就不能生成\( (\text{S}, \text{T}) = (\text{S}, \mu \text{Y. } \text{T}_1) \)了，故可得思路：令\( \text{T}_u \)为\( \text{T} \)完全unfold的类型，也就是不停unfold类型\( \text{T} \)，直到\( \text{T} \)前面没有\( \mu \)-绑定，\( \mu \textit{-height} \)为\( 0 \)，得到的就是\( \text{T}_u \)，由于\( \mu \textit{-height}(\text{T}) \)有限且\( \text{T} \)是contractive的（定义21.8.2），故不会出现无限unfold但\( \mu \textit{-height} \)却降不到\( 0 \)的情况，同理可得到\( \text{S} \)完全unfold后的类型\( \text{S}_u \)，我们希望证明\( (\text{S}_u, \text{T}_u) \in \nu S_d \)，然后不停地利用\( S_d \)的分支5以及\( S_d(\nu S_d) = \nu S_d \)以证明\( (\text{S}, \text{T}_u) \in \nu S_d \)，接着不停地利用\( S_d \)的分支4以及\( S_d(\nu S_d) = \nu S_d \)以证明\( (\text{S}, [\text{Y} \mapsto \mu \text{Y. } \text{T}_1] \text{T}_1) \in \nu S_d \)，最终利用\( S_m \)的分支4以证明\( (\text{S}, \text{T}) \in S_m(\nu S_d) \)，思路说明完毕，但我们用的归纳法来证明，故实际过程会有些差异，不过思路、目标是一致的。现在继续回去证明：由于\( \mu \textit{-height}([\text{X} \mapsto \mu \text{X. } \text{S}_1] \text{S}_1) = m - 1 < m \)，于是有\( (m - 1, n) < (m, n) \)，再由\( ([\text{X} \mapsto \mu \text{X. } \text{S}_1] \text{S}_1, \text{T}) \in \nu S_d \)以及归纳假设，可得\( ([\text{X} \mapsto \mu \text{X. } \text{S}_1] \text{S}_1, \text{T}) \in S_m(S_d) \)，即\( ([\text{X} \mapsto \mu \text{X. } \text{S}_1] \text{S}_1, \text{T}) \)可由\( S_m \)作用于\( S_d \)生成，由于\( S_m \)定义的前三个分支最终生成的关系对的\( \mu \)-深度均为\( 0 \)，而\( \mu \textit{-height}(\text{T}) = n > 0 \)，可得\( ([\text{X} \mapsto \mu \text{X. } \text{S}_1] \text{S}_1, \text{T}) \)不能由\( S_m \)定义的前三个分支生成，加上\( \text{T} = \mu \text{Y. } \text{T}_1 \)，不满足\( S_m \)分支5的限制条件，可得\( ([\text{X} \mapsto \mu \text{X. } \text{S}_1] \text{S}_1, \text{T}) \)必由\( S_m \)的分支4生成，于是可得\( ([\text{X} \mapsto \mu \text{X. } \text{S}_1] \text{S}_1, [\text{Y} \mapsto \mu \text{Y. } \text{T}_1] \text{T}_1) \in \nu S_d \)，再由\( S_d \)的分支5，可得\( (\text{S}, [\text{Y} \mapsto \mu \text{Y. } \text{T}_1] \text{T}_1) \in S_d(\nu S_d) = \nu S_d \)，此时由\( S_m \)的分支4，可得\( (\text{S}, \text{T}) \in S_m(\nu S_d) \)。

综上，归纳完毕，命题成立，有\( \forall (\text{S}, \text{T}) \in \nu S_d, (\text{S}, \text{T}) \in S_m(\nu S_d) \)，即\( \nu S_d \)是\( S_m \)-consistent集合，而\( S_m \)为最大的\( S_m \)-consistent集合，可得\( \nu S_d \subseteq \nu S_m \)。

至此，我们证明了\( \nu S_m \subseteq \nu S_d, \nu S_d \subseteq \nu S_m \)，可得\( \nu S_d = \nu S_m \)。

证毕。

章节21.9

练习21.9.2

题目：

Give an equivalent definition of the relation \( \text{S} \sqsubseteq \text{T} \) as a set of inference rules.

解答：

\[ \dfrac{}{\text{T} \sqsubseteq \text{T}} \]

\[ \dfrac{\text{S} \sqsubseteq \text{T}_1}{\text{S} \sqsubseteq \text{T}_1 \times \text{T}_2} \]

\[ \dfrac{\text{S} \sqsubseteq \text{T}_2}{\text{S} \sqsubseteq \text{T}_1 \times \text{T}_2} \]

\[ \dfrac{\text{S} \sqsubseteq \text{T}_1}{\text{S} \sqsubseteq \text{T}_1 \to \text{T}_2} \]

\[ \dfrac{\text{S} \sqsubseteq \text{T}_2}{\text{S} \sqsubseteq \text{T}_1 \to \text{T}_2} \]

\[ \dfrac{\text{S} \sqsubseteq [\text{X} \mapsto \mu \text{X. } \text{T}] \text{T}}{\text{S} \sqsubseteq \mu \text{X. } \text{T}} \]

练习21.9.7

题目：

Give an equivalent definition of the relation \( \text{S} \preceq \text{T} \) as a set of inference rules.

解答：

\[ \dfrac{}{\text{T} \preceq \text{T}} \]

\[ \dfrac{\text{S} \preceq \text{T}_1}{\text{S} \preceq \text{T}_1 \times \text{T}_2} \]

\[ \dfrac{\text{S} \preceq \text{T}_2}{\text{S} \preceq \text{T}_1 \times \text{T}_2} \]

\[ \dfrac{\text{S} \preceq \text{T}_1}{\text{S} \preceq \text{T}_1 \to \text{T}_2} \]

\[ \dfrac{\text{S} \preceq \text{T}_2}{\text{S} \preceq \text{T}_1 \to \text{T}_2} \]

\[ \dfrac{\text{S} \preceq \text{T}}{[\text{X} \mapsto \mu \text{X. } \text{T}] \text{S} \preceq \mu \text{X. } \text{T}} \]

章节21.11

练习21.11.1

题目：

Find recursive types \( \text{S} \) and \( \text{T} \) such that \( \text{S} <: \text{T} \) using the equi-recursive definition, but not using the Amber rule.

解答：

一个最简单的例子，考虑类型\( \text{T} = \mu \text{X. } \text{T}_1 \)，这里\( \text{T}_1 \)可以代入任意具体类型，比如\( \text{T}_1 = \text{Nat} \)，则\( \text{T} = \mu \text{X. } \text{Nat} \)，我们展开一次\( \mu \)-绑定，便得到了类型\( \text{S} = [\text{X} \mapsto \mu \text{X. } \text{T}_1] \text{T}_1 \)，在equi-recursive定义下，一个表达式的任意展开都与其本身等价（不管在哪里展开\( \text{X} \)，展开多少次，都没有关系），故\( \text{S} \)等价于\( \text{T} \)（不仅仅是子类型，是完全等价），进而在equi-recursive定义下有\( \text{S} <: \text{T} \)，而考虑S-AMBER规则，如下：

\[ \dfrac{\Sigma, \text{X} <: \text{Y} \vdash \text{S} <: \text{T}}{\Sigma \vdash \mu \text{X. } \text{S} <: \mu \text{Y. } \text{T}} \qquad \text{S-AMBER} \]

可以看到，针对涉及\( \mu \)-绑定的类型，它要求子类型关系的双方都得是\( \mu \)-绑定类型，进而易证如果两个类型\( \text{S} <: \text{T} \)，则必须有\( \mu \mathit{-height}(\text{S}) = \mu \mathit{-height}(\text{T}) \)，不然如果两者\( \mu \mathit{-height} \)不一样的话，不断展开，必有一方\( \mu \mathit{-height} \)先变成\( 0 \)，另一方则还没变成\( 0 \)，即不断展开后的其中一方前面/顶部没有\( \mu \)-绑定，另一方则前面/顶部有\( \mu \)-绑定，这种情况不符合S-AMBER的使用规则，而使用S-AMBER规则的类型系统的其他规则（处理\( \times, \to \)等的规则）也不能处理含\( \mu \)-绑定的类型，因此\( \mu \mathit{-height} \)必须相等，而针对上面给出的类型\( \text{S}, \text{T} \)，有\( \mu \mathit{-height}(\text{S} = [\text{X} \mapsto \mu \text{X. } \text{T}_1] \text{T}_1) < \mu \mathit{-height}(\text{T} = \mu \text{X. } \text{T}_1) \)，可得在该类型系统下有\( \text{S} \nless: \text{T} \)。

另外一个例子，令\( \text{S} = \mu \text{X. } \text{T}_1 \times \text{X}, \text{T} = \mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X}) \)，这里同上，\( \text{T} \)可以代入任意具体类型（比如\( \text{Nat} \)），这里直观上，两者无限展开的结果都是\( \text{T}_1 \times (\text{T}_1 \times (\text{T}_1 \times \dots) \dots) \)，故直观上，两者等价，进而在equi-recursive定义下，应该有\( \text{S} <: \text{T} \)，严格点来说，考虑沿着\( \mathit{support}_{S_m} \)图走，其边由\( \mathit{support}_{S_m} \)定义，有：

\[ \begin{aligned} &\mathit{support}_{S_m}((\text{S}, \text{T})) \\ &= \{ (\text{S}, [\text{X} \mapsto \mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X})] (\text{T}_1 \times (\text{T}_1 \times \text{X}))) \} \\ &= \{ (\text{S}, \text{T}_1 \times (\text{T}_1 \times (\mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X})))) \} \end{aligned} \]

进一步沿着\( \mathit{support}_{S_m} \)图走，有：

\[ \begin{aligned} &\mathit{support}_{S_m}((\text{S}, \text{T}_1 \times (\text{T}_1 \times (\mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X}))))) \\ &= \{ ([\text{X} \mapsto \mu \text{X. } \text{T}_1 \times \text{X}] (\text{T}_1 \times \text{X}), \text{T}_1 \times (\text{T}_1 \times (\mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X})))) \} \\ &= \{ (\text{T}_1 \times (\mu \text{X. } \text{T}_1 \times \text{X}), \text{T}_1 \times (\text{T}_1 \times (\mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X})))) \} \end{aligned} \]

再进一步沿着\( \mathit{support}_{S_m} \)图走，有：

\[ \begin{aligned} &\mathit{support}_{S_m}(\{ (\text{T}_1 \times (\mu \text{X. } \text{T}_1 \times \text{X}), \text{T}_1 \times (\text{T}_1 \times (\mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X})))) \}) \\ &= \{ (\text{T}_1, \text{T}_1), (\mu \text{X. } \text{T}_1 \times \text{X}, \text{T}_1 \times (\mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X}))) \} \end{aligned} \]

这里\( (\text{T}_1, \text{T}_1) \)即\( \text{T}_1 <: \text{T}_1 \)是显然成立的，故进一步需要检查\( (\mu \text{X. } \text{T}_1 \times \text{X}, \text{T}_1 \times (\mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X}))) \)，有：

\[ \begin{aligned} &\mathit{support}_{S_m}((\mu \text{X. } \text{T}_1 \times \text{X}, \text{T}_1 \times (\mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X})))) \\ &= \{ ([\text{X} \mapsto \mu \text{X. } \text{T}_1 \times \text{X}] (\text{T}_1 \times \text{X}), \text{T}_1 \times (\mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X}))) \} \\ &= \{ (\text{T}_1 \times (\mu \text{X. } \text{T}_1 \times \text{X}), \text{T}_1 \times (\mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X}))) \} \end{aligned} \]

进一步检查\( (\text{T}_1 \times (\mu \text{X. } \text{T}_1 \times \text{X}), \text{T}_1 \times (\mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X}))) \)，有：

\[ \begin{aligned} &\mathit{support}_{S_m}((\text{T}_1 \times (\mu \text{X. } \text{T}_1 \times \text{X}), \text{T}_1 \times (\mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X})))) \\ &= \{ (\text{T}_1, \text{T}_1), (\mu \text{X. } \text{T}_1 \times \text{X}, \mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X})) \} \end{aligned} \]

同上，\( (\text{T}_1, \text{T}_1) \)是显然成立的，而\( (\mu \text{X. } \text{T}_1 \times \text{X}, \mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X})) = (\text{S}, \text{T}) \)是我们在\( \mathit{support}_{S_m} \)图中已经走过的节点，按书中Figure 21-4中算法的话来说就是， \( (\mu \text{X. } \text{T}_1 \times \text{X}, \mu \text{X. } \text{T}_1 \times (\text{T}_1 \times \text{X})) = (\text{S}, \text{T}) \)已经在已知的assumption，即第一个参数\( A \)中了，直接有\( (\text{S}, \text{T}) \)成立。

综上可得，在equi-recursive定义下，有\( \text{S} <: \text{T} \)。

接着考虑S-AMBER规则，为了方便区分，我们改下\( \text{T} \)的类型变量名，令\( \text{T} = \mu \text{Y. } \text{T}_1 \times (\text{T}_1 \times \text{Y})\)，要证明\( \Sigma \vdash \text{S} <: \text{T} \)，我们需要证明：

\[ \Sigma, \text{X} <: \text{Y} \vdash \text{T}_1 \times \text{X} <: \text{T}_1 \times (\text{T}_1 \times \text{Y}) \]

进一步的，我们需要证明：

\[ \begin{aligned} &\Sigma, \text{X} <: \text{Y} \vdash \text{T}_1 <: \text{T}_1 \\ &\Sigma, \text{X} <: \text{Y} \vdash \text{X} <: \text{T}_1 \times \text{Y} \end{aligned} \]

上面\( \Sigma, \text{X} <: \text{Y} \vdash \text{T}_1 <: \text{T}_1 \)显然成立，但是针对\( \Sigma, \text{X} <: \text{Y} \vdash \text{X} <: \text{T}_1 \times \text{Y} \)，这里左侧的\( \text{X} \)是类型变量，而右侧的\( \text{T}_1 \times \text{Y} \)则是\( \times \)类型，没有匹配的子类型规则，可得\( \Sigma, \text{X} <: \text{Y} \vdash \text{X} \nless: \text{T}_1 \times \text{Y} \)。

综上可得，在使用S-AMBER规则的类型系统下，有\( \text{S} \nless: \text{T} \)。

参考文章

  1. Is Dictionary order on \( \mathbf{N} \times \mathbf{N} \) a well order?
更新于 2023-04-05
 数学, 类型理论
返回 | 主页