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

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

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

一些例子会非常有用。

解决方法

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

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

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

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

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

我强烈建议您通读 Winskel 的书，如果您能掌握它的话，因为它提供了对所有三种技术的详细但非常易于理解的说明。