形式语义学

在编程语言理论中，语义学是对编程语言含义的严格数学研究。 语义为编程语言语法中的有效字符串分配计算意义。

语义描述了计算机在以该特定语言执行程序时遵循的过程。 这可以通过描述程序的输入和输出之间的关系，或解释程序将如何在特定平台上执行来显示，从而创建计算模型。

1967 年，罗伯特·W·弗洛伊德 (Robert W. Floyd) 发表了论文 Assigning meanings to programs； 他的主要目标是为计算机程序的证明制定严格的标准，包括正确性、等价性和终止性的证明。 弗洛伊德进一步写道：

在我们的方法中，编程语言的语义定义是建立在句法定义之上的。 它必须指定语法正确的程序中哪些短语代表命令，以及必须对每个命令附近的解释施加什么条件。

1969 年，托尼·霍尔 (Tony Hoare) 发表了一篇关于以弗洛伊德 (Floyd) 思想为种子的霍尔逻辑的论文，现在有时统称为公理语义学。

在 1970 年代，出现了操作语义和指称语义这两个术语。

形式语义学领域包括以下所有内容：

• 语义模型的定义
• 不同语义模型之间的关系
• 不同意义处理方法之间的关系
• 逻辑、集合论、模型论、范畴论等领域的计算与底层数学结构之间的关系。

它与计算机科学的其他领域有密切联系，例如编程语言设计、类型理论、编译器和解释器、程序验证和模型检查。

形式语义有很多方法； 这些属于三大类：

• 外延语义，语言中的每个短语都被解释为外延，即可以抽象地思考的概念意义。 这样的外延通常是居住在数学空间中的数学对象，但并不要求它们必须如此。 作为一种实际需要，外延是使用某种形式的数学符号来描述的，这又可以形式化为指称元语言。 例如，功能语言的指称语义通常将语言翻译成领域理论。 指称语义描述还可以作为从编程语言到指称元语言的组合翻译，并用作设计编译器的基础。
• 操作语义，直接描述语言的执行（而不是通过翻译）。 操作语义松散地对应于解释，尽管解释器的实现语言通常也是一种数学形式。 操作语义可以定义一个抽象机器（例如 SECD 机器），并通过描述它们在机器状态上引起的转换来赋予短语意义。 或者，与纯 lambda 演算一样，可以通过对语言本身的短语进行句法转换来定义操作语义；
• 公理语义学，通过描述适用于短语的公理来赋予短语意义。 公理化语义不区分短语的含义和描述它的逻辑公式； 它的意义正是在某种逻辑上可以证明的。 公理语义的典型例子是霍尔逻辑。

除了在指称、操作或公理化方法之间进行选择外，形式语义系统的大多数变化都来自支持数学形式主义的选择。

形式语义的一些变体包括：

• • 动作语义是一种尝试模块化指称语义的方法，将形式化过程分为两层（宏语义和微观语义）并预定义三个语义实体（动作、数据和 yielders）以简化规范；
  • 代数语义是基于代数定律的公理语义的一种形式，用于以形式化的方式描述和推理程序语义。 它还支持指称语义和操作语义；
  • 属性语法定义了系统地为语言句法的各种情况计算元数据（称为属性）的系统。 属性语法可以理解为一种指称语义，其中目标语言只是原始语言，并通过属性注释进行了丰富。 除了形式语义之外，属性语法还被用于编译器中的代码生成，以及使用上下文敏感条件来扩充常规或上下文无关语法。