指称语义
維基百科,自由的 encyclopedia
在计算机科学中,指称语义(英語:Denotational semantics)是通过构造表达其语义的(叫做指称(denotation)或意义的)数学对象来形式化计算机系统的语义的一种方法。编程语言的形式语义的其他方法包括公理语义和操作语义。指称语义方式最初开发来处理一个单一计算机程序定义的系统。后来领域扩展到了由多于一个程序构成的系统,比如网络和并发系统。
指称语义起源于 克里斯托弗·斯特雷奇 和 Dana Scott 在1960年代的工作。在 Strachey 和 Scott 最初开发的时候,指称语义把计算机程序的指称(意义)解释为映射输入到输出的函数。后来证明对于允许包含递归定义的函数和数据结构,这样的元素的程序的指称(意义)定义太受限制了。为了解决这个困难,Scott 介入了基于域的指称语义的一般性方法(Abramsky and Jung 1994)。后来的研究者介入了基于幂域的方法,来解决并发系统的语义的问题(Clinger 1981)。
粗略的说,指称语义关注找到代表程序所做所为的数学对象。这种对象的搜集叫做域。例如,程序(或程序段)可以被偏函数,或演员事件图想定,或用环境和系统之间的博弈表示: 它们都是域的一般性例子。
指称语义的一个重要原则是“语义应当是复合性的”: 程序段的指称应当建立自它的子段的指称。最简单的例子是: “3 + 4”的意义确定自“3”、“4”和“+”的意义。
指称语义最初被开发为把函数式和顺序式程序建模为映射输入到输出的数学函数的框架。本文第一节描述在这个框架内开发的指称语义。后续章节处理多态、并发等问题。