指称语义

在计算机科学中，指称语义（英語：Denotational semantics）是通过构造表达其语义的(叫做指称(denotation)或意义的)数学对象来形式化计算机系统的语义的一种方法。编程语言的形式语义的其他方法包括公理语义和操作语义。指称语义方式最初开发来处理一个单一计算机程序定义的系统。后来领域扩展到了由多于一个程序构成的系统，比如网络和并发系统。

指称语义起源于 克里斯托弗·斯特雷奇 和 Dana Scott 在1960年代的工作。在 Strachey 和 Scott 最初开发的时候，指称语义把计算机程序的指称(意义)解释为映射输入到输出的函数。后来证明对于允许包含递归定义的函数和数据结构，这样的元素的程序的指称(意义)定义太受限制了。为了解决这个困难，Scott 介入了基于域的指称语义的一般性方法(Abramsky and Jung 1994)。后来的研究者介入了基于幂域的方法，来解决并发系统的语义的问题(Clinger 1981)。

粗略的说，指称语义关注找到代表程序所做所为的数学对象。这种对象的搜集叫做域。例如，程序(或程序段)可以被偏函数，或演员事件图想定，或用环境和系统之间的博弈表示: 它们都是域的一般性例子。

指称语义的一个重要原则是“语义应当是复合性的”: 程序段的指称应当建立自它的子段的指称。最简单的例子是: “3 + 4”的意义确定自“3”、“4”和“+”的意义。

指称语义最初被开发为把函数式和顺序式程序建模为映射输入到输出的数学函数的框架。本文第一节描述在这个框架内开发的指称语义。后续章节处理多态、并发等问题。

递归程序的语义

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

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

function factorial(n:Nat):Nat ≡ if (n==0)then 1 else n*factorial(n-1)。

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

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

给定偏函数 f 和 g，设“f≤g”意味着“在 f 定义的所有值之上 f 一致于 g”。

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

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

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

${\displaystyle \mathbb {N} \times (\mathbb {N} \rightharpoonup \mathbb {N} )\to \mathbb {N} }$ 。

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

λ n:N. if (n==0)then 1 else n*g(n-1)

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

${\displaystyle F:(\mathbb {N} \rightharpoonup \mathbb {N} )\to (\mathbb {N} \rightharpoonup \mathbb {N} )}$ 。

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

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

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

⊔_i∈NFⁱ(⊥)。

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

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

• F⁰(⊥) 是完全未定义偏函数 N→N；
• F¹(⊥) 是定义在 0 上，得到 1，在其他地方未定义的函数；
• F⁵(⊥) 是定义直到 4 的阶乘函数: F⁵(⊥)(4) = 24。它对于大于 4 的参数是未定义的。

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

指称语义的发展

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

状态的指称语义

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

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

数据类型的指称

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

datatype list = Cons of (Nat, list) | Empty.

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

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

datatype D = (D → D)

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

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

datatype α list = Cons of (α, list) | Empty.

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

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

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

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

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

非确定性程序的指称语义

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

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

并发性的指称语义

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

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

顺序性的指称语义

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

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

源到源转换的指称语义

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

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

完全抽象

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

1. 抽象性: 指称语义必须使用独立于编程语言的表示和操作语义的数学结构来做形式化；
2. 可靠性: 所有观察有区别的程序必须有不同的语义；
3. 完备性: 有不同指称的任何两个程序必须有观察区别。

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

1. “构造性”: 语义模型应当在只包含在可以直觉上构造的元素的意义上是构造性的。公式化这个性质的一种方式所有元素必须是有限元素的有向集合的极限。
2. “累进性”: 对于每个系统 S，都有语义的一个 progression_s 函数，使得系统 S 的指称(意义)是 ∨_i∈ωprogression_sⁱ(⊥_S)，这里的 ⊥_S 是 S 的初始格局(configuration)。
3. 完全完备性: 语义模型的所有态射应当是程序的指称。

在指称语义中长期存在的重点是完全抽象存在于归纳类型中，特别是自然数的类型，作为接受用做递归的一种方法的类型。这个问题的传统解释是作为系统 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)来依据函数式编程语义表达顺序编程中的控制流。

引用

教科书

• Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge, Massachusetts, 1977. (A classic if dated textbook.)
• Carl Gunter, "Semantics of Programming Languages: Structures and Techniques". MIT Press, Cambridge, Massachusetts, 1992. (ISBN 978-0262071437)
• Glynn Winskel, Formal Semantics of Programming Languages. MIT Press, Cambridge, Massachusetts, 1993. (ISBN 978-0262731034)
• R. D. Tennent, Denotational semantics. Handbook of logic in computer science, vol. 3 pp 169--322. Oxford University Press, 1994. (ISBN 0-19-853762-X)

其他引用

• ^- S. Abramsky and A. Jung: Domain theory （页面存档备份，存于互联网档案馆）. In S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, vol. III. Oxford University Press, 1994. (ISBN 0-19-853762-X)
• Irene Greif. Semantics of Communicating Parallel Professes MIT EECS Doctoral Dissertation. August 1975.
• Gordon Plotkin. A powerdomain construction SIAM Journal of Computing September 1976.
• Edsger Dijkstra. A Discipline of Programming Prentice Hall. 1976.
• Krzysztof R. Apt, J. W. de Bakker. Exercises in Denotational Semantics MFCS 1976: 1-11
• J. W. de Bakker. Least Fixed Points Revisited Theor. Comput. Sci. 2(2): 155-181 (1976)
• Carl Hewitt and Henry Baker Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1-5, 1977.
• Henry Baker. Actor Systems for Real-Time Computation MIT EECS Doctoral Dissertation. January 1978.
• Michael Smyth. Power domains Journal of Computer and System Sciences. 1978.
• C.A.R. Hoare. Communicating Sequential Processes CACM. August, 1978.
• George Milne and Robin Milner. Concurrent processes and their syntax JACM. April, 1979.
• Nissim Francez, C.A.R. Hoare, Daniel Lehmann, and Willem-Paul de Roever. Semantics of nondeterminism, concurrency, and communication Journal of Computer and System Sciences. December 1979.
• Nancy Lynch and Michael Fischer. On describing the behavior of distributed systems in Semantics of Concurrent Computation. Springer-Verlag. 1979.
• Jerald Schwartz Denotational semantics of parallelism in Semantics of Concurrent Computation. Springer-Verlag. 1979.
• William Wadge. An extensional treatment of dataflow deadlock Semantics of Concurrent Computation. Springer-Verlag. 1979.
• Ralph-Johan Back. Semantics of Unbounded Nondeterminism ICALP 1980.
• David Park. On the semantics of fair parallelism Proceedings of the Winter School on Formal Software Specification. Springer-Verlag. 1980.
• ^- Will Clinger, Foundations of Actor Semantics. MIT Mathematics Doctoral Dissertation, June 1981.
• Lloyd Allison, A Practical Introduction to Denotational Semantics Cambridge University Press. 1987.
• P. America, J. de Bakker, J. N. Kok and J. Rutten. Denotational semantics of a parallel object-oriented language Information and Computation, 83(2): 152 - 205 (1989)
• David A. Schmidt, The Structure of Typed Programming Languages. MIT Press, Cambridge, Massachusetts, 1994. ISBN 0-262-69171-X.
• M. Korff True concurrency semantics for single pushout graph transformations with applications to actor systems Working papers of the Int. Workshop on Information Systems - Correctness and Reusability. World Scientific. 1995.
• M. Korff and L. Ribeiro Concurrent derivations as single pushout graph grammar processes Proceedings of the Joint COMPUGRAPH/SEMAGRAPH Workshop on Graph Rewriting and Computation. ENTCS Vol 2, Elsevier. 1995.
• Thati, Prasanna, Carolyn Talcott, and Gul Agha. Techniques for Executing and Reasoning About Specification Diagrams International Conference on Algebraic Methodology and Software Technology (AMAST), 2004.
• J. C. M. Baeten. Theoretical Computer Science. 2005.
• J.C.M. Baeten, T. Basten, and M.A. Reniers. Algebra of Communicating Processes Cambridge University Press. 2005.
• He Jifeng and C.A.R. Hoare. Linking Theories of Concurrency United Nations University International Institute for Software Technology UNU-IIST Report No. 328. July, 2005.
• Luca Aceto and Andrew D. Gordon (editors). Algebraic Process Calculi: The First Twenty Five Years and Beyond Process Algebra. Bertinoro, Forl`ı, Italy, August 1–5, 2005.
• Bill Roscoe. The Theory and Practice of Concurrency Prentice-Hall. 2005.
• Carl Sassenrath (1999) denotational semantics （页面存档备份，存于互联网档案馆） and the Rebol programming language
• ^- A. W. Roscoe: The Theory and Practice of Concurrency, Prentice Hall, ISBN 0-13-674409-5. Revised 2005.
• Carl Hewitt (2006) What is Commitment? Physical, Organizational, and Social （页面存档备份，存于互联网档案馆） COIN@AAMAS. 2006.

外部链接

• Denotational Semantics （页面存档备份，存于互联网档案馆）. Overview of book by Lloyd Allison
• Structure of Programming Languages I: Denotational Semantics （页面存档备份，存于互联网档案馆）. Course notes from 1995 by Wolfgang Schreiner
• Denotational Semantics: A Methodology for Language Development （页面存档备份，存于互联网档案馆） by David Schmidt

注释

1. Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama: Syntactic control of interference revisited. Electr. Notes Theor. Comput. Sci. 1. 1995.
2. Frank J. Oles: A Category-Theoretic Approach to the Semanics of Programming. PhD thesis, Syracuse University. 1982.
3. Bernhard Reus, Thomas Streicher: Semantics and logic of object calculi. Theor. Comput. Sci. 316(1): 191-213 (2004)
4. P. Baillot. Stratified coherence spaces: a denotational semantics for Light Linear Logic ( ps.gz) Theoretical Computer Science , 318 (1-2), pp.29-55, 2004.
5. Paul Blain Levy: Amb Breaks Well-Pointedness, Ground Amb Doesn't. Electr. Notes Theor. Comput. Sci. 173: 221-239 (2007)
6. Event Structure Semantics for CCS and Related Languages. DAIMI Research Report, University of Aarhus, 67 pp., April 1983.
7. Gian Luca Cattani, Glynn Winskel: Profunctors, open maps and bisimulation. Mathematical Structures in Computer Science 15(3): 553-614 (2005)
8. Mikkel Nygaard, Glynn Winskel: Domain theory for concurrency. Theor. Comput. Sci. 316(1): 153-190 (2004)
9. P. W. O'Hearn and J. G. Riecke, Kripke Logical Relations and PCF, Information and Computation, Volume 120, Issue 1, July 1995, Pages 107-116.
10. Martin Abadi. Protection in programming-language translations. Proc. of ICALP'98. LNCS 1443. 1998.
11. Andrew Kennedy. Securing the .NET programming model. Theoretical Computer Science, 364(3). 2006

参见

• 域理论
• 演员模型的指称语义
• 指称语义的历史