递归程序的语义

在本节中我们概览作为指称语义的最初主题的函数式递归程序的语义。

问题如下。我们需要给予程序如阶乘函数的定义以语义

这个阶乘程序的意义应当是在自然数上一个函数，但是由于它的递归定义，如何以复合方式理解它是不明白的。

在递归的语义中，域典型的是偏序，它可以被理解为已定义性(definedness)的次序。例如，在自然数上的偏函数的集合可以给出为如下次序:

通常假定这个域的某个性质，比如链的极限的存在性(参见cpo)和一个底元素。偏函数的偏序有一个底元素，完全未定义函数。它还有链的最小上界。各种额外性质经常是合理的和有用的: 在域理论条目中有更详尽细节。

我们特别感兴趣于在域之间的“连续”函数。它们是保持次序结构和保持最小上界的函数。

在这种设置下，类型被指示为域，而域的元素粗略的捕获了类型的元素。给予带有自由变量的一个程序段的指称语义，依据它从它的环境类型的指称到它的类型的指称的连续函数。例如，段落 n*g(n-1) 有类型 Nat，它有两个自由变量: Nat 类型的n 和 Nat -> Nat 类型的 g。所以它的指称将是连续函数

在这个偏函数的次序下，可以如下这样给出阶乘程序的指称。首先，我们必须开发基本构造如 if-then-else, ==, 和乘法的指称。还必须开发函数抽象和应用的指称语义。程序段

可以接着被给予作为在偏函数的域之间的连续函数的一个指称

阶乘程序的指称被定义为函数 F 的最小不动点。它因此是域 (N⇀ ⇀ -->N){\displaystyle (\mathbb {N} \rightharpoonup \mathbb {N} )} 的一个元素。

这种不动点存在的原因是 F 是连续函数。一种版本的Tarski不动点定理声称在域上的连续函数有最小不动点。

证明不动点定理的一种方式给出了为什么以这种方式给出递归的语义合适的直觉认识，所有在域 D 的带有底元素 ⊥ 的连续函数 F:D→D 都有不动点，它给出自

这里的符号 F 指示 F 的 i 次应用。符号“⊔”意味着“最小上界”。

把这个链的构件认为是“迭代”的有益的。在上述阶乘的情况下，我们有在偏函数的域上的函数 F。

F(⊥) 是完全未定义偏函数 N→N；

F(⊥) 是定义在 0 上，得到 1，在其他地方未定义的函数；

F(⊥) 是定义直到 4 的阶乘函数: F(⊥)(4) = 24。它对于大于 4 的参数是未定义的。

所以这个链的最小上界是完全定义的阶乘函数(它凑巧是全函数)。

指称语义的发展

通过研究编程语言的更精细的构造和不同的计算模型，指称语义已经发展起来了。

状态的指称语义

状态(比如堆)和命令特征可以直接用上述指称语义来建模。下面列出的所有教科书都有详情。关键想法是把命令当作在某个状态域上的偏函数。“x:=3”的指称是使一个状态成为带有 3 被赋值给 x 的状态。顺序算符“;”被指示为函数复合。不动点构造被用来给予循环构造如“while”的语义。

在建模有局部变量的程序的时候事情变得更加困难。一种途径是不在使用域，转而把类型解释为从世界的范畴到域的范畴的函子。程序被指示为在这些函子之间的自然连续函数。

数据类型的指称

很多编程语言允许用户定义递归数据类型。例如，数的列表的类型可以指定为

本节只处理不能变更的泛函数据类型。常规编程语言将典型的允许这种递归列表的元素被变更。

另一个例子: 无类型 lambda 演算的指称为

“解域方程”问题关注找到建模这类数据类型的域。有一种途径，粗略的说把所有域的搜集自身当作一个域，并接着在这里解这个递归定义。下面的教科书给出详情。

多态数据类型是定义时带有参数的数据类型。比如 α lists 的类型被定义为

数的列表，接着是有类型 Nat list，而字符串的列表有类型 String list。

一些研究者开发了多态性的域理论模型。其他研究者还在构造性集合论内建模了参数化多态。详情可见下面列出的教科书。

一个新近研究领域已经涉及了基于编程语言的对象和类的指称语义。

受限复杂性的程序的指称语义

随着基于线性逻辑的编程语言的开发，指称语义已经被给予了线性使用(参见 证明网、一致空间)和多项式时间复杂性的语言。

非确定性程序的指称语义

要给出非确定性程序顺序程序指称语义，研究者已经开发出了幂域理论。对幂域构造写上 P，域 P(D) 是指示为 D 的类型的非确定性计算的域。

在非确定性域理论模型中在公正性和无界性上有困难。参见非确定性的幂域。

并发性的指称语义

很多研究者争论说域理论模型不捕获并发计算的本质。为此介入各种新模型。在 1980 年代早期，人们开始使用指称语义的方式给予并发语言以语义。例子包括Will Clinger 关于演员模型的工作；Glynn Winskel 关于事件结构和petri网的工作 ；和 Francez, Hoare, Lehmann 和 de Roever (1979) 关于CSP的跟踪语义的工作。对所有这些工作的质询仍在研究中。

最近，Winskel 和其他人已经提议了 profunctor 范畴作为并发的域理论。

顺序性的指称语义

顺序编程语言 PCF 的完全抽象问题是在指称语义中长时间的重要的开放问题。PCF 的困难在它是绝对的顺序语言。例如，在 PCF 中无法定义并行或函数。为此如上述介绍的使用域的方式，产生了不是完全抽象的指称语义。

这个开放问题在1990年代随着博弈语义和涉及逻辑关系的技术的发展基本解决了。 详情请参见PCF语言。

源到源转换的指称语义

把一个程序语言转换成另一个语言经常是有用的。例如一个并发编程语言可被转换成进程演算；高级编程语言可以被转换成字节码(实际上，常规指称语义可以被看作把编程语言解释成域的范畴的内部语言)。

在这个语境中，来自指称语义的概念，不如完全抽象，有助于满足安全关注。

完全抽象

完全抽象的概念关心程序的指称语义是否精确的匹配它的操作语义。完全抽象的关键性质有:

抽象性: 指称语义必须使用独立于编程语言的表示和操作语义的数学结构来做形式化；

可靠性: 所有观察有区别的程序必须有不同的语义；

完备性: 有不同指称的任何两个程序必须有观察区别。

我们希望在操作语义和指称语义之间的额外想要的性质有:

“构造性”: 语义模型应当在只包含在可以直觉上构造的元素的意义上是构造性的。公式化这个性质的一种方式所有元素必须是有限元素的的有向集合的极限。

“累进性”: 对于每个系统 S，都有语义的一个 progressions 函数，使得系统 S 的指称(意义)是 ∨i∈ωprogressions(⊥S)，这里的 ⊥S 是 S 的初始格局(configuration)。

完全完备性: 语义模型的所有态射应当是程序的指称。

在指称语义中长期存在的重点是完全抽象存在于归纳类型中，特别是自然数的类型，作为接受用做递归的一种方法的类型。这个问题的传统解释是作为系统 PCF语言的语义。在 1990年代成功的用博弈语义为 PCF 提供了完全抽象模型，导致了对指称语义的工作在方式上的根本改变。

语义与实现

依据 Dana Scott [1980]:

依据 Clinger [1981]:

指称语义的早期历史

如前面提到过的，这个领域最初由 Christopher Strachey 和 Dana Scott 在 1960年代，接着由 Joe Stoy 在 1970年代于“Oxford University Computing Laboratory”的“Programming Research Group”开发。

Montague文法是英语的理想片段的某种形式的指称语义。

同其他计算机科学领域的联系

某些指称语义的著作把类型解释为域理论意义上的域，因而可以被看作模型论的分支，导致了同类型论和范畴论的联系。在计算机科学内与抽象释义、程序验证和函数式编程有联系，参见函数式编程语言中的单子(monad)。特别是，指称语义使用了续体(continuation)来依据函数式编程语义表达顺序编程中的控制流。

域理论

演员模型的指称语义

指称语义的历史

免责声明：以上内容版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。感谢每一位辛勤著写的作者，感谢每一位的分享。