指称语义学讲义

前言

我们的目的在于介绍domain论和指称语义, 并展示其是如何为推理程序行为提供数学基础的.

深入阅读

Gunter, C. A. (1992). Semantics of Programming Languages. Structures and Techniques. MIT Press.
这是一本研究生水平的教材, 包含有诸多本讲义未能涵盖的材料. 就讲义本身而言, 相关的章节是第1章, 第2章, 以及第4到6章.
Streicher, T. (2006). Domain-Theoretic Foundations of Functional Programming. World Scientific Publishing Co. ISBN 981-270-142-7
一本关于本讲义后半部分所涉及的PCF语言的研究生水平教材.

第1章引论

幻灯片1提示了给出编程语言的形式语义的几种方法. 操作性方法于Part IB课程Semantics of Programming Languages中介绍, 而公理性方法在Part II课程Hoare Logic中刻画. 本课程讲义给出了指称性方法的一些技巧的简要导引. 指称语义学的目的之一在于以尽可能抽象且实现无关的方式描述编程语言的构造: 通过这种方法, 我们有可能获得对于某些概念的洞察, 而这些概念构成了编程语言以及其间关系的基础, 甚至有时还能理解在语言设计中实现这些概念的新方式. 当然, 验证指称性描述可以被实现是重要的. 换言之, 即将指称语义和操作语义联系起来: 我们将在之后刻画如何施行此事.

形式语义的风格

操作的.程序片段的意义基于程序执行过程中其可以施行的计算步骤定义.

公理的.程序片段的意义间接地通过程序性质的某种逻辑的公理和规则定义.

指称的.关心给出编程语言的数学模型. 程序片段的意义抽象地定义为某种适当数学结构的元素.

幻灯片1

指称语义的特征性质

每个程序片段 $P$ 被赋予一个指称 $⟦ P ⟧$ , 这是一个数学对象, 其代表了 $P$ 对于完整程序的意义的贡献.
一个程序片段的意义只由其子片段决定, 或者说指称语义是可复合的.

幻灯片2

第1.1节指称语义的基本例子

考虑基本的编程语言IMP^$-$, 其相当于带有控制结构的算术和布尔表达式, 而这里的控制结构是由赋值, 顺序, 条件刻画的, 见幻灯片3.

指称语义的基本例子 (I):

IMP^$-$的句法

算术表达式: $A \in Aexp ⩴ \underline{n} | L | A + A | \dots$ 其中 $n$ 是整数, 而 $L \in 𝕃$ , $𝕃$ 是给定的位置的集合.

布尔表达式: $B \in Bexp ⩴ true | false | A = A | \neg B | \dots$

命令: $\begin{matrix} C \in Comm & ⩴ & skip | L ≔ A | C; C \\ | & if B then C else C \end{matrix}$

幻灯片3

译者注记.

\underline{n}

是代表整数

n

的句法.

为了给出一个编程语言的指称语义, 我们需要赋予每种程序片段的句法范畴以一个解释的domain (domain of interpretation), 然后复合性地描述各种形成程序片段 (phrase-forming) 的构造所对应的语义函数. 对于IMP^$-$, 幻灯片4到10给出了其指称语义, 并且这个语义也很容易在SML中实现.

指称语义的基本例子 (II)

语义函数

\begin{array}{l} A : Aexp \to (State \to ℤ) \\ B : Bexp \to (State \to 𝔹) \\ C : Comm \to (State ⇀ State) \end{array}

其中

\begin{matrix} ℤ & = & {\dots, - 1, 0, 1, \dots} \\ 𝔹 & = & {true, false} \\ State & = & (𝕃 \to ℤ) \end{matrix}

幻灯片4

译者注记.

⇀

的含义是部分函数 (partial function). 另外,

true

和

true

是不同的, 前者是句法, 而后者是一个数学对象.

指称语义的基本例子 (III)

语义函数

A

\begin{matrix} A ⟦ \underline{n} ⟧ & = & λ s \in State . n \\ A ⟦ L ⟧ & = & λ s \in State . s (L) \\ A ⟦ A_{1} + A_{2} ⟧ & = & λ s \in State . A ⟦ A_{1} ⟧ (s) + A ⟦ A_{2} ⟧ (s) \end{matrix}

幻灯片5

指称语义的基本例子 (IV)

语义函数

B

\begin{matrix} B ⟦ true ⟧ & = & λ s \in State . true \\ B ⟦ false ⟧ & = & λ s \in State . false \\ B ⟦ A_{1} = A_{2} ⟧ & = & λ s \in State . eq (A ⟦ A_{1} ⟧ (s), A ⟦ A_{2} ⟧ (s)) \\ 其中 eq (a, a^{'}) = {\begin{matrix} true & , 如果 a = a^{'} \\ false & , 如果 a \neq a^{'} \end{matrix} \\ B ⟦ \neg B ⟧ & = & λ s \in State . \neg (B ⟦ B ⟧ (s)) \end{matrix}

幻灯片6

指称语义的基本例子 (V)

语义函数

C

⟦ skip ⟧ = λ s \in State . s

注记: 从现在开始, 语义函数的名字都将省略.

幻灯片7

可复合性一例

给定部分函数 $⟦ C ⟧, ⟦ C^{'} ⟧ : State ⇀ State$ 以及函数 $⟦ B ⟧ : State \to {true, false}$ , 我们可以定义 $⟦ if B then C else C^{'} ⟧ = λ s \in State . if (⟦ B ⟧ (s), ⟦ C ⟧ (s), ⟦ C^{'} ⟧ (s))$ 其中 $if (b, x, x^{'}) = {\begin{matrix} x & , 如果 b = true \\ x^{'} & , 如果 b = false \end{matrix}$

幻灯片8

指称语义的基本例子 (VI)

语义函数

C

⟦ L ≔ A ⟧ = λ s \in State . λ l \in 𝕃 . if (l = L, ⟦ A ⟧ (s), s (l))

幻灯片9

顺序复合的指称语义

两个命令的顺序复合 $C; C^{'}$ 的指称为 $⟦ C; C^{'} ⟧ = ⟦ C^{'} ⟧ \circ ⟦ C ⟧ = λ s \in State . ⟦ C^{'} ⟧ (⟦ C ⟧ (s))$ 这实际上就是命令的指称 (即部分函数 $⟦ C ⟧, ⟦ C^{'} ⟧ : State ⇀ State$ ) 的复合而已.

与之相对的是, 顺序复合的操作语义为 $\frac{C, s ⇓ s^{'} C^{'}, s^{'} ⇓ s^{″}}{C; C^{'}, s ⇓ s^{″}}$

幻灯片10

第1.2节例子: 作为不动点的 $while$ 循环

幻灯片2所提及的可复合性的要求是相当tough的. 我们用以赋予程序片段指称的数学对象必须足够丰富, 因为需要支持建模所讨论编程语言的一切形成程序片段的构造. 某些形成程序片段的构造是容易处理的, 而其他一些可能就不那么容易了. 例如, 牵涉状态改变命令的条件表达式 [译注: 更准确地说, 应该是条件命令] 可以基于应用相应的分支函数于立即子表达式的指称给出其指称语义: 见幻灯片8. 类似地, 命令的顺序复合的指称语义可由从状态到状态的部分函数的复合操作得到, 如幻灯片10.

现在我们来考虑基本编程语言IMP的指称语义, 其扩展了IMP^$-$以 $while$ 循环: $C \in Comm ⩴ \dots | while B do C$ 然而, 这种循环构造并不容易以可复合的方式解释!

$while$ 循环的转换语义为 $⟨ while B do C, s ⟩ \to ⟨ if B then C; (while B do C) else skip, s ⟩$ 这暗示了其作为从状态到状态的部分函数的指称应该满足 $⟦ while B do C ⟧ = ⟦ if B then C; (while B do C) else skip ⟧$ 我们应该注意到这不能直接用来定义 $⟦ while B do C ⟧$ , 因为右边恰恰包含有一个我们想要定义其指称的子片段. 使用顺序复合和 $if$ 的指称语义, 以及 $skip$ 的指称为恒等函数 $λ s \in State . s$ 的事实, 上面这条等式是在说 $⟦ while B do C ⟧$ 应该是幻灯片11中给出的不动点方程的一个解.

$⟦ while B do C ⟧ 的不动点性质$

⟦ while B do C ⟧ = f_{⟦ B ⟧, ⟦ C ⟧} (⟦ while B do C ⟧)

其中, 对于每个

b : State \to {true, false}

和

c : State ⇀ State

, 我们定义

f_{b, c} : (State ⇀ State) \to (State ⇀ State)

为

f_{b, c} = λ w \in (State ⇀ State) . λ s \in State . if (b (s), w (c (s)), s)

为什么 $w = f_{⟦ B ⟧, ⟦ C ⟧} (w)$ 有解?
若此方程具有多解, 那么选取哪一个作为 $⟦ while B do C ⟧$ 呢?

幻灯片11

在赋予带有递归特性的编程语言以指称语义时, 这样的不动点方程经常出现. 自Dana Scott于60年代晚期的先驱性研究始, 一种被称为domain论的数学理论建立起来以提供一种背景环境, 其中我们不仅总是可以找到因指称语义而生的不动点方程的解, 而且还能选出在某种适切意义下最小的解, 而这实际上保证了指称语义和操作语义之间的协调配合. 关键的想法在于考虑用作指称的数学对象之间的一种偏序, 此偏序表达了这样的事实, 一个对象由另一个对象近似, 或者说比另一个对象携带了更多的信息, 或者说比另一个对象更加良定. 然后, 不动点方程的最小解可以被构造为对于解的近似升链的极限. 在下一章里, 这些想法将会变得从数学角度来说更加精确和一般, 但是目前先让我们具体地阐明该如何运用此想法解决幻灯片11中的特定问题.

为了确定起见, 让我们考虑以下特定的 $while$ 循环 $while X > 0 do (Y ≔ X ⁎ Y; X ≔ X - 1)$ 其中 $X$ 和 $Y$ 是两个不同的整数存储位置 (变量), 而位置的集合 $𝕃 = {X, Y}$ .

译者注记. 在某种意义上说, 将

𝕃

的元素既用作句法也用作讨论语义时所牵涉的概念对象是一种(司空见惯的)滥用. 但是, 只要满足目的就好.

在这种情形之下, 我们可以就取状态为赋值 $[X \mapsto x, Y \mapsto y]$ , 其中 $x, y \in ℤ$ , 这记录了位置 $X$ 和 $Y$ 的当前内容. 因此, $State = (𝕃 \to ℤ)$ .

译者注记. 实际上, 幻灯片4中就已经定义

State

为

(𝕃 \to ℤ)

了.

我们正在试着将这个 $while$ 循环的指称定义为一个部分函数 $w : State ⇀ State$ 其应该是幻灯片11上的不动点方程 $w = f_{⟦ X > 0 ⟧, ⟦ Y ≔ X ⁎ Y; X ≔ X - 1 ⟧} (w)$ 的一个解.

对于特定的布尔表达式 $B = (X > 0)$ 和命令 $C = (Y ≔ X ⁎ Y; X ≔ X - 1)$ , 函数 $f_{⟦ B ⟧, ⟦ C ⟧}$ 恰好与幻灯片12上定义的函数 $f$ 相同.

$⟦ while X > 0 do (Y ≔ X ⁎ Y; X ≔ X - 1) ⟧$

令

\begin{matrix} State & \overset{def}{=} & (𝕃 \to ℤ) \\ D & \overset{def}{=} & (State ⇀ State) \end{matrix}

对于

⟦ while X > 0 do (Y ≔ X ⁎ Y; X ≔ X - 1) ⟧ \in D

, 我们寻求

w = f (w)

的一个最小的解, 其中

f : D \to D

被定义为

f (w) ([X \mapsto x, Y \mapsto y]) = {\begin{matrix} [X \mapsto x, Y \mapsto y] & , 如果 x \leq 0 \\ w ([X \mapsto x - 1, Y \mapsto x ⁎ y]) & , 如果 x > 0 \end{matrix}

幻灯片12

$D 上的偏序$

$D$ 上的偏序 $⊑$ :
$w ⊑ w^{'}$ 当且仅当对于每个 $s \in State$ , 如果 $w$ 在 $s$ 上有定义, 那么 $w^{'}$ 也在 $s$ 上有定义, 并且 $w (s) = w^{'} (s)$ . 另外一种描述是, $w$ 的图包含于 $w^{'}$ 的图.
最小元 $⊥ \in D$ w.r.t. $⊑$ :
$⊥$ 即全然未定义的部分函数, 或者说图为空的部分函数, 其满足对于每个 $w \in D$ , $⊥ ⊑ w$ .

幻灯片13

考虑幻灯片13上给出的 $D = (State ⇀ State)$ 的元素之间的偏序 $⊑$ . 注意到 $⊑$ 实际上就是前文所提及的"信息序"的具体化身: 如果 $w ⊑ w^{'}$ , 那么 $w^{'}$ 在 $w$ 有定义的地方都保持和 $w$ 的一致, 但是它可能在其他一些参数上也有定义. 我们还应该注意到的是, $D$ 包含一个相对于此偏序的最小元: 对于全然未定义的部分函数, 我们将其记作 $⊥$ , 它满足对于任意的 $w \in D$ 都有 $⊥ ⊑ w$ .

自 $⊥$ 开始, 我们反复应用函数 $f$ 以构造一个部分函数的序列 $w_{0}, w_{1}, w_{2}, \dots$ : $w_{0} \overset{def}{=} ⊥; w_{n + 1} \overset{def}{=} f (w_{n}) .$ 使用幻灯片12上的 $f$ 的定义, 我们发现 $w_{1} [X \mapsto x, Y \mapsto y] = f (⊥) [X \mapsto x, Y \mapsto y] = {\begin{matrix} [X \mapsto x, Y \mapsto y] & , 如果 x \leq 0 \\ undefined & , 如果 x \geq 1 \end{matrix}$ $w_{2} [X \mapsto x, Y \mapsto y] = f (w_{1}) [X \mapsto x, Y \mapsto y] = {\begin{matrix} [X \mapsto x, Y \mapsto y] & , 如果 x \leq 0 \\ [X \mapsto 0, Y \mapsto y] & , 如果 x = 1 \\ undefined & , 如果 x \geq 2 \end{matrix}$ $w_{3} [X \mapsto x, Y \mapsto y] = f (w_{2}) [X \mapsto x, Y \mapsto y] = {\begin{matrix} [X \mapsto x, Y \mapsto y] & , 如果 x \leq 0 \\ [X \mapsto 0, Y \mapsto y] & , 如果 x = 1 \\ [X \mapsto 0, Y \mapsto 2 ⁎ y] & , 如果 x = 2 \\ undefined & , 如果 x \geq 3 \end{matrix}$ $w_{4} [X \mapsto x, Y \mapsto y] = f (w_{3}) [X \mapsto x, Y \mapsto y] = {\begin{matrix} [X \mapsto x, Y \mapsto y] & , 如果 x \leq 0 \\ [X \mapsto 0, Y \mapsto y] & , 如果 x = 1 \\ [X \mapsto 0, Y \mapsto 2 ⁎ y] & , 如果 x = 2 \\ [X \mapsto 0, Y \mapsto 6 ⁎ y] & , 如果 x = 3 \\ undefined & , 如果 x \geq 4 \end{matrix}$ 并且, 在 $n \geq 1$ 的一般情况下, 我们有 $w_{n} [X \mapsto x, Y \mapsto y] = {\begin{matrix} [X \mapsto x, Y \mapsto y] & , 如果 x \leq 0 \\ [X \mapsto 0, Y \mapsto (! x) ⁎ y] & , 如果 0 < x < n \\ undefined & , 如果 x \geq n \end{matrix}$ 其中 $! x$ 是 $x$ 的阶乘.

因此, 我们得到了一个部分函数的递增序列 $w_{0} ⊑ w_{1} ⊑ w_{2} ⊑ \dots ⊑ w_{n} ⊑ \dots$ 所有这些部分函数之并是元素 $w_{\infty} \in D$ , 其为 $w_{\infty} [X \mapsto x, Y \mapsto y] = {\begin{matrix} [X \mapsto x, Y \mapsto y] & , 如果 x \leq 0 \\ [X \mapsto 0, Y \mapsto (! x) ⁎ y] & , 如果 x > 0 \end{matrix}$ 注意到 $w_{\infty}$ 是 $f$ 的一个不动点, 因为对于每个 $[X \mapsto x, Y \mapsto y]$ , 我们有 $\begin{array}{rcl} f (w_{\infty}) [X \mapsto x, Y \mapsto y] & = & {\begin{matrix} [X \mapsto x, Y \mapsto y] & , 如果 x \leq 0 \\ w_{\infty} [X \mapsto x - 1, Y \mapsto x ⁎ y] & , 如果 x > 0 \end{matrix} (根据 f 的定义) \\ = & {\begin{matrix} [X \mapsto x, Y \mapsto y] & , 如果 x \leq 0 \\ [X \mapsto 0, Y \mapsto 1 ⁎ y] & , 如果 x = 1 \\ [X \mapsto 0, Y \mapsto! (x - 1) ⁎ x ⁎ y] & , 如果 x > 1 \end{matrix} (根据 w_{\infty} 的定义) \\ = & w_{\infty} [X \mapsto x, Y \mapsto y] \end{array}$ 实际上, 我们可以表明 $w_{\infty}$ 是 $f$ 的最小不动点, 意即对于任意的 $w \in D$ , 有 $w = f (w) \Rightarrow w_{\infty} ⊑ w .$ 我们取这个最小不动点 $w_{\infty}$ 作为 $while X > 0 do (Y ≔ X ⁎ Y; X ≔ X - 1)$ 的指称, 其构造方式是下一章要证明的Tarski不动点定理的一个实例. 我们也应该注意到, $w_{\infty}$ 的确就是命令 $while X > 0 do (Y ≔ X ⁎ Y; X ≔ X - 1)$ 的结构操作语义所给出的从状态到状态的函数, 见Part IB课程Semantics of Programming Languages.

第1.3节练习

练习1. 在SML中实现IMP^$-$的指称语义.

练习2. 考虑幻灯片11上定义的函数

f_{b, c} : (State ⇀ State) \to (State ⇀ State)

根据 $n$ 上的归纳证明 $f_{b, c}^{n} (⊥) = λ s \in State . {\begin{matrix} c^{k} (s) & , 如果存在 0 \leq k < n 满足对于每个 0 \leq i < k \\ 有 b (c^{i} (s)) = true 而 b (c^{k} (s)) = false \\ undefined & , 如果对于每个 0 \leq i < n 有 b (c^{i} (s)) = true \end{matrix}$
令 $w_{b, c} : State ⇀ State$ 是由 $w_{b, c} \overset{def}{=} λ s \in State . {\begin{matrix} c^{k} (s) & , 如果存在 k \geq 0 满足对于每个 0 \leq i < k \\ 有 b (c^{i} (s)) = true 而 b (c^{k} (s)) = false \\ undefined & , 如果对于每个 i \geq 0 有 b (c^{i} (s)) = true \end{matrix}$ 定义的部分函数, 证明 $w_{b, c}$ 满足不动点方程 $w_{b, c} = f_{b, c} (w_{b, c}) .$
对于 $b = ⟦ true ⟧ = λ s \in State . true$ 和 $c = ⟦ skip ⟧ = λ s \in State . s$ , 描述函数 $f_{b, c}$ . 什么样的从状态到状态的部分函数是 $f_{b, c}$ 的不动点呢? 相对于 $⊑$ 的最小不动点是什么呢? 这个最小不动点和 $while true do skip$ 的操作语义所确定的从状态到状态的部分函数是一致的吗?

练习3. 说明幻灯片13上的关系

⊑

的确是一个偏序, 而且

⊥

是最小元.

练习4. 证明

w_{\infty}

的确是

f

的最小不动点. 更一般地, 根据幻灯片13和练习2的定义, 证明对于任意的

w \in (State ⇀ State)

, 有

w = f_{b, c} (w) \Rightarrow w_{b, c} ⊑ w .

第2章最小不动点

本章介绍了被称为domain论的数学理论, 其为构造各种编程语言特性的指称语义中所用到的最小不动点提供了一个一般性的框架. 该理论是由Dana Scott提出的.

第2.1节偏序集和单调函数

论点

所有计算的domain都是带有最小元的偏序集.
所有可计算函数都是单调的.

幻灯片14

第2.1.1小节偏序集

domain论使用满足特定完备性质的偏序集. 我们在幻灯片15中回顾了偏序的定义. $D$ 被称为偏序集 $(D, ⊑)$ 的基础集(underlying set). 大部分时候, 我们只以基础集的名字引用偏序集, 而以相同的符号 $⊑$ 代表不同偏序集的偏序.

偏序集

集合

D

上的二元关系

⊑

是一个偏序, 当且仅当它是

自反的: $\forall d \in D . d ⊑ d$ ;
传递的: $\forall d, d^{'}, d^{″} \in D . d ⊑ d^{'} ⊑ d^{″} \Rightarrow d ⊑ d^{″}$ ;
反对称的: $\forall d, d^{'} \in D . d ⊑ d^{'} ⊑ d \Rightarrow d = d^{'}$ .

序对

(D, ⊑)

被称为一个偏序集.

幻灯片15

译者注记.

d ⊑ d^{'} ⊑ d^{″}

是

d ⊑ d^{'} & d^{'} ⊑ d^{″}

的缩写.

偏序集公理: 规则形式

\frac{}{x ⊑ x}

\frac{x ⊑ y y ⊑ z}{x ⊑ z}

\frac{x ⊑ y y ⊑ x}{x = y}

幻灯片16

$部分函数的domain, X ⇀ Y$

基础集: 由所有定义域 $dom (f) \subseteq X$ 且取值于 $Y$ 的部分函数 $f$ 构成.
偏序: $f ⊑ g$ 当且仅当 $dom (f) \subseteq dom (g)$ 且 $\forall x \in dom (f) . f (x) = g (x)$ , 或者说 $graph (f) \subseteq graph (g)$ .

幻灯片17

译者注记. 实在是一点可有可无且无聊的注记. 若

A \subseteq X

而

B \subseteq Y

, 那么应该将

f : A ⇀ B

也视为

X ⇀ Y

的元素吗 (假设排除

A = X

且

B = Y

的平凡情形)? 这是微妙的, 往往取决于具体的上下文.

例子1. 从集合

X

到集合

Y

的所有部分函数构成的集合

(X ⇀ Y)

可以看成是一个偏序集, 如幻灯片17那样. 前一章里, 我们取这个domain在

X = Y = State

(某个状态集合) 情形下的实例作为命令的指称集.

第2.1.2小节单调函数

幻灯片18中给出了偏序集之间的单调映射的概念.

单调性

两个偏序集之间的函数

f : D \to E

是单调的, 如果

\forall d, d^{'} \in D . d ⊑ d^{'} \Rightarrow f (d) ⊑ f (d^{'}) .

\frac{x ⊑ y}{f (x) ⊑ f (y)} (f 单调)

幻灯片18

例子2. 给定偏序集

D

和

E

, 显然常函数

λ d \in D . e : D \to E

是单调的.

例子3. 当

D

是部分函数的domain

(State ⇀ State)

(见幻灯片17) 时, 幻灯片11上定义的与

while

循环的指称语义有关的函数

f_{b, c} : D \to D

是一个单调函数. 我们将其验证留作练习.

第2.2节最小元和前不动点 (pre-fixed point)

定义1. 设

D

是一个偏序集,

S

是

D

的一个子集,

d \in S

被称为

S

的最小元, 如果其满足

\forall x \in S . d ⊑ x .

注意到因为 $⊑$ 是反对称的, 所以 $S$ 至多拥有一个最小元. 我们也应该注意到, 有的偏序集是没有最小元的. 例如, 带有通常偏序的 $ℤ$ .

函数 $f : D \to D$ 的一个不动点, 根据定义, 是满足 $f (d) = d$ 的一个元素 $d \in D$ . 如果 $D$ 是一个偏序集, 我们可以考虑一个更弱的概念, 即前不动点, 见幻灯片19.

前不动点

令

D

是一个偏序集而

f : D \to D

是一个函数.
一个元素

d \in D

是

f

的一个前不动点, 如果其满足

f (d) ⊑ d

f

的最小前不动点, 如果存在的话, 记作

fix (f) .

因此, 最小前不动点由以下两条性质(唯一地)刻画:

(lpf1): $f (fix (f)) ⊑ fix (f)$ ;
(lpf2): $\forall d \in D . f (d) ⊑ d \Rightarrow fix (f) ⊑ d$ .

幻灯片19

证明原理

$\frac{}{f (fix (f)) ⊑ fix (f)}$
令 $D$ 是一个偏序集, $f : D \to D$ 是一个带有最小前不动点 $fix (f) \in D$ 的函数.
对于任意的 $x \in D$ , 为了证明 $fix (f) ⊑ x$ , 只需要证明 $f (x) ⊑ x$ . $\frac{f (x) ⊑ x}{fix (f) ⊑ x}$

幻灯片20

命题2. 设

D

是一个偏序集而

f : D \to D

是一个带有最小前不动点

fix (f)

的函数. 只要

f

是单调的, 那么

fix (f)

实际上就是

f

的一个不动点, 因此也是

f

的最小不动点.

证明. 因为

fix (f)

是

f

的前不动点, 所以

f (fix (f)) ⊑ fix (f)

. 如果

f

是单调的, 那么

f (f (fix (f))) ⊑ f (fix (f)) .

换言之,

f (fix (f))

也是

f

的一个前不动点. 但是, 鉴于

fix (f)

是最小的前不动点, 我们可以推出

fix (f) ⊑ f (fix (f)) .

根据偏序的反对称性, 我们可以断言

fix (f) = f (fix (f))

即

fix (f)

是

f

的一个不动点. 而且, 考虑到偏序的自反性, 不动点也是前不动点. 对于任意的

d \in D

满足

d = f (d)

, 我们有

fix (f) ⊑ d

. 换言之,

fix (f)

是

f

的最小不动点.

◻

第2.3节完全偏序 (cpo) 和连续函数

论点*

所有计算的domain都是带有最小元的完全偏序.
所有可计算函数都是连续的.

幻灯片21

第2.3.1小节 domain

定义1.

若存在, 我们将偏序集 $D$ 的最小元记为 $⊥_{D}$ . 若 $D$ 在上下文中是已知的, 写成 $⊥$ 就可以了. 因此, $⊥$ 由性质 $\forall d \in D . ⊥ ⊑ d$ 唯一确定. 偏序集的最小元有时也被称为其底(bottom)元素.
偏序集D中的一个可数的升链是由D的元素构成的一个序列满足d0⊑d1⊑d2⊑…这样的链的一个上界是任意满足∀n∈ℕ.dn⊑d的d∈D. 若链的最小上界(lub)存在, 我们将其记为⨆n≥0dn.因此, 根据定义:
- $\forall m \in ℕ . d_{m} ⊑ ⨆_{n \geq 0} d_{n}$ .
- 对于任意的 $d \in D$ , 如果 $\forall m \in ℕ . d_{m} ⊑ d$ , 那么 $⨆_{n \geq 0} d_{n} ⊑ d$ .

译者注记. 所谓的链, 指的是偏序集的全序子集. 不过, 本讲义实际上只考虑以(通常的)序列面目出现的可数的升链.

评注2. 以下是读者应该注意的点.

我们不需要考虑偏序集中不可数的链, 或者降链: 因此, "链"将总是指可数的升链.
就和偏序集的任意子集的最小元一样, 链的最小上界若存在则唯一. 当然, 链可以没有最小上界, 例如 $ℕ$ 中的 $0 \leq 1 \leq 2 \leq \dots$ , 不过它连上界也没有.
最小上界有时也被称为上确界. $⨆_{n \geq 0} d_{n}$ 的一些其他常见替代记号为 $⨆_{n = 0}^{\infty} d_{n} 和 ⨆ {d_{n} | n \geq 0} .$
链的元素不必是互异的. 实际上, 我们称一个链 $d_{0} ⊑ d_{1} ⊑ d_{2} ⊑ \dots$ 终至恒常, 如果存在 $N \in ℕ$ 使得 $\forall n \geq N . d_{n} = d_{N}$ . 注意到此时 $⨆_{n \geq 0} d_{n} = d_{N}$ .
如果我们丢弃链的开头任意有限数目的元素, 也并不会影响其上界集和最小上界: $\forall N \in ℕ . ⨆_{n \geq 0} d_{n} = ⨆_{n \geq 0} d_{N + n} .$

cpo和domain

一个链完备偏序集(chain-complete poset), 或者说缩写为cpo, 是一个偏序集

(D, ⊑)

满足其中的每个链

d_{0} ⊑ d_{1} ⊑ d_{2} ⊑ \dots

都具有最小上界

⨆_{n \geq 0} d_{n}

(lub1): $\forall m \geq 0 . d_{m} ⊑ ⨆_{n \geq 0} d_{n}$ ;
(lub2): $\forall d \in D . (\forall m \geq 0 . d_{m} ⊑ d) \Rightarrow ⨆_{n \geq 0} d_{n} ⊑ d$ .

一个domain是一个带有最小元

⊥

的cpo:

\forall d \in D . ⊥ ⊑ d .

幻灯片22

译者注记. 幻灯片22的两个冒号后面的内容, 只是为了解释什么是最小上界和最小元. 另外, 链完备偏序集也被称为完全偏序, complete partial order.

最小元和最小上界的定义: 规则形式

\frac{}{⊥ ⊑ x}

\frac{}{x_{i} ⊑ ⨆_{n \geq 0} x_{n}} (i \geq 0 而 ⟨ x_{n} ⟩ 是一个链)

\frac{\forall m \geq 0 . x_{m} ⊑ x}{⨆_{n \geq 0} x_{n} ⊑ x} (⟨ x_{n} ⟩ 是一个链)

幻灯片23

本讲义里我们关心的是具有特定完备性质的偏序集, 见幻灯片22. 读者应该注意的是, 在有关的指称语义的文献中, 术语"domain"的含义是相当宽泛的: 存在各种各样的domain, 它们可能具有各种各样的序论性质, 而不仅仅是满足链完备性质和拥有最小元.

例子3. 从集合

X

到集合

Y

的所有部分函数的集合

(X ⇀ Y)

上可以赋予一个偏序成为domain, 见幻灯片24. 在第1.2节, 我们使用了

X = Y = State

的特殊情形作为命令的指称集. 我们应该注意到, 声称是链

f_{0} ⊑ f_{1} ⊑ f_{2} ⊑ \dots

的最小上界的

f

的确是一个良定的部分函数, 因为在有定义的地方, 每个

f_{n}

的值都是一致的. 至于验证

f

的确是偏序集

(X ⇀ Y, ⊑)

中的

f_{0} ⊑ f_{1} ⊑ f_{2} ⊑ \dots

的最小上界, 我们将其留给读者作为练习.

$部分函数的domain, X ⇀ Y$

基础集: 由所有满足以下条件的部分函数

f

构成, 其定义域

dom (f) \subseteq X

而取值于

Y

.
偏序:

f ⊑ g

当且仅当

dom (f) \subseteq dom (g)

且

\forall x \in dom (f) . f (x) = g (x)

, 或者说

graph (f) \subseteq graph (g)

.
链的最小上界: 链

f_{0} ⊑ f_{1} ⊑ f_{2} ⊑ \dots

的最小上界是部分函数

f

, 其

dom (f) = ⋃_{n \geq 0} dom (f_{n})

而

f (x) = {\begin{matrix} f_{n} (x) & , 如果存在某个 n \in ℕ 使得 x \in dom (f_{n}) \\ undefined & , 否则的话 \end{matrix}

最小元素:

⊥

是全然未定义的部分函数.

幻灯片24

例子4. 对于任意的偏序集

(D, ⊑)

而言, 如果

D

是有限的, 那么该偏序集是一个cpo. 这是因为, 在这样的偏序集中, 任何链都将终至恒常, 因而拥有最小上界. 当然, 有限的偏序集也不一定拥有最小元, 即不是一个domain. 例如, 考虑以下Hasse图所描述的偏序集.一个偏序集的Hasse图是一个有向图, 其顶点是偏序集的基础集的元素, 而从顶点

x

到顶点

y

有一条边当且仅当

x \neq y

且

\forall z . (x ⊑ z & z ⊑ y) \Rightarrow (z = x \lor z = y)

图1

图1展示两个非常简单但却无限的domain, 而以下是两个并非cpo的偏序集的例子.

例子5. 装备有通常偏序

\leq

的自然数集

ℕ = {0, 1, 2, \dots}

不是一个cpo, 因为链

0 \leq 1 \leq 2 \leq \dots

在

ℕ

中没有上界.

例子6. 考虑上图的第二个例子的一种修改版本, 其中我们为

ℕ

添加了两个不同的上界

ω_{1} \neq ω_{2}

. 换言之, 我们考虑的是

D \overset{def}{=} ℕ \cup {ω_{1}, ω_{2}}

, 而其上的偏序

⊑

为

d ⊑ d^{'} \overset{def}{\Leftrightarrow} {\begin{matrix} d \leq d^{'} & , 如果 d, d^{'} \in ℕ \\ d \in ℕ \lor d = d^{'} & , 如果 d^{'} \in {ω_{1}, ω_{2}} \end{matrix}

然后,

D

中的链

0 ⊑ 1 ⊑ 2 ⊑ \dots

拥有两个上界, 即

ω_{1}

和

ω_{2}

, 但是没有最小的上界, 因为

ω_{1}

和

ω_{2}

不可比较. 因此,

(D, ⊑)

不是一个cpo.

链的最小上界的一些性质

设

D

是一个cpo.

对于任意的 $d \in D$ , $⨆_{n \geq 0} d = d$ .
对于 $D$ 中的每个链 $d_{0} ⊑ d_{1} ⊑ \dots ⊑ d_{n} ⊑ \dots$ , 我们有 $⨆_{n \geq 0} d_{n} = ⨆_{n \geq 0} d_{N + n}$ 对于任意的 $N \in ℕ$ 成立.

幻灯片25

链的最小上界的一些性质 (续)

对于 $D$ 中的两条链 $d_{0} ⊑ d_{1} ⊑ \dots ⊑ d_{n} ⊑ \dots$ 和 $e_{0} ⊑ e_{1} ⊑ \dots ⊑ e_{n} ⊑ \dots$ , 如果对于每个 $n \in ℕ$ 有 $d_{n} ⊑ e_{n}$ , 那么 $⨆_{n \geq 0} d_{n} ⊑ ⨆_{n \geq 0} e_{n} .$

\frac{\forall n \in 0 . x_{n} ⊑ y_{n}}{⨆_{n \geq 0} x_{n} ⊑ ⨆_{n \geq 0} y_{n}} (⟨ x_{n} ⟩ 和 ⟨ y_{n} ⟩ 俱是链)

幻灯片26

双链的对角化

引理. 令

D

是一个cpo, 设双下标索引的元素

d_{m, n} \in D

(其中

m, n \geq 0

) 构成的族满足

m \leq m^{'} & n \leq n^{'} \Rightarrow d_{m, n} ⊑ d_{m^{'}, n^{'}}

那么我们有

⨆_{n \geq 0} d_{0, n} ⊑ ⨆_{n \geq 0} d_{1, n} ⊑ ⨆_{n \geq 0} d_{2, n} ⊑ \dots

以及

⨆_{m \geq 0} d_{m, 0} ⊑ ⨆_{m \geq 0} d_{m, 1} ⊑ ⨆_{m \geq 0} d_{m, 2} ⊑ \dots

而且

⨆_{m \geq 0} (⨆_{n \geq 0} d_{m, n}) = ⨆_{k \geq 0} d_{k, k} = ⨆_{n \geq 0} (⨆_{m \geq 0} d_{m, n}) .

幻灯片27

证明. 我们利用了定义链的最小上界的性质, 即幻灯片22上的(lub1)和(lub2). 首先, 注意到如果

m \leq m^{'}

, 那么

\begin{array}{rcl} d_{m, n} & ⊑ & d_{m^{'}, n} \\ ⊑ & ⨆_{n^{'} \geq 0} d_{m^{'}, n^{'}} \end{array}

对于每个

n \geq 0

成立. 因此,

⨆_{n \geq 0} d_{m, n} ⊑ ⨆_{n^{'} \geq 0} d_{m^{'}, n^{'}}

. 于是, 我们的确可以得到一条由最小上界构成的链

⨆_{n \geq 0} d_{0, n} ⊑ ⨆_{n \geq 0} d_{1, n} ⊑ ⨆_{n \geq 0} d_{2, n} ⊑ \dots

并且我们可以构造其最小上界

⨆_{m \geq 0} ⨆_{n \geq 0} d_{m, n}

. 运用两次(lub1), 我们有

d_{k, k} ⊑ ⨆_{n \geq 0} d_{k, n} ⊑ ⨆_{m \geq 0} ⨆_{n \geq 0} d_{m, n}

对于每个

k \geq 0

成立, 那么根据(lub2)可以得到

⨆_{k \geq 0} d_{k, k} ⊑ ⨆_{m \geq 0} ⨆_{n \geq 0} d_{m, n}

反过来, 对于每个

m, n \geq 0

, 我们注意到

\begin{array}{rcl} d_{m, n} & ⊑ & d_{\max (m, n), \max (m, n)} \\ ⊑ & ⨆_{k \geq 0} d_{k, k} \end{array}

因而再应用两次(lub2)就可以推出

⨆_{m \geq 0} ⨆_{n \geq 0} d_{m, n} ⊑ ⨆_{k \geq 0} d_{k, k}

根据

⊑

的反对称性, 我们就得出了想要的等式. 剩余的结果也可按照相同的论证手法得到, 只需要交换

m

和

n

的角色.

◻

第2.3.2小节连续函数

连续性和严格性

如果D和E是cpo, 函数f是连续的当且仅当
1. $f$ 是单调的;
2. $f$ 保持链的最小上界, 即对于 $D$ 中的每条链 $d_{0} ⊑ d_{1} ⊑ \dots$ , 我们有 $f (⨆_{n \geq 0} d_{n}) = ⨆_{n \geq 0} f (d_{n}) .$
如果 $D$ 和 $E$ 都拥有最小元, 那么称函数 $f$ 是严格的, 如果 $f (⊥) = ⊥$ .

幻灯片28

评注7. 我们注意到如果

f : D \to E

是单调的, 并且

d_{0} ⊑ d_{1} ⊑ d_{2} ⊑ \dots

是

D

中的一个链, 那么应用

f

就可以得到

E

中的一个链

f (d_{0}) ⊑ f (d_{1}) ⊑ f (d_{2}) ⊑ \dots

. 而且, 如果

d

是第一条链的一个上界, 那么

f (d)

是第二条链的一个上界. 换言之, 如果

f : D \to E

是cpo之间的单调函数, 我们总有

⨆_{n \geq 0} f (d_{n}) ⊑ f (⨆_{n \geq 0} d_{n})

因此, 根据

⊑

的固有性质, 给定cpo之间的单调函数

f : D \to E

f

是连续的等价于对于

D

中的每条链

d_{0} ⊑ d_{1} ⊑ d_{2} ⊑ \dots

E

中

f (⨆_{n \geq 0} d_{n}) ⊑ ⨆_{n \geq 0} f (d_{n})

成立.

例子8. 给定cpo

D

和

E

, 对于每个

e \in E

而言, 常函数

λ d \in D . e : D \to E

是连续的.

例子9. 当

D

是部分函数的domain

(State ⇀ State)

时 (见幻灯片24), 定义于幻灯片11的与

while

循环的指称语义有关的函数

f_{b, c} : D \to D

是一个连续函数. 我们将其验证留作练习.

例子10. 令

Ω

是垂直自然数的domain, 那么由

f (x) = {\begin{matrix} 0 & , 如果 x \in ℕ \\ ω & , 如果 x = ω \end{matrix}

定义的函数

f : Ω \to Ω

既是单调的也是严格的, 但是并非连续, 因为

f (⨆_{n \geq 0} n) = f (ω) = ω

然而

⨆_{n \geq 0} f (n) = ⨆_{n \geq 0} 0 = 0

第2.4节 Tarski不动点定理

Tarski不动点定理

令

f : D \to D

是domain

D

上的一个连续函数, 那么

$f$ 具有最小前不动点, 由 $fix (f) = ⨆_{n \geq 0} f^{n} (⊥)$ 给出.
于是, $fix (f)$ 也是 $f$ 的不动点, 因而是 $f$ 的最小不动点.

幻灯片29

幻灯片29给出了关于domain上的连续函数的关键结果, 其允许我们赋予牵涉递归特性的程序以指称语义. 幻灯片上所用的记号 $f^{n} (⊥)$ 是递归定义的: $f^{0} (⊥) \overset{def}{=} ⊥; f^{n + 1} (⊥) \overset{def}{=} f (f^{n} (⊥)) .$ 注意到既然 $\forall d \in D . ⊥ ⊑ d$ , 我们有 $f^{0} (⊥) = ⊥ ⊑ f^{1} (⊥)$ ; 而根据单调性, 又可以推出 $f^{n} (⊥) ⊑ f^{n + 1} (⊥) \Rightarrow f^{n + 1} (⊥) = f (f^{n} (⊥)) ⊑ f (f^{n + 1} (⊥)) = f^{n + 2} (⊥) .$ 因此, 通过对于 $n \in ℕ$ 进行归纳, 我们可以得到 $\forall n \in ℕ . f^{n} (⊥) ⊑ f^{n + 1} (⊥) .$ 换言之, 元素 $f^{n} (⊥)$ 构成了 $D$ 中的一条链. 所以说, 既然 $D$ 是cpo, 那么幻灯片29上用到的 $⨆_{n \geq 0} f^{n} (⊥)$ 的确是有意义的.

证明. 首先我们注意到

\begin{matrix} f (fix (f)) & = & f (⨆_{n \geq 0} f^{n} (⊥)) \\ = & ⨆_{n \geq 0} f (f^{n} (⊥)) & 根据 f 的连续性 \\ = & ⨆_{n \geq 0} f^{n + 1} (⊥) & 根据函数的幂次的定义 \\ = & ⨆_{n \geq 0} f^{n} (⊥) & 根据第2.3节的评注2 \\ = & fix (f) \end{matrix}

因此,

fix (f)

的确是

f

的一个不动点, 当然也就满足幻灯片19上的条件(lpf1). 为了验证(lpf2), 即前不动点的最小性, 我们设

d \in D

满足

f (d) ⊑ d

, 那么既然

⊥

在

D

是最小的, 可以得到

f^{0} (⊥) = ⊥ ⊑ d

并且

f^{n} (⊥) ⊑ d \Rightarrow f^{n + 1} (⊥) = f (f^{n} (⊥)) ⊑ f (d) ⊑ d

根据归纳, 我们可以推出

\forall n \in ℕ . f^{n} (⊥) ⊑ d

. 换言之,

d

是链的一个上界, 所以它大于等于最小上界, 即

fix (f) = ⨆_{n \geq 0} f^{n} (⊥) ⊑ d

这就是我们想要的(lpf2)了.

◻

例子1. 定义于幻灯片11上的函数

f_{⟦ B ⟧, ⟦ C ⟧}

是domain

(State ⇀ State)

上的一个连续函数, 因而我们可以应用Tarski不动点定理, 将

⟦ while B do C ⟧

定义为

fix (f_{⟦ B ⟧, ⟦ C ⟧})

. 实际上, 第1.2节中我们构造部分函数

w_{\infty}

的方法不过就是不动点定理的一个实例而已.

$⟦ while B do C ⟧$

\begin{array}{rcl} ⟦ while B do C ⟧ & = & fix (f_{⟦ B ⟧, ⟦ C ⟧}) \\ = & ⨆_{n \geq 0} f_{⟦ B ⟧, ⟦ C ⟧}^{n} (⊥) \\ = & λ s \in State . {\begin{matrix} {⟦ C ⟧}^{k} (s) & , 如果存在 k \geq 0 满足对于每个 0 \leq i < k 有 \\ ⟦ B ⟧ ({⟦ C ⟧}^{i} (s)) = true 而 ⟦ B ⟧ ({⟦ C ⟧}^{k} (s)) = false \\ undefined & , 如果对于每个 i \geq 0 有 ⟦ B ⟧ ({⟦ C ⟧}^{i} (s)) = true \end{matrix} \end{array}

幻灯片30

第2.5节练习

练习1. 验证幻灯片24上的断言.

练习2. 证明幻灯片25和27中的声明.

练习3. 验证例子9中

f_{b, c}

是连续函数的断言. 何时

f_{b, c}

是严格的?

译者注记. 以上练习皆相当平凡.

第3章 domain上的构造

本节我们将给出诸多构造domain和连续函数的方式, 实际上专注于PCF编程语言的指称语义所需的构造, PCF是本讲义的后半部分的研究对象. 注意到为了描述一个cpo, 我们必须先定义一个装备有某二元关系的集合, 然后证明

这个关系是一个偏序;
对于这个偏序集中所有的链, 其最小上界存在.

另外, 为了使得cpo成为一个domain, 我们还需要说明

存在最小的元素.

注意到既然链的最小上界以及最小元若存在则唯一, 那么cpo和domain完全由其基础集和偏序决定. [译注: 意味不明.] 之后我们将给出各种各样构造cpo和domain的方法, 而将验证i, ii, iii成立的任务留作练习.

第3.1节扁平domain

为了模拟PCF的基本类型 (ground type) $nat$ 和 $bool$ , 我们将使用幻灯片31给出的扁平domain的概念.

离散cpo和扁平domain

对于任意的集合

X

, 相等关系

x ⊑ x^{'} \overset{def}{\Leftrightarrow} x = x^{'}

使得

(X, ⊑)

成为一个cpo, 其被称为以

X

为基础集的离散cpo.
令

X_{⊥} \overset{def}{=} X \cup {⊥}

, 其中

⊥

是某个不在

X

中的元素, 那么

d ⊑ d^{'} \overset{def}{\Leftrightarrow} (d = d^{'}) \lor (d = ⊥)

使得

(X_{⊥}, ⊑)

成为一个以

⊥

为最小元的domain, 其被称为由

X

确定的扁平domain.

幻灯片31

自然数的扁平domain $ℕ_{⊥}$ , 上一章的图1中我们就已描绘过其图像. 至于布尔值的扁平domain $𝔹_{⊥}$ , 其Hasse图为以下牵涉扁平domain的连续函数实例对于PCF的指称语义而言也是必要的, 我们将其验证留给读者作为练习.

命题1. 令

f : X ⇀ Y

是两个集合之间的部分函数, 那么

f_{⊥} (d) \overset{def}{=} {\begin{matrix} f (d) & , 如果 d \in X 且 f 定义于 d \\ ⊥ & , 如果 d \in X 而 f 在 d 上没有定义 \\ ⊥ & , 如果 d = ⊥ \end{matrix}

定义了相应扁平domain之间的连续函数

f_{⊥} : X_{⊥} \to Y_{⊥}

第3.2节 domain的积

cpo和domain的二元积

两个cpo

(D_{1}, ⊑_{1})

和

(D_{2}, ⊑_{2})

之积的基础集为

D_{1} \times D_{2} = {(d_{1}, d_{2}) | d_{1} \in D_{1} & d_{2} \in D_{2}}

而其上的偏序

⊑

定义如下

(d_{1}, d_{2}) ⊑ (d_{1}^{'}, d_{2}^{'}) \overset{def}{\Leftrightarrow} d_{1} ⊑_{1} d_{1}^{'} & d_{2} ⊑_{2} d_{2}^{'}

链的最小上界可以按照分量进行计算:

⨆_{n \geq 0} (d_{1, n}, d_{2, n}) = (⨆_{i \geq 0} d_{1, i}, ⨆_{j \geq 0} d_{2, j})

若

(D_{1}, ⊑_{1})

和

(D_{2}, ⊑_{2})

都是domain, 那么

(D_{1} \times D_{2}, ⊑)

也是一个domain, 并且

⊥_{D_{1} \times D_{2}} = (⊥_{D_{1}}, ⊥_{D_{2}})

幻灯片32

命题1. 投影和配对. 令

D_{1}

和

D_{2}

是cpo, 那么投影

π_{1} : D_{1} \times D_{2} \to D_{1}, (d_{1}, d_{2}) \mapsto d_{1}

和

π_{2} : D_{1} \times D_{2} \to D_{2}, (d_{1}, d_{2}) \mapsto d_{2}

是连续函数. 如果

f_{1} : D \to D_{1}

和

f_{2} : D \to D_{2}

是连续函数, 其中

D

是一个cpo, 那么

⟨ f_{1}, f_{2} ⟩ : D \to D_{1} \times D_{2}, d \mapsto (f_{1} (d), f_{2} (d))

是连续的.

证明. 这些函数的连续性可由幻灯片32上对于

D_{1} \times D_{2}

中的链的最小上界的刻画直接推出.

◻

命题2. 对于每个domain

D

, 函数

if : 𝔹_{⊥} \times (D \times D) \to D, (x, (d, d^{'})) \mapsto {\begin{matrix} d & , 如果 x = true \\ d^{'} & , 如果 x = false \\ ⊥_{D} & , 如果 x = ⊥ \end{matrix}

是连续的.

我们将会需要以下更一般的积构造.

定义3. 依赖积. 给定集合

I

, 设对于每个

i \in I

我们有一个cpo

(D_{i}, ⊑_{i})

, 那么这个cpo族之积为

基础集是集合 $D_{i}$ 的 $I$ 重笛卡尔积 $\prod_{i \in I} D_{i}$ , 其由所有这样的函数 $p$ 构成, $p$ 定义在 $I$ 上, 而 $p$ 在每个 $i \in I$ 处的值 $p (i) \in D_{i}$ ;
偏序 $⊑$ 为 $p ⊑ p^{'} \overset{def}{\Leftrightarrow} \forall i \in I . p (i) ⊑_{i} p^{'} (i) .$

就和二元积的情况一样,

(\prod_{i \in I} D_{i}, ⊑)

中的链的最小上界也可以逐分量计算: 如果

p_{0} ⊑ p_{1} ⊑ p_{2} ⊑ \dots

是积cpo中的一个链, 那么其最小上界是将每个

i \in I

映射至

D_{i}

中的链

p_{0} (i) ⊑ p_{1} (i) ⊑ p_{2} (i) ⊑ \dots

的最小上界的函数, 即

(⨆_{n \geq 0} p_{n}) (i) = ⨆_{n \geq 0} p_{n} (i), i \in I .

而且, 对于每个

i \in I

, 第

i

投影函数

π_{i} : \prod_{j \in I} D_{j} \to D_{i}, p \mapsto p (i)

是连续的. 如果每个

D_{i}

都是domain, 那么它们的积也是domain, 并且其最小元是将每个

i \in I

映射至

D_{i}

的最小元的函数.

两个参数的连续函数

命题. 令

D, E, F

是cpo, 那么函数

f : D \times E \to F

是单调的当且仅当其对于每个参数分别都是单调的:

\forall d, d^{'} \in D, e \in E . d ⊑ d^{'} \Rightarrow f (d, e) ⊑ f (d^{'}, e)

\forall d \in D, e, e^{'} \in E . e ⊑ e^{'} \Rightarrow f (d, e) ⊑ f (d, e^{'})

而且, 其是连续的当且仅当其对于每个参数分别都是连续的 [译注: 在单调的基础之上, 也就是对于每个参数分别都是保持链的最小上界的]:

f (⨆_{n \geq 0} d_{n}, e) = ⨆_{n \geq 0} f (d_{n}, e)

f (d, ⨆_{n \geq 0} e_{n}) = ⨆_{n \geq 0} f (d, e_{n})

幻灯片33

两个参数的连续函数: 推导规则

在 $f$ 单调的情况下, 我们有 $\frac{x ⊑ x^{'} y ⊑ y^{'}}{f (x, y) ⊑ f (x^{'}, y^{'})}$
在 $f$ 连续的情况下, 我们有 $\frac{}{f (⨆_{m \geq 0} x_{m}, ⨆_{n \geq 0} y_{n}) = ⨆_{k \geq 0} f (x_{k}, y_{k})}$

幻灯片34

证明. "仅当"的方向是直接的, 其证明依赖于简单的观察, 即

d ⊑ d^{'} \Rightarrow (d, e) ⊑ (d^{'}, e)

和

(⨆_{n \geq 0} d_{n}, e) = ⨆_{n \geq 0} (d_{n}, e)

, 以及它们之于右参数的对偶版本. 对于"当"的方向, 首先设

f

对于每个参数分别都是单调的, 那么如果

D \times E

中有

(d, e) ⊑ (d^{'}, e^{'})

, 根据二元积的定义, 我们可以推出

D

中有

d ⊑ d^{'}

而

E

中有

e ⊑ e^{'}

, 因此

\begin{matrix} f (d, e) & ⊑ & f (d^{'}, e) & 根据对于第一个参数的单调性 \\ ⊑ & f (d^{'}, e^{'}) & 根据对于第二个参数的单调性 \end{matrix}

于是,

f (d, e) ⊑ f (d^{'}, e^{'})

, 即

f

是单调函数.
现在设

f

对于每个参数分别都是连续的, 那么如果

(d_{0}, e_{0}) ⊑ (d_{1}, e_{1}) ⊑ (d_{2}, e_{2}) ⊑ \dots

是二元积中的一个链, 我们有

\begin{matrix} f (⨆_{n \geq 0} (d_{n}, e_{n})) & = & f (⨆_{i \geq 0} d_{i}, ⨆_{j \geq 0} e_{j}) & 见幻灯片32 \\ = & ⨆_{i \geq 0} f (d_{i}, ⨆_{j \geq 0} e_{j}) & 根据对于第一个参数的连续性 \\ = & ⨆_{i \geq 0} ⨆_{j \geq 0} f (d_{i}, e_{j}) & 根据对于第二个参数的连续性 \\ = & ⨆_{n \geq 0} f (d_{n}, e_{n}) & 根据幻灯片27上的引理 \end{matrix}

而这就说明了

f

的连续性.

◻

第3.3节函数domain

两个cpo/domain之间的所有连续函数的集合可以赋予一个偏序而成为一个cpo/domain, 见幻灯片35. 有时我们也用术语"指数cpo/domain (exponential cpo/domain)"而不是"函数cpo/domain".

函数cpo和domain

给定cpo

(D, ⊑_{D})

和

(E, ⊑_{E})

, 函数cpo

(D \to E, ⊑)

的基础集为 [译注: 以下符号有点过载]

(D \to E) \overset{def}{=} {f : D \to E | f 连续}

而偏序为

f ⊑ f^{'} \overset{def}{\Leftrightarrow} \forall d \in D . f (d) ⊑_{E} f^{'} (d)

推导规则:

\frac{f ⊑_{(D \to E)} g x ⊑_{D} y}{f (x) ⊑_{E} g (y)}

幻灯片35

函数cpo和domain (续)

链的最小上界可以逐参数计算:

⨆_{n \geq 0} f_{n} = λ d \in D . ⨆_{n \geq 0} f_{n} (d)

推导规则:

\frac{}{(⨆_{n \geq 0} f_{n}) (⨆_{n \geq 0} x_{n}) = ⨆_{k \geq 0} f_{k} (x_{k})}

如果

D

和

E

还是domain, 那么

D \to E

也成为一个domain, 并且最小元为

⊥_{D \to E} : D \to E, d \mapsto ⊥_{E} .

幻灯片36

证明. 我们应该证明函数的链

⨆_{n \geq 0} f_{n}

的最小上界是连续的. 这个证明使用了幻灯片27的互换律 (interchange law). 对于

D

中的一个链

d_{0} ⊑ d_{1} ⊑ d_{2} ⊑ \dots

, 我们有

\begin{matrix} (⨆_{n \geq 0} f_{n}) (⨆_{m \geq 0} d_{m}) & = & ⨆_{n \geq 0} f_{n} (⨆_{m \geq 0} d_{m}) & ⨆_{n \geq 0} f_{n} 的定义 \\ = & ⨆_{n \geq 0} (⨆_{m \geq 0} f_{n} (d_{m})) & 每个 f_{n} 的连续性 \\ = & ⨆_{m \geq 0} (⨆_{n \geq 0} f_{n} (d_{m})) & 互换律 \\ = & ⨆_{m \geq 0} ((⨆_{n \geq 0} f_{n}) (d_{m})) & ⨆_{n \geq 0} f_{n} 的定义 \end{matrix}

◻

译者注记. 这个证明有点没头没脑, 所以我感到有必要写下注记. 原文写的是这是对于幻灯片35的证明, 这实际上就足够令人费解的了. 毕竟幻灯片35是一个定义, 那么需要证明什么呢? 这个证明的目的实际上是为了补足定义里的一点gap, 以使得定义的确是well-defined的. (译者很有先见之明的给幻灯片36取了合适的标题, 而的确要证明的内容和幻灯片36有关.) 我们知道一个cpo需要能够对于(升)链作最小上界操作, 而幻灯片36只是指出可以这么计算该操作, 没有说明这个计算结果的确是最小上界操作. 这个证明比较令人迷惑的地方主要是在证明之前就使用了

⨆_{n \geq 0} f_{n}

这种符号, 实际上在证明的过程之中你不应该把它视为最小上界. 另外, 这个证明只是论证了保持最小上界这一性质, 其他还需要论证的内容是单调性, 然后在连续的基础之上说明这个计算结果的确是链的上界且是上界之中最小的. 当然, 额外的内容并不困难, 只是因为先前证明总是过分细致而显得这里省略这么多内容让译者感到有点奇怪.

命题1. 求值和Curry化. 给定cpo

D

和

E

, 函数

ev : (D \to E) \times D \to E, (f, d) \mapsto f (d)

是连续的. 给定任意的连续函数

f : D^{'} \times D \to E

(其中

D^{'}

是一个cpo), 对于每个

d^{'} \in D^{'}

, 函数

d \in D \mapsto f (d^{'}, d)

都是连续的, 因而确定了函数cpo

D \to E

中的一个元素. 我们将其记为

cur (f) (d^{'})

, 那么

cur (f) : D^{'} \to (D \to E), d^{'} \mapsto λ d \in D . f (d^{'}, d)

是一个连续函数. [原注: Curry化这个名字是为了纪念逻辑学家H. B. Curry, 一位组合子逻辑和lambda演算先驱.]

证明. 对于

ev

的连续性, 注意到

\begin{matrix} ev (⨆_{n \geq 0} (f_{n}, d_{n})) & = & ev (⨆_{i \geq 0} f_{i}, ⨆_{j \geq 0} d_{j}) & 积的最小上界是逐分量计算的 \\ = & (⨆_{i \geq 0} f_{i}) (⨆_{j \geq 0} d_{j}) & 根据 ev 的定义 \\ = & ⨆_{i \geq 0} f_{i} (⨆_{j \geq 0} d_{j}) & 函数cpo中的最小上界是逐参数计算的 \\ = & ⨆_{i \geq 0} ⨆_{j \geq 0} f_{i} (d_{j}) & 根据每个 f_{i} 的连续性 \\ = & ⨆_{n \geq 0} f_{n} (d_{n}) & 根据幻灯片27的引理 \\ = & ⨆_{n \geq 0} ev (f_{n}, d_{n}) & 根据 ev 的定义 \end{matrix}

每个

cur (f) (d^{'})

以及然后

cur (f)

的连续性可以由

D_{1} \times D_{2}

中的链的最小上界可以逐分量计算这一事实立即推出.

◻

复合的连续性

对于cpo

D, E, F

, 复合函数

\circ : ((E \to F) \times (D \to E)) \to (D \to F)

是连续的, 其定义为对于

f \in (D \to E)

和

g \in (E \to F)

g \circ f = λ d \in D . g (f (d)) .

幻灯片37

不动点算子的连续性

令

D

是一个domain.
根据Tarski不动点定理, 我们知道每个连续函数

f \in (D \to D)

都拥有一个最小不动点

fix (f) \in D

命题. 函数

fix : (D \to D) \to D

是连续的.

幻灯片38

证明. 我们必须首先证明

fix : (D \to D) \to D

是一个单调函数. 设

f_{1} ⊑ f_{2}

是函数domain中的两个元素. 我们需要证明的是

fix (f_{1}) ⊑ fix (f_{2})

, 不过

\begin{matrix} f_{1} (fix (f_{2})) & ⊑ & f_{2} (fix (f_{2})) & 鉴于 f_{1} ⊑ f_{2} \\ ⊑ & fix (f_{2}) & 根据 fix (f_{2}) 的(lpf1) \end{matrix}

于是,

fix (f_{2})

是

f_{1}

的一个前不动点, 因而根据

fix (f_{1})

的(lpf2)我们有

fix (f_{1}) ⊑ fix (f_{2})

, 这也正是我们想要的. [译注: 作者这里将lpf均误作lfp, 而lfp在书中并没有出现过, 证明的剩余部分也都写错了. 另外, 读者应该回忆一下, 根据之前的命题, 此时最小前不动点和最小不动点均存在且相等.]
现在我们将注意力转向证明链的最小上界的保持, 设

D \to D

中有

f_{0} ⊑ f_{1} ⊑ f_{2} ⊑ \dots

. 根据第2章第3节的评注7, 我们只需要证明

fix (⨆_{n \geq 0} f_{n}) ⊑ ⨆_{n \geq 0} fix (f_{n})

而根据最小前不动点的(lpf2), 证明

⨆_{n \geq 0} fix (f_{n})

是

⨆_{n \geq 0} f_{n}

的一个前不动点就足够了. [译注: 即最小前不动点小于其他的前不动点.] 这是因为:

\begin{matrix} (⨆_{m \geq 0} f_{m}) (⨆_{n \geq 0} fix (f_{n})) & = & ⨆_{m \geq 0} f_{m} (⨆_{n \geq 0} fix (f_{n})) & 函数链的最小上界可以逐参数计算 \\ = & ⨆_{m \geq 0} ⨆_{n \geq 0} f_{m} (fix (f_{n})) & 鉴于每个 f_{m} 都是连续的 \\ = & ⨆_{k \geq 0} f_{k} (fix (f_{k})) & 根据幻灯片27的引理 \\ ⊑ & ⨆_{k \geq 0} fix (f_{k}) & 根据每个 f_{k} 的(lpf1) \end{matrix}

[译注: 这里根据幻灯片27的引理需要用到之前证明的单调性, 另外最后一步这里的

⊑

实际上更确切地说是

=

, 因为

fix

是不动点算子, 不过这个证明的所有地方作者都把最小不动点当作最小前不动点使用.]

◻

第3.4节练习

练习1. 验证本章未经证明的构造, 证明本章未经证明的命题.

练习2. 令

X

和

Y

是集合而

X_{⊥}

和

Y_{⊥}

是对应的扁平domain, 如幻灯片31. 证明一个函数

f : X_{⊥} \to Y_{⊥}

是连续的当且仅当以下条件之一成立:

$f$ 是严格的, 即 $f (⊥) = ⊥$ ;
$f$ 是常函数, 即 $\forall x \in X . f (x) = f (⊥)$ .

练习3. 令

{⊤}

是一个单元素集合, 而

{⊤}_{⊥}

是相对应的扁平domain. 令

Ω

是图1所描绘的垂直自然数的domain. 证明函数domain

(Ω \to {⊤}_{⊥})

和

Ω

之间存在一个双射.

练习4. 证明幻灯片37的内容.

第4章 Scott归纳

第4.1节链封闭子集和可容许子集

在第2章的时候我们看到一个domain $D$ 上的一个连续函数 $f : D \to D$ 的最小不动点可以表达为自 $D$ 的最小元素 $⊥$ 起反复应用 $f$ 所得到的链的最小上界: $fix (f) = ⨆_{n \geq 0} f^{n} (⊥)$ . 这种构造允许我们使用特定方式证明 $fix (f)$ 的性质, 只要这个性质满足幻灯片39中的条件, 证明方式为使用数学归纳法表明对于每个 $n$ 而言 $f^{n} (⊥)$ 具有该性质. 或许将这种对于数学归纳法的使用方式打包以隐藏 $fix (f)$ 作为某个链的不动点的显式构造也是方便的, 见幻灯片40. 为了澄清幻灯片40的陈述, 注意到 $f^{0} (⊥) = ⊥ \in S$ , 此为基本步骤; 而 $f^{n} (⊥) \in S$ 可以推出 $f^{n + 1} (⊥) = f (f^{n} (⊥)) \in S$ , 此为归纳步骤; 因此, 根据 $n$ 上的归纳, 我们有 $\forall n \geq 0 . f^{n} (⊥) \in S$ . 最后, 根据 $S$ 的链封闭性, $fix (f) = ⨆_{n \geq 0} f^{n} (⊥) \in S$ , 这正是我们所要的.

链封闭子集和可容许子集

令

D

是一个cpo. 一个子集

S \subseteq D

被称为是链封闭的当且仅当对于

D

中所有的链

d_{0} ⊑ d_{1} ⊑ d_{2} ⊑ \dots

, 有

(\forall n \geq 0 . d_{n} \in S) \Rightarrow (⨆_{n \geq 0} d_{n}) \in S

如果

D

是一个domain,

S \subseteq D

被称为是可容许的当且仅当其是

D

的一个链封闭子集且

⊥ \in S

元素

d \in D

的一个性质

Φ (d)

被称为是链封闭的当且仅当

{d \in D | Φ (d)}

是

D

的一个链封闭子集, 类似地还可以定义可容许性质.

幻灯片39

译者注记. 所谓(

D

上的)性质指的是一个从

D

到真假的函数, 这是一种外延性的观念. 另外, 正如幻灯片39,

D

上的一个性质

Φ

也可以由子集

{d \in D | Φ (d)}

表示, 这和函数表示是完全等价的.

注记. 术语inclusive或者inductive经常用作链封闭的同义词.

例子1. 考虑图1所描绘的垂直自然数的domain

Ω

, 那么

$Ω$ 的任意有限子集都是链封闭的;
${0, 2, 4, 6, \dots}$ 不是 $Ω$ 的一个链封闭子集;
${0, 2, 4, 6, \dots} \cup {ω}$ 是 $Ω$ 的一个链封闭子集, 当然其也是一个可容许子集.

Scott的不动点归纳原理

令

f : D \to D

是domain

D

上的一个连续函数.
对于任意的可容许子集

S \subseteq D

, 为了证明

f

的最小不动点在

S

之中, 即

fix (f) \in S

实际上证明

\forall d \in D . d \in S \Rightarrow f (d) \in S

就足够了.

幻灯片40

译者注记. 约定俗成地, 点号代表辖域尽可能向右延伸.

在实际情况下应用Scott的不动点归纳原理的难点在于识别出一个适切的可容许子集 $S$ , 即寻找一个具有合适强度的归纳假设.

第4.2节例子

例子1. 设

D

是一个domain而

f : (D \times (D \times D)) \to D

是一个连续函数. 令

g : (D \times D) \to (D \times D)

是由

g (d_{1}, d_{2}) \overset{def}{=} (f (d_{1}, (d_{1}, d_{2})), f (d_{1}, (d_{2}, d_{2}))), 其中 d_{1}, d_{2} \in D

定义的连续函数. 那么,

u_{1} = u_{2}

, 其中

(u_{1}, u_{2}) \overset{def}{=} fix (g)

. (注意到之所以

g

是连续的, 是因为我们可以将其表达为复合, 投影和配对, 因而可以应用第3章第2节的命题1和幻灯片37:

g = ⟨ f \circ ⟨ π_{1}, ⟨ π_{1}, π_{2} ⟩ ⟩, f \circ ⟨ π_{1}, ⟨ π_{2}, π_{2} ⟩ ⟩ ⟩

证明. 我们想要证明的是

fix (g) \in Δ

, 其中

Δ \overset{def}{=} {(d_{1}, d_{2}) \in D \times D | d_{1} = d_{2}} .

不难看出

Δ

是积domain

D \times D

的一个可容许子集. 因此, 根据Scott不动点归纳原理, 我们只需要检验

\forall (d_{1}, d_{2}) \in D \times D . (d_{1}, d_{2}) \in Δ \Rightarrow g (d_{1}, d_{2}) \in Δ

其等价于

\forall (d_{1}, d_{2}) \in D \times D . d_{1} = d_{2} \Rightarrow f (d_{1}, d_{1}, d_{2}) = f (d_{1}, d_{2}, d_{2})

这显然为真.

◻

接下来的例子表明Scott归纳原理对于证明关于程序的(指称版本的)部分正确性(partial correctness)断言来说很有用, 即具有形式如果程序终止, 那么对于结果来说这个那个的性质成立的断言. 与之形成对比的是, 完全正确性断言指的是程序的确会终止且对于结果来说这个那个的性质成立. 鉴于Scott归纳只能应用于这样的性质 $Φ$ , 其满足 $Φ (⊥)$ 成立, 所以说它对于证明完全正确性不是很有用.

例子2. 令

f : D \to D

是幻灯片12上定义的连续函数, 其最小不动点是命令

while X > 0 do (Y ≔ X ⁎ Y; X ≔ X - 1)

的指称. 我们将会使用Scott归纳证明

\forall x, y \geq 0 . fix (f) [X \mapsto x, Y \mapsto y] ↓ \Rightarrow fix (f) [X \mapsto x, Y \mapsto y] = [X \mapsto 0, Y \mapsto (! x) ⁎ y]

其中

第4.3节构建链封闭子集

Scott归纳的威力依赖于我们有许多链封闭子集储备能用. 幸运的是, 我们可以根据构造方式来保证许多子集是链封闭的.

第4.3.1小节基本关系

令 $D$ 是一个cpo. $D \times D$ 的子集 ${(x, y) \in D \times D | x ⊑ y}$ 和 ${(x, y) \in D \times D | x = y}$ 都是链封闭的 (为什么?). 换言之, $D \times D$ 上的性质 (或者说谓词) $x ⊑ y$ 和 $x = y$ 都确定了链封闭集合.

译者注记. 对于

D

中的两个链

x_{0} ⊑ x_{1} ⊑ x_{2} ⊑ \dots

和

y_{0} ⊑ y_{1} ⊑ y_{2} ⊑ \dots

, 如果对于每个

n \in ℕ

都有

x_{n} ⊑ y_{n}

, 那么

⨆_{n \in ℕ} x_{n} ⊑ ⨆_{n \in ℕ} y_{n} .

例子I: 最小前不动点性质

令

D

是一个domain而

f : D \to D

是一个连续函数, 那么

\forall d \in D . f (d) ⊑ d ⟹ fix (f) ⊑ d .

以下是使用Scott归纳的证明.

证明. 令

d \in D

是

f

的一个前不动点, 那么

\begin{array}{rcl} x \in ↓ (d) & ⟹ & x ⊑ d \\ ⟹ & f (x) ⊑ f (d) \\ ⟹ & f (x) ⊑ d \\ ⟹ & f (x) \in ↓ (d) \end{array}

因此, 我们有

fix (f) \in ↓ (d) .

◻

幻灯片41

译者注记. 译者猜测这里使用

⟹

而非

\Rightarrow

的原因在于

⟹

相当于断言

\Rightarrow

为真. 另外, 幻灯片41有很多令译者感到奇怪的地方. 当然, 最奇怪的地方还是证明的命题是定义的一部分, 最小前不动点本来就应该小于其他不动点. 至于存在性之前读者已经看过证明了. 并且因为之前我们一起证明了最小前不动点和最小不动点均存在且相等, 所以说这里的Scott归纳的确也可以应用于最小前不动点. 不过, 实际上如果不看这个幻灯片的标题, 我们肯定会将

fix (f)

当成最小不动点. 而且, 证明的具体内容里本来就没有牵涉不动点和前不动点. 当然, 这是因为其被掩藏在了Scott归纳的抽象之下. 这个证明还有一些gap值得注意. 首先是

↓ (d)

没有在书中任何地方得到定义, 不过按照格论的习惯其定义应该为

↓ (d) ≔ {x \in D | x ⊑ d} .

其次, 这个证明未经验证地使用了所有

↓ (d)

均为可容许子集这一事实. 不过, 这当然是显然的. 对于

↓ (d)

中的任意链

x_{0} ⊑ x_{1} ⊑ x_{2} ⊑ \dots

, 鉴于每个

x_{n} ⊑ d

, 故

⨆_{n \in ℕ} x_{n} ⊑ d

即

⨆_{n \in ℕ} x_{n} \in ↓ (d)

. 另外, 因为

⊥ ⊑ d

, 所以

⊥ \in ↓ (d)

第4.3.2小节逆像和替换

令 $f : D \to E$ 是cpo $D$ 和 $E$ 之间的一个连续函数. 设 $S$ 是 $E$ 的一个链封闭子集, 那么逆像 $f^{- 1} (S) = {x \in D | f (x) \in S}$ 是 $D$ 的一个链封闭子集 (为什么?).

译者注记. 设

S

是

E

的一个链封闭子集, 对于

f^{- 1} (S)

中的链

x_{0} ⊑ x_{1} ⊑ x_{2} ⊑ \dots

, 考虑其最小上界在

f

下的像

f (⨆_{n \in ℕ} x_{n})

我们希望其是

S

的一个元素, 而这实际上是显然的. 根据

f

的连续性, 我们知道

f (⨆_{n \in ℕ} x_{n}) = ⨆_{n \in ℕ} f (x_{n})

鉴于

S

是一个链封闭子集, 且对于每个

n \in ℕ

f (x_{n}) \in S

, 故

⨆_{n \in ℕ} f (x_{n}) \in S

也就是说, 我们有

⨆_{n \in ℕ} x_{n} \in f^{- 1} (S)

那么, 我们可以断言

f^{- 1} (S)

是一个链封闭子集. 译注完毕.

设子集 $S$ 由 $E$ 上的性质 $P$ 所定义, 即 $S = {y \in E | P (y)}$ 那么 $f^{- 1} (S) = {x \in D | P (f (x))}$ 也就是说, 若 $E$ 上的性质 $P (y)$ 确定了 $E$ 的一个链封闭子集, 而 $f : D \to E$ 是一个连续函数, 那么 $D$ 上的性质 $P (f (x))$ 确定了 $D$ 的一个链封闭子集.

例子II

令

D

是一个domain而

f, g : D \to D

是连续函数并且满足

f \circ g ⊑ g \circ f

, 那么

f (⊥) ⊑ g (⊥) ⟹ fix (f) ⊑ fix (g) .

以下是使用Scott归纳的证明.

证明. 考虑

D

的可容许性质

Φ (x) \equiv (f (x) ⊑ g (x))

鉴于

f (x) ⊑ g (x) \Rightarrow g (f (x)) ⊑ g (g (x)) \Rightarrow f (g (x)) ⊑ g (g (x))

我们有

f (fix (g)) ⊑ g (fix (g)) .

◻

幻灯片42

译者注记. 我们继续补齐一点gap. 鉴于

g (fix (g)) = fix (g)

故

f (fix (g)) ⊑ fix (g)

换言之,

fix (g)

是

f

的一个前不动点. 然而

fix (f)

是

f

的最小前不动点, 所以有

fix (f) ⊑ fix (g) .

第4.3.3小节逻辑运算

令 $D$ 是一个cpo. 令 $S \subseteq D$ 和 $T \subseteq D$ 是 $D$ 的链封闭子集. 那么, 我们有 $S \cup T 和 S \cap T$ 都是链封闭子集 (为什么?). 若是基于性质的语言, 若 $P (x)$ 和 $Q (x)$ 都确定了 $D$ 的链封闭子集, 那么 $P (x) 或者 Q (x), P (x) & Q (x)$ 也是如此.

如果 $S_{i}, i \in I$ 是由集合 $I$ 索引的 $D$ 的一个链封闭子集的族, 那么 $⋂_{i \in I} S_{i}$ 是 $D$ 的一个链封闭子集 (为什么?).

译者注记. (不论有限还是无限的)交的情况比较简单, 并的情况比较有趣. 对于

S \cup T

中的链

x_{0} ⊑ x_{1} ⊑ x_{2} ⊑ \dots

, 我们可以按照是否属于

S

进行分类. 至少其中一类是无限的, 设其构成了(子)链

y_{0} ⊑ y_{1} ⊑ y_{2} ⊑ \dots

. 我们知道

⨆_{n \in ℕ} y_{n}

肯定是属于

S \cup T

的, 若是能够证明

⨆_{n \in ℕ} y_{n} = ⨆_{n \in ℕ} x_{n}

那么就结束了. 首先鉴于

{y_{0}, y_{1}, \dots}

是

{x_{0}, x_{1}, \dots}

的一个子集, 所以

⨆_{n \in ℕ} y_{n} ⊑ ⨆_{n \in ℕ} x_{n}

那么我们需要证明的是

⨆_{n \in ℕ} x_{n} ⊑ ⨆_{n \in ℕ} y_{n}

实际上对于任意的

i \in ℕ

, 鉴于子链

y_{0} ⊑ y_{1} ⊑ y_{2} ⊑ \dots

的长度是无限的, 所以必然可以找到某个

j \in ℕ

使得

x_{i} ⊑ y_{j}

, 那么可以看出

⨆_{n \in ℕ} y_{n}

是

x_{0} ⊑ x_{1} ⊑ x_{2} ⊑ \dots

的一个上界, 也就是说

⨆_{n \in ℕ} x_{n} ⊑ ⨆_{n \in ℕ} y_{n} .

说明完毕, 以下是正文.

因此, 如果一个性质 $P (x, y)$ 确定了 $D \times E$ 的一个链封闭子集, 那么性质 $\forall x \in D . P (x, y)$ 确定了 $E$ 的一个链封闭子集. 这是因为 $\begin{array}{rcl} {y \in E | \forall x \in D . P (x, y)} & = & ⋂_{d \in D} {y \in E | P (d, y)} \\ = & ⋂_{d \in D} {f_{d}}^{- 1} {(x, y) \in D \times E | P (x, y)} \end{array}$ 其中 $f_{d} : E \to D \times E$ 是连续函数, 定义为对于每个 $d \in D$ , $f_{d} (y) = (d, y)$ .

实际上, 若称形式为 $f (x_{1}, \dots, x_{k}) ⊑ g (x_{1}, \dots, x_{l})$ 或 $f (x_{1}, \dots, x_{k}) = g (x_{1}, \dots, x_{l})$ 的性质为基本性质 (其中 $f$ 和 $g$ 为连续函数), 那么对于由基本性质的合取与析取构成的东西进行其中一些变量的全称量化, 那么就会确定非量化的变量所对应的积cpo的一个链封闭子集.

译者注记.

不过, 注意到链封闭子集的无限并不必然是链封闭的; 有限子集总是链完备的, 但是其任意的并不是. 因此, 一般情况下我们不能使用存在量化构造链封闭子集.

第4.4节练习

练习1.

第5章 PCF

语言PCF (Programming Computable Functions, 编程可计算函数) 是一个简单的函数式编程语言, 其经常用作指称语义和操作语义的理论建立中的示例语言, 也包括这两种语义之间的关系的理论. 其句法是由Dana Scott于大约1969年引入的, 作为Logic of Computable Functions (可计算函数逻辑)的一部分, 其也在具有高度影响力的论文Plotkin (1977) 里作为一种编程语言被研究.

本章将给出我们在这个讲义里所使用的PCF的某个特定版本的句法和操作语义. 而在第6章中我们将看到如何使用domain和连续函数来赋予它一个指称语义.

第5.1节项和类型

PCF语言的类型, 表达式, 项在幻灯片43中定义.

PCF句法

类型

τ ⩴ nat | bool | τ \to τ

表达式

\begin{matrix} M & ⩴ & 0 | succ (M) | pred (M) \\ | & true | false | zero (M) \\ | & x | if M then M else M \\ | & fn x : τ . M | M M | fix (M) \end{matrix}

其中

x \in 𝕍

, 一个变量无限集合.
技术细节: 我们在绑定变量的

α

变换的意义下将表达式视为等同的, 而绑定变量是由

fn

表达式构造子创建的: 根据定义一个PCF项是一个表达式的

α

等价类.

幻灯片43

各种句法形式的意义如下.

$nat$ 是自然数 $0, 1, 2, 3, \dots$ 的类型.

指称语义学讲义

前言

推荐书目

深入阅读

第1章引论

第1.1节指称语义的基本例子

第1.2节例子: 作为不动点的 $while$ 循环

第1.3节练习

第2章最小不动点

第2.1节偏序集和单调函数

第2.1.1小节偏序集

第2.1.2小节单调函数

第2.2节最小元和前不动点 (pre-fixed point)

第2.3节完全偏序 (cpo) 和连续函数

第2.3.1小节 domain

第2.3.2小节连续函数

第2.4节 Tarski不动点定理

第2.5节练习

第3章 domain上的构造

第3.1节扁平domain

第3.2节 domain的积

第3.3节函数domain

第3.4节练习

第4章 Scott归纳

第4.1节链封闭子集和可容许子集

第4.2节例子

第4.3节构建链封闭子集

第4.3.1小节基本关系

第4.3.2小节逆像和替换

第4.3.3小节逻辑运算

第4.4节练习

第5章 PCF

第5.1节项和类型

第6章 PCF的指称语义

第7章将指称语义和操作语义联系起来

第8章完全抽象

指称语义学讲义

前言

推荐书目

深入阅读

第1章 引论

第1.1节 指称语义的基本例子

第1.2节 例子: 作为不动点的while循环

第1.3节 练习

第2章 最小不动点

第2.1节 偏序集和单调函数

第2.1.1小节 偏序集

第2.1.2小节 单调函数

第2.2节 最小元和前不动点 (pre-fixed point)

第2.3节 完全偏序 (cpo) 和连续函数

第2.3.1小节 domain

第2.3.2小节 连续函数

第2.4节 Tarski不动点定理

第2.5节 练习

第3章 domain上的构造

第3.1节 扁平domain

第3.2节 domain的积

第3.3节 函数domain

第3.4节 练习

第4章 Scott归纳

第4.1节 链封闭子集和可容许子集

第4.2节 例子

第4.3节 构建链封闭子集

第4.3.1小节 基本关系

第4.3.2小节 逆像和替换

第4.3.3小节 逻辑运算

第4.4节 练习

第5章 PCF

第5.1节 项和类型

第6章 PCF的指称语义

第7章 将指称语义和操作语义联系起来

第8章 完全抽象

第1章引论

第1.1节指称语义的基本例子

第1.2节例子: 作为不动点的 $while$ 循环

第1.3节练习

第2章最小不动点

第2.1节偏序集和单调函数

第2.1.1小节偏序集

第2.1.2小节单调函数

第2.2节最小元和前不动点 (pre-fixed point)

第2.3节完全偏序 (cpo) 和连续函数

第2.3.2小节连续函数

第2.5节练习

第3.1节扁平domain

第3.3节函数domain

第3.4节练习

第4.1节链封闭子集和可容许子集

第4.2节例子

第4.3节构建链封闭子集

第4.3.1小节基本关系

第4.3.2小节逆像和替换

第4.3.3小节逻辑运算

第4.4节练习

第5.1节项和类型

第7章将指称语义和操作语义联系起来

第8章完全抽象