什么是指称语义?

What is denotational semantics?

我正在寻找一个准确易懂的定义。我发现的那些彼此不同:

Denotational semantics is a mathematical expression of the formal meaning of a programming language.

Denotational semantics is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called denotations) that describe the meanings of expressions from the languages

术语"denotational semantics"指的是程序的数学含义为程序赋予这些含义的方法。就好像"history"这个词,意思是某事物的历史,也就是事物历史的整个研究领域。

我从未发现术语 "denotational semantics" 的定义对于理解概念及其意义有用。相反,我认为最好的方法是考虑指称语义支持的推理形式。

具体来说,指称语义使 等式推理 具有 referentially transparent 程序。维基百科给出了引用透明度的介绍性定义:

An expression is said to be referentially transparent if it can be replaced with its value without changing the behavior of a program (in other words, yielding a program that has the same effects and output on the same input).

但更精确的定义不会谈论用 "value" 替换表达式,而是用 另一个表达式 替换它。然后,引用透明度是 属性,如果您将 部分 替换为具有 相同表示 的替换,则生成的整体 同义

所以恕我直言,作为一名程序员,这是理解的关键:指称语义是关于如何将数学 "teeth" 赋予引用透明性的概念,因此我们可以对关于正确性的声明给出原则性的回答代换。例如,在函数式编程的上下文中,一个关键应用是:我们什么时候可以说两个函数值表达式实际上表示 "the same" 函数,因此其中一个可以安全地替换另一个?经典的指称答案是 extensional equality:两个函数相等当且仅当它们将相同的输入映射到相同的输出时,所以我们只需要证明所讨论的表达式是否表示扩展等价函数。因此,例如,Quicksort 和 Bubblesort 是明显不同的参数,但在指称上它们是相同的函数。

在响应式编程的上下文中,最大的问题是:我们什么时候可以说两个不同的表达式仍然表示相同的事件流或时间相关值?