• 💭 写在前面：本章我们将继续探讨形式化语义，讲解语义树，然后我们将讨论“为什么需要形式化语义”，以及讲述一个比较有趣的事实（大部分编程语言设计者其实并不会形式化语义的定义）。

目录

0x00 语义树（Derivation Tree）

0x01 关于实现语言

0x02 为什么需要形式化语义？

0x03 事实：部分编程语言的设计者并不会形式化语义

---

0x00 语义树（Derivation Tree）

对于程序 ，如果存在 ，使得 ，则其语义被定义 (即成功终止) 。 

• 这里，符号  表示初始内存，是空的。

💭 举个例子：用于程序 x=1; y=x+5 的推导树

x = 1
y = x + 5

0x01 关于实现语言

我们可以实现一个解释器来解释我们迄今设计的语言，我们可以尝试使用 F# 来实现解释器。

例如：语义域  可以实现为：

type Val = Int of int | Boolean of bool

例如：表达式的评估可以实现为：

let rec eval (e: Exp) (m: Mem) : Val = ...

归纳定义 (Inductive definition) 可以通过递归实现。

对于某些程序，语义未定义，例如：

y = x + true   // 无法应用任何规则

这类程序可以认为是运行时错误，在实现中，我们将设计解释器让其抛出异常。

0x02 为什么需要形式化语义？

我们上一章到目前为止，都在谈论 形式化语义（formal semantics）

形式化语义是计算机科学和语言学中的一个重要领域。

它旨在使用形式化的数学工具来准确地描述自然语言或计算机程序的含义。

用形式化方法来定义语言的结构和含义，以及推导出语言表达式的含义和行为。

主要目标就是消除歧义，确保语言或程序的含义在不同环境下的一致性和可预测性。

它通常包括以下几种主要方法：

• 操作语义（Operational Semantics）
• 语义动态学（Dynamic Semantics）
• 语义形式学（Denotational Semantics）
• 公理化语义（Axiomatic Semantics）

.

❓ 思考：为什么需要形式化语义？

因为需要形式地证明某些有用的属性，比如：

• 证明类型推断算法的正确性。
• 证明编译器优化的正确性
• 证明程序分析算法的正确性。

所有这些都与程序的行为 (语义) 相关，因此，我们首先必须定义这种语义，比如：

• 要证明优化的正确性，我们首先需要定义两个程序的语义等价

0x03 事实：部分编程语言的设计者并不会形式化语义

UUUUnfortunately！！！非常不幸的是，编程语言的爹爹们通常不会 "规范的" 定义其语义！

例如，C 和 JavaScript 的语义是用自然语言口头描述的。

JavaScript 的语义特别复杂，经常令人难以理解（这样产生了许多有趣的研究）

因此，编程语言研究者首先必须正式定义他们想讨论的语言的语义！

例如，CompCert 的作者首先定义了 C 语言的语义，以便制作一个带有正确性证明的编译器。

---

📌 [ 笔者 ]   王亦优
📃 [ 更新 ]   2023.6.12
❌ [ 勘误 ]   /* 暂无 */
📜 [ 声明 ]   由于作者水平有限，本文有错误和不准确之处在所难免，
              本人也很想知道这些错误，恳望读者批评指正！

📜 参考资料  Microsoft. MSDN(Microsoft Developer Network)[EB/OL]. []. .