操作语义、指称语义和公理语义之间有什么区别？

Question

在阅读有关计算机科学和编程语言的论文时，我经常偶然发现术语指称语义和操作语义。有时，但很少，我也发现公理。虽然我知道语义是什么，但我不明白这三者之间的区别——实际的分类是什么？

一些例子会非常有用。

Answer 1

这直接来自 Glynn Winskel（麻省理工学院出版社，1993 年）的精彩著作《编程语言的形式语义学》的序言：

操作语义通过指定编程语言在抽象机器上的执行方式来描述编程语言的含义。我们专注于 Gordon Plotkin 在奥胡斯关于“结构操作语义”的讲座中提倡的方法，其中评估和执行关系由规则以语法指导的方式指定。

指称语义是一种定义编程语言含义的技术，由 Christopher Strachey 开创，并由 Dana Scott 提供了数学基础。它曾一度被称为“数学语义”，它使用完全偏序、连续函数和最小不动点等更抽象的数学概念。

公理语义试图通过在程序逻辑中为其提供证明规则来修复编程构造的含义。与这种方法相关的主要名字是 R.W.Floyd 和 C.A.R.Hoare。因此，公理化语义从一开始就强调正确性的证明。

因此，这些是推理程序含义的不同方法，总体目标是能够证明特定程序“正确”运行。它们并不相互对立：每种技术都有其用途，并且通常可以一起用于研究各个方面。例如，在推理 Haskell 时，通常对纯片段（本质上是递归函数）使用指称方法，而对 IO 和并发进行推理则使用操作方法。典型的命令式语言（Pascal 或类似 C）通常使用公理化语义以最弱前提条件的形式推理正确性。

我强烈建议您阅读 Winskel 的书，如果您能亲身体验的话，因为它提供了对所有三种技术的详细且易于理解的说明。