指称语义

在计算机科学中，指称语义（英语：Denotational semantics）是通过构造表达其语义的(叫做指称(denotation)或意义的)数学对象来形式化计算机系统的语义的一种方法。编程语言的形式语义的其他方法包括公理语义和操作语义。指称语义方式最初开发来处理一个单一计算机程序定义的系统。后来领域扩展到了由多于一个程序构成的系统，比如网络和并发系统。指称语义起源于 克里斯托弗·斯特雷奇 和 Dana Scott 在1960年代的工作。在 Strachey 和 Scott 最初开发的时候，指称语义把计算机程序的指称(意义)解释为映射输入到输出的函数。后来证明对于允许包含递归定义的函数和数据结构，这样的元素的程序的指称(意义)定义太受限制了。为了解决这个困难，Scott 介入了基于域的指称语义的一般性方法(Abramsky and Jung 1994)。后来的研究者介入了基于幂域的方法，来解决并发系统的语义的问题(Clinger 1981)。粗略的说，指称语义关注找到代表程序所做所为的数学对象。这种对象的搜集叫做域。例如，程序(或程序段)可以被偏函数，或演员事件图想定，或用环境和系统之间的博弈表示: 它们都是域的一般性例子。指称语义的一个重要原则是“语义应当是复合性的”: 程序段的指称应当创建自它的子段的指称。最简单的例子是: “3 + 4”的意义确定自“3”、“4”和“+”的意义。指称语义最初被开发为把函数式和顺序式程序建模为映射输入到输出的数学函数的框架。本文第一节描述在这个框架内开发的指称语义。后续章节处理多态、并发等问题。在本节中我们概览作为指称语义的最初主题的函数式递归程序的语义。问题如下。我们需要给予程序如阶乘函数的定义以语义这个阶乘程序的意义应当是在自然数上一个函数，但是由于它的递归定义，如何以复合方式理解它是不明白的。在递归的语义中，域典型的是偏序，它可以被理解为已定义性(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 都有不动点，它给出自这里的符号 Fi 指示 F 的 i 次应用。符号“⊔”意味着“最小上界”。把这个链的构件认为是“迭代”的有益的。在上述阶乘的情况下，我们有在偏函数的域上的函数 F。所以这个链的最小上界是完全定义的阶乘函数(它凑巧是全函数)。通过研究编程语言的更精细的构造和不同的计算模型，指称语义已经发展起来了。状态(比如堆)和命令特征可以直接用上述指称语义来建模。下面列出的所有教科书都有详情。关键想法是把命令当作在某个状态域上的偏函数。“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语言。把一个程序语言转换成另一个语言经常是有用的。例如一个并发编程语言可被转换成进程演算；高级编程语言可以被转换成字节码(实际上，常规指称语义可以被看作把编程语言解释成域的范畴的内部语言)。在这个语境中，来自指称语义的概念，不如完全抽象，有助于满足安全关注。完全抽象的概念关心程序的指称语义是否精确的匹配它的操作语义。完全抽象的关键性质有:我们希望在操作语义和指称语义之间的额外想要的性质有:在指称语义中长期存在的重点是完全抽象存在于归纳类型中，特别是自然数的类型，作为接受用做递归的一种方法的类型。这个问题的传统解释是作为系统 PCF语言的语义。在 1990年代成功的用博弈语义为 PCF 提供了完全抽象模型，导致了对指称语义的工作在方式上的根本改变。依据 Dana Scott :依据 Clinger :如前面提到过的，这个领域最初由 Christopher Strachey 和 Dana Scott 在 1960年代，接着由 Joe Stoy 在 1970年代于“Oxford University Computing Laboratory”的“Programming Research Group”开发。Montague文法是英语的理想片段的某种形式的指称语义。某些指称语义的著作把类型解释为域理论意义上的域，因而可以被看作模型论的分支，导致了同类型论和范畴论的联系。在计算机科学内与抽象释义、程序验证和函数式编程有联系，参见函数式编程语言中的单子(monad)。特别是，指称语义使用了续体(continuation)来依据函数式编程语义表达顺序编程中的控制流。