函数式编程的domain论基础

前言

这本小书是我过去十年间为Technical University Darmstadt的数学系和计算机系学生开设的一门课程的产物. 这门课程的目的在于为想要撰写指称语义领域的硕士论文或者想要在这个领域开始PhD生涯的学生提供坚实的基础. 对于后一个目的而言, 本书也在University of Birmingham (UK) 由Martin Escardó的学生成功地运用.

因此, 我认为这本小册子很好地满足了预想的目标, 即填补介绍性教科书 (例如[Winskel 1993]) 和指称语义领域的诸多研究性论文之间的沟壑. 我有意专注于基于domain论的指称语义, 而忽略了近来的博弈语义(Game Semantics) (见[Hyland and Ong 2000; Abramsky et al. 2000]), 在某种意义上其坐落于操作语义和指称语义之间. 这种选择的理由一方面在于博弈语义在[McCusker 1998]里已经很好地涵盖了, 另一方面在于我发现基于domain的语义在数学上相比其他方法更加简单, 因为其本质更加抽象而更少组合 (combinatorial). 当然, 这种偏好是有些主观性的, 但是我的借口在于我们写书应该写人们更不熟悉的领域, 而不是写那些已经广为人知的领域.

我们建立我们的主题的方式是研究为人熟知的函数式的内核语言PCF, 其由Dana Scott于1960年代末引入. 第2章和第3章中我们设置了本书的场景 (scene), 这两章分别引入了PCF的操作语义和domain语义. 之后我们专注于以越来越精细的逻辑关系技术来研究操作语义和domain语义之间的关系, 而这在第11章和第12章中对于PCF的完全抽象模型的构造里达到顶峰. 我认为我们对于完全抽象模型的构造比既有文献中的记述更加优雅和简明, 然而当然其也是基于那些文献的. 稍微偏离了主线地, 我们也呈现了如何以Scott domain解释递归类型 (第9章) 以及给出了基于Scott domain对于可计算性的描述 (第13章), 其中我们证明了[Plotkin 1977]的经典定理,

第1章引论

函数式编程语言基本上和更为人熟知的命令式语言 (例如FORTRAN, PASCAL, C, 等等) 一样古老. 最古老的函数式语言是LISP, 其由John McCarthy于1950年代建立, 即基本上和FORTRAN同时. 尽管像FORTRAN这样的命令式或者说面向状态语言是为了数值计算的目的而建立的, 诸如LISP这样的函数式编程语言的意图应用领域是 (并且至今仍然是) 对于诸如列表, 树等符号性数据的算法性操纵.

命令式语言的基本构造是修改状态的命令 (例如赋值 $x ≔ E$ ) 和命令的条件性迭代 (例如 $while$ 循环). 而且, 命令式语言对于诸如数组这样的随机访问数据结构有着强力的支持, 这在数值计算中是重要的.

然而, 在纯函数式语言之中, 并不存在状态或者状态改变指称的概念. 其基本概念是

一个函数之于一个参数的应用
函数的定义, 要么显式地 (例如 $f (x) = x ⁎ x + 1$ ), 要么递归地 (例如 $f (x) = if x = 0 then 1 else x ⁎ f (x - 1) fi$ ).

这些例子表明除了除了函数的应用和定义, 我们还需要基本数据类型 (例如自然数或者布尔) 上的基本操作以及用于分类讨论定义的条件式. 而且, 所有常见的函数式编程语言 (例如LISP, Scheme, (S)ML, Haskell, 等等) 都提供了通过显式列举构造子来定义递归数据类型的机制, 例如在以下对于二叉树的数据类型的定义里

tree = empty () | mk_tree (tree, tree)

empty

是对于没有儿子的空树的一个

0

元构造子, 而

mk_tree

是一个二元构造子, 其取两个树

t_{1}

和

t_{2}

, 然后构造一个新的树, 其根的左右儿子分别是

t_{1}

和

t_{2}

. 因此, 函数式语言不仅支持函数的递归定义, 也支持数据类型的递归定义. 后一个特点应该被认为是相较于PASCAL这样的命令式语言的一大优势, 其中的递归数据类型需要通过指针来实现, 这是精细的工作, 也是引入难以消除的微妙错误的一个源头.

命令式程序开发的典型方法是设计流程图(flow chart), 其描述并可视化了程序的动态行为. 因此, 命令式语言编程的主要任务是组合复杂的动态行为, 也就是所谓的控制流.

然而, 在函数式编程语言里, 程序的动态行为无需显式描述. 转而, 人们只需要定义要被实现的函数. 当然, 在实践中, 这些函数定义是相当层次性的, 即基于一整个预先定义的辅助函数的级联. 然后, 一个程序 (与一个函数定义相对) 通常具有应用 $f (e_{1}, \dots, e_{n})$ 的形式, 其会由解释器求值. 鉴于在函数式语言中编程基本上由定义函数 (显式地或者递归地) 构成, 我们无需担心执行的动态方面, 因为这项任务被解释器完全接管了. 因此, 在函数式语言中编程时我们可以专注于what而忘记how. 然而, 当在函数式编程语言中定义函数时, 我们不得不拘泥于 (stick to) 由语言所提供的定义形式, 而不能使用日常数学中通常的集合论语言.

在这个课程讲义之中, 我们将分别就以下三个方面探究函数式的(内核)语言.或者特别是, 这些方面时如何交互的.

首先, 我们将会引入一个最简单的函数式编程语言, 即带有自然数作为基本类型但没有一般性的递归类型的PCF (Programming Computable Functionals).

PCF的操作语义将由一个归纳定义的求值关系 $E ⇓ V$ 给出, 其刻画了哪个表达式 $E$ 会求值至哪个值, 而值是不能被进一步求值的特定表达式. 例如, 如果 $E ⇓ V$ 而 $E$ 是一个具有自然数类型 $nat$ 的封闭项, 那么 $V$ 会是一个具有形式 $\underline{n}$ 的表达式, 即自然数 $n$ 的一个canonical表达式 (通常其被称为数码(numeral)). 实际上求值关系 $⇓$ 应该具有一个性质, 即每当 $E ⇓ V_{1}$ 且 $E ⇓ V_{2}$ , 那么 $V_{1} = V_{2}$ . 这意味着关系 $⇓$ 是确定性的, 意即 $⇓$ 分配给一个给定的表达式 $E$ 以至多一个值. 由(归纳定义的)求值关系 $⇓$ 所给出的操作语义通常被称为大步语义, 因为其抽象掉了由 $E$ 得到 $V$ 的计算的中间步骤. 我们注意到一般情况下对于任意的表达式 $E$ , 可能并不存在一个值 $V$ 使得 $E ⇓ V$ , 即不是每个程序都会终止. {译注: 其实还有另外的可能, 例如产生了运行时异常, 其并非类型错误.} 这 {译注: 指不能保证终止} 是由于一般递归在我们语言PCF中的存在, 其保证了所有的可计算函数都可以由PCF程序所表达.

基于由 $⇓$ 所给出的PCF的大步语义, 我们将会引入具有相同类型的封闭PCF表达式的观察性相等(observational equality)的概念, 其中 $E_{1}$ 和 $E_{2}$ 被认为是观察性相等的当且仅当对于所有具有基本类型 $nat$ 的上下文 $C []$ , 都有 $C [E_{1}] ⇓ \underline{n} \Leftrightarrow C [E_{2}] ⇓ \underline{n}$ 对于每个自然数 $n \in ℕ$ 成立. 从直觉上来说, 表达式 $E_{1}$ 和 $E_{2}$ 是观察性相等的当且仅当对于 $E_{1}$ 和 $E_{2}$ 可以作出相同的观察, 其中一个对于 $E$ 的观察由观察到对于某个具有基本类型 $nat$ 的上下文 $C []$ 和某个自然数 $n$ 有 $C [E] ⇓ \underline{n}$ . 这种观察的概念是对于以下通常实践的数学形式化, 即对于程序进行测试并秉持着程序是(观察性)相等的当且仅当其通过了相同的测试这一观念.

然而, 这个观察性相等的概念并不容易使用, 因为其牵涉所有上下文上的量化, 而这所有上下文构成的集合并不容易抓住 (grasp). 因此, 我们想要找到更为方便的判则, 其可以用来推出观察性相等, 但又避免了诉诸于(有些复杂的)句法概念, 例如求值关系和上下文.

为此目的, 我们引入了所谓的PCF的指称语义, 其为每个具有类型 $σ$ 的封闭表达式 $E$ 赋予一个元素 $⟦ E ⟧ \in D_{σ}$ , 其被称为 $E$ 的指称或者意义或者语义, 其中 $D_{σ}$ 是一个预先定义的结构化集合 (称为语义domain), 在这里面具有类型 $σ$ 的封闭表达式可以找到它们的解释.

指称语义的想法于1960年代末由Christopher Strachey和Dana Scott引入. 当然了, 一个自然的问题是我们应该给语义domain施加什么样的数学结构性质. 尽管实际上语义domain作为特定的拓扑空间来考虑是合适的, 然而其又和分析学和几何学中出现的拓扑空间在风味上相当不同. {原注: 特别地, 语义domain不是Hausdorff空间.} 合适的语义domain概念由Dana Scott引入, 其也发展了语义domain的基本数学理论到相当成熟的程度. 自1970年代初起, 全世界的诸多研究小组都在发展语义domain的理论上投入了相当的能量, 自那时起这个学科被简称为domain论, 其既可以从纯粹数学的观点出发, 也可以从计算机科学的观点出发, 作为编程语言的语义理论的一种.

尽管之后还将远为细致地进行讨论, 现在我们将给出预备性的陈述, 关于如何构造domain $D_{σ}$ , 其中具有类型 $σ$ 的封闭项可以找到它们的指称. 对于自然数类型 $nat$ , 我们置 $D_{nat} = ℕ \cup {⊥}$ , 其中

函数式编程的domain论基础

前言

第1章引论

第2章 PCF及其操作语义

第3章 PCF的Scott模型

第3.1节基本的domain论

第3.2节 PCF的domain模型

第3.3节 LCF——可计算函数逻辑

函数式编程的domain论基础

前言

第1章 引论

第2章 PCF及其操作语义

第3章 PCF的Scott模型

第3.1节 基本的domain论

第3.2节 PCF的domain模型

第3.3节 LCF——可计算函数逻辑

第1章引论

第3.1节基本的domain论