语义学

形式语义学领域包含以下所有内容:

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

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

形式语义学有许多方法；这些属于三大类:

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

三大类方法之间的区别有时可能是模糊的，但是所有已知的形式语义方法都使用上述技术，或者它们的某种组合。

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

形式语义学的一些变体包括:

• 动作语义是一种尝试模块化指称语义的方法，将形式化过程分成两层(宏和微语义)，并预定义三个语义实体(动作、数据和产出者)以简化规范；
• 代数语义是一种基于代数定律的公理语义形式，用于以形式描述和推理程序语义；
• 属性语法定义了系统地为语言语法的各种情况计算“元数据”(称为属性)的系统。属性语法可以理解为一种指称语义，其中目标语言只是富含属性注释的原始语言。除了形式语义之外，属性语法还被用于编译器中的代码生成，并用上下文敏感的条件来增强常规语法或上下文无关语法；
• 范畴语义学使用范畴理论作为核心数学形式主义。范畴语义学通常被证明对应于给出范畴结构句法表示的一些公理语义学。此外，指称语义通常是一般范畴语义的实例；
• 并发语义是描述并发计算的任何形式语义的总称。历史上重要的并发形式包括参与者模型和过程演算；
• 游戏语义学使用了一个受博弈论启发的隐喻。
• 埃德格·迪杰斯特拉(Edsger W. Dijkstra)开发的谓词转换语义将程序片段的含义描述为将后置条件转换为建立它所需的前提条件的函数。

出于各种原因，人们可能希望描述不同形式语义之间的关系。例如:

• 证明一种语言的特定操作语义满足该语言公理语义的逻辑公式。这种证明表明，使用特定的(公理)证明系统来推理特定的(可操作的)解释策略是“合理的”。
• 通过模拟证明高级机器上的操作语义与低级机器上的语义相关，由此低级抽象机器包含比给定语言的高级抽象机器定义更多的原始操作。这样的证明表明低级机器“忠实地实现”高级机器。

也有可能通过抽象解释理论通过抽象来关联多种语义。

罗伯特·弗洛伊德 被认为是在 。^[1]