Types and Programming Languages习题的参考解答及思考（第2章）
第2章
章节2.2
练习2.2.6
题目：
Suppose we are given a relation \( R \) on a set \( S \). Define the relation \( R' \) as follows:
\[ R' = R \cup \{ (s, s) \mid s \in S \} \text{.} \]
That is, \( R' \) contains all the pairs in \( R \) plus all pairs of the form \( (s, s) \). Show that \( R' \) is the reflexive closure of \( R \).
证明：
根据\( R' \)的定义，有\( R \subseteq R' \) 且\( R' \)满足自反性。
令\( R'' \)为任意包含\( R \)且满足自反性的\( S \)上的关系，则\( \forall (a, b) \in R' \)，有\( (a, b) \in R \)或\( (a, b) \in \{ (s, s) \mid s \in S \} \)，分情况讨论：
- 如果\( (a, b) \in R \)，则由于\( R'' \)包含\( R \)，因此\( (a, b) \in R'' \)。
- 如果\( (a, b) \in \{ (s, s) \mid s \in S \} \)，则\( a = b, (a, b) = (a, a) \)，又由于\( R'' \)满足自反性，因此\( (a, b) = (a, a) \in R'' \)。
综上，有\( R' \subseteq R'' \)，加上前面证明的\( R' \)包含\( R \)且满足自反性，可得\( R' \)为\( R \)的自反闭包。
证毕。
练习2.2.7
题目：
Here is a more constructive definition of the transitive closure of a relation \( R \). First, we define the following sequence of sets of pairs:
\[ R_0 = R \] \[ R_{i + 1} = R_i \cup \{ (s, u) \mid \text{ for some } t, (s, t) \in R_i \text{ and } (t, u) \in R_i \} \]
That is, we construct each \( R_{i + 1} \) by adding to \( R_i \) all the pairs that can be obtained by “one step of transitivity” from pairs already in \( R_i \). Finally, define the relation \( R^+ \) as the union of all the \( R_i \):
\[ R^+ = \bigcup_i R_i \]
Show that this \( R^+ \) is really the transitive closure of R — i.e., that it satisfies the conditions given in Definition 2.2.5.
证明：
包含：根据定义，\( R = R_0 \subseteq R^+ \)。
传递性：证明传递性之前，注意到，由\( R_{i + 1} \)的定义，用数学归纳法，易得\( \forall j \geq i \in \mathbf{N} \)，有\( R_i \subseteq R_j \)，即后面的集合包含前面的任意集合，现在我们去证明传递性， \( \forall (s, t), (t, u) \in R^+ \)，根据\( R^+ \)的定义，可得\( \exists i, j \in \mathbf{N}, (s, t) \in R_i, (t, u) \in R_j \)，不妨设\( j \geq i \)，则有\( (s, t) \)也\( \in R_j \)，于是根据\( R_j \)的定义，有\( (s, u) \in R_j \)，进而\( (s, u) \in R^+ \)，即\( R^+ \)满足传递性。
最小包含：令\( R' \)为任意包含\( R \)且满足传递性的关系，我们证明\( \forall i \in \mathbf{N}, R_i \subseteq R' \)，进而由\( R^+ \)的定义可得\( R^+ \subseteq R' \)，用数学归纳法来证明：当\( i = 0 \)时，\( R_i = R_0 = R \)，有\( R \subseteq R' \)，归纳假设当\( i = k \)时成立，当\( i = k + 1 \)时， \( R_{k + 1} = R_k \cup \{ (s, u) \mid \text{ for some } t, (s, t) \in R_k \text{ and } (t, u) \in R_k \} \)，根据归纳假设，有\( R_k \subseteq R' \)，而\( \forall (a, b) \in \{ (s, u) \mid \text{ for some } t, (s, t) \in R_k \text{ and } (t, u) \in R_k \} \)，有\( \exists c, (a, c), (c, b) \in R_k \)，进而有\( (a, c), (c, b) \in R' \)，再根据\( R' \)的传递性，可得\( (a, b) \in R' \)，至此可得，\( R_{k + 1} \)定义右侧两个并集的集合均是\( R' \)的子集，进而可得\( R_{k + 1} \subseteq R' \)，归纳完毕，有\( \forall i \in \mathbf{N}, R_i \subseteq R' \)，再由\( R^+ \)的定义可得\( R^+ \subseteq R' \)。
综上，\( R^+ \)是\( R \)的传递闭包。
证毕。
练习2.2.8
题目：
Suppose \( R \) is a binary relation on a set \( S \) and \( P \) is a predicate on \( S \) that is preserved by \( R \). Show that \( P \) is also preserved by \( R^* \).
证明：
令\( R', R^+ \)分别为练习2.2.6、练习2.2.7中构造的\( R \)的自反、传递闭包，令\( R'' = R' \cup R^+ \)，我们证明\( R'' = R^* \)，即\( R'' \)为 \( R \)的自反、传递闭包：
包含：根据\( R'', R', R^+ \)的定义，明显有\( R \subseteq R'' \)。
自反性：由\( \{ (s, s) \mid s \in S \} \subseteq R' \subseteq R'' \)，易得\( R'' \)满足自反性。
传递性：\( \forall (s, t), (t, u) \in R'' \)，分情况讨论：
- 如果\( (s, t), (t, u) \in R' \)，则继续分情况讨论：
- 如果\( (s, t), (t, u) \in R \)，此时\( (s, u) \in R^+ \)，进而\( (s, u) \in R'' \)。
- 如果\( (s, t), (t, u) \)中一个\( \in R \)，一个\( \in \{ (s, s) \mid s \in S \} \)，不妨设\( (s, t) \in R, (t, u) \in \{ (s, s) \mid s \in S \} \)，此时\( (s, u) = (s, t) \in R \)，进而\( (s, u) \in R'' \)。
- 如果\( (s, t), (t, u) \in \{ (s, s) \mid s \in S \} \)，则 \( (s, u) = (s, s) \in R' \)，进而\( (s, u) \in R'' \)。
- 如果\( (s, t), (t, u) \in R^+ \)，则\( (s, u) \in R^+ \)，进而\( (s, u) \in R'' \)。
综上，\( R'' \)满足传递性。
最小包含：令\( R''' \)为任意包含\( R \)的自反、传递闭包，类似练习2.2.7，用数学归纳法，易证\( R^+ \subseteq R''' \)，又明显\( R' \subseteq R''' \)，因此\( R'' = R' \cup R^+ \subseteq R''' \)。
综上，\( R'' \)为\( R \)的自反、传递闭包，即\( R^* = R'' \)。
现在，我们证明\( R^* \)保持\( P \)， \( \forall (s, s') \in R^*, P(s) \)，由\( R^* = R'' = R' \cup R^+ \)，可得 \( (s, s') \in R' \)或\( (s, s') \in R^+ \)，分情况讨论：
- 如果\( (s, s') \in R' \)，此时有\( (s, s') \in R \) 或\( (s, s') \in \{ (s, s) \mid s \in S \} \)，前者可由\( R \)保持\( P \)得到\( P(s') \)，后者则\( s' = s \)，进而有\( P(s') \)。
- 如果\( (s, s') \in R^+ \)，使用数学归纳法证明 \( \forall i \in \mathbf{N} \)，\( \forall (a, b) \in R_i \)，如果\( (a, b) \in R_i, P(a) \)，则\( P(b) \)，当\( i = 0 \)时，\( R_i = R_0 = R \)，如果\( (a, b) \in R_i = R, P(a) \)，则由\( R \)保持\( P \)可得\( P(b) \)，归纳假设当\( i = k \)时成立，当\( i = k + 1 \)时，如果\( (a, b) \in R_{k + 1}, P(a) \)，则\( (a, b) \in R_k \)或 \( (a, b) \in \{ (s, u) \mid \text{ for some } t, (s, t) \in R_k \text{ and } (t, u) \in R_k \} \)，前者由归纳假设可得结论成立，后者\( \exists c, (a, c), (c, b) \in R_k \)，根据归纳假设以及\( P(a) \)，可得\( P( c) \)，再根据归纳假设，可得\( P(b) \)，归纳完毕。继续回去证明，由\( (s, s') \in R^+ \)，可得\( \exists i \in \mathbf{N}, (s, s') \in R_i \)，加上\( P(s) \)以及数学归纳法证明的结论，可得\( P(s') \)。
综上，\( R^* \)保持\( P \)。
证毕。