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

给出如下例子

第一条规则称为公理(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是比较重要的，但是咕咕咕