指称语义学讲义

前言

我们的目的在于介绍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

证明.

◻

指称语义学讲义

前言

推荐书目

深入阅读

第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

第4章 Scott归纳

第5章 PCF

第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

第4章 Scott归纳

第5章 PCF

第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

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

第8章完全抽象