语义学（计算机科学）

在编程语言理论中，语义学是对编程语言意义的严格的数学研究。语义学将计算意义分配给编程语言语法中的有效字符串。语义学描述了计算机在执行该特定语言的程序时所遵循的过程。这可以通过描述程序的输入和输出之间的关系来显示，或者解释该程序将如何在某个平台上执行，从而创建一个计算模型。

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

不同语义模型之间的关系不同的意义方法之间的关系计算与逻辑、集合论、模型论、范畴论等领域的基础数学结构之间的关系它与计算机科学的其他领域有着密切的联系，如编程语言设计、类型理论、编译器和解释器、程序验证和模型检查。

形式语义学有许多方法；这些方法属于三个主要类别。指称语义学，即语言中的每个短语都被解释为一个指称，即一个可以被抽象思考的概念性意义。这种指称通常是居住在数学空间的数学对象，但并不要求它们应该如此。作为一种实际需要，指称是用某种形式的数学符号来描述的，而这种数学符号又可以被形式化为指称的金属语言。例如，功能语言的指称语义学经常将语言翻译成领域理论。指称语义描述也可以作为从编程语言到指称金属语言的组合翻译，并作为设计编译器的基础。操作语义，即直接描述语言的执行（而不是通过翻译）。操作语义学松散地对应于解释，尽管解释器的执行语言通常也是数学形式主义。操作语义学可以定义一个抽象的机器（比如SECD机器），并通过描述它们在机器的状态上引起的转换来赋予短语以意义。或者，像纯羔羊微积分那样，操作性语义可以通过语言本身的短语的语法转换来定义；公理语义，即通过描述适用于短语的公理来赋予短语以意义。公理语义学在短语的意义和描述它的逻辑公式之间没有区别；它的意义正是在某种逻辑中可以证明的东西。公理语义学的典型例子是Hoare逻辑。除了在指称、操作或公理方法之间的选择之外，形式语义系统中的大多数变化都来自于对支持数学形式主义的选择。变化形式形式语义学的一些变化包括如下。行动语义学是一种试图将指称语义学模块化的方法，它将形式化过程分成两层（宏观和微观语义学），并预先定义了三个语义实体（行动、数据和产出者）以简化规范；代数语义学是公理语义学的一种形式，它基于代数法，以形式化的方式描述和推理程序语义。它还支持指称语义和操作语义；属性语法定义了系统地计算语言语法的各种情况的元数据（称为属性）的系统。

属性语法可以被理解为一种指称语义，其中目标语言只是用属性注释丰富了原始语言。除了形式语义学，属性语法也被用于编译器中的代码生成，以及用上下文敏感的条件来增强正则或无语境语法；分类（或漏斗）语义学使用类别理论作为核心数学形式主义。一个分类语义学通常被证明对应于一些公理语义学，它给出了分类结构的句法表述。另外，指称语义学通常是一般分类语义学的实例；并发语义学是描述并发计算的任何形式语义学的总称。历史上重要的并发形式学包括行为者模型和过程计算；博弈语义学使用了受博弈论启发的隐喻；由EdsgerW.Dijkstra开发的谓词转换器语义学，将程序片段的意义描述为将后置条件转换为建立该条件所需的前置条件的函数。描述关系由于各种原因，人们可能希望描述不同形式语义学之间的关系。