Notations
简单的就不说了
Mathematics
Partial Function
称 \(f\subseteq A\times B\) 这个二元关系为 partial function 当且仅当 \(\forall a\in A, \forall b_1,b_2\in B, afb_1\wedge afb_2\Rightarrow b_1=b_2\).
之所以说是 partial 的是因为 \(f\) 不一定对 \(A\) 中所有元素都有定义。一个写法是 \(f(a)=\bot\) 表示 \(a\not\in D(f)\)，经典的含义是 \(f\) 对输入 \(a\) 不会终止。
Relation Closure
二元关系 \(R\) 的 reflexive closure 记作 \(R^+\)，transitive closure 记作 \(R^*\)
Preservation by Relation
考虑 \(R\subseteq A\times B\)，\(P\) 是谓词，若 \(\forall a,b, P(a)\wedge aRb\Rightarrow P(b)\)，那么称 \(P\) 在 \(R\) 下保持。
Syntax
可以用如下几种等价方式定义语法
- BNF
- 递归构造句子的集合
- 定义合法句子集合的性质，声明合法句子集合是满足这些性质的最小集
Semantics
主要是小步操作语义(Small Step Operational Semantics)，本质上是定义了一个抽象的状态机(不一定要是确定状态机)以及这个抽象状态机上的状态转换
方便起见，下面记语言的集合为 \(T\)
reduction relation
二元关系 \(\rightarrow\subseteq T\times T\) 被称为 reduction relation。通常用若干规则(Inference Rules)来定义这样的规约关系。例如 \(\dfrac{a\rightarrow b\quad b\rightarrow c}{a\rightarrow c}\) 就展示了一种有传递性的规约关系。
If-Then-Else
给出如下例子
\[ \dfrac{}{\text{if True then $s_1$ else $s_2$}\rightarrow s_1} \\ \\ \dfrac{e\rightarrow e'}{\text{if $e$ then $s_1$ else $s_2$}\rightarrow \text{if $e'$ then $s_1$ else $s_2$}} \\ \]
第一条规则称为公理(Axiom)，这样直接进行计算的规则也叫Computation Rule。
第二条的前提(Premise)是 \(e\rightarrow e'\)，这样只是指出要对哪个 subterm 做规约的规则叫Congruence Rule(回忆Evaluation Context)
Normal Form/Value
如果一个项没法继续规约了，就称这个项为Normal Form Term。
Value是认为规定的一个项的集合，通常希望Value是Normal Form的。
一些非预期的Normal Form往往意味着违反了语言的语义(或是未定义行为)，此时可以给这样的错误情况定一个 \(\overline{t\rightarrow \bot}\) 的规则，这样就是前面提到的运行时错误检查了(不存在UB)。
Property/Metatheory
一些这一章提到的比较基础的语言性质
- 确定性(Determinism)，即每次只有唯一的规则可以推导
- 终止性(Termination)，即推导有限次可以变成Normal Form
- Diamond Property，即使没有单步推导的确定性，也有总体上的确定性。
Diamond Property是比较重要的，但是咕咕咕