By Chapter#
2: Mathematical Background#
2.3 Transition System#
一个transition system由以下要素构成：
- 一个集合 \(Config\)，由所有可能的 configuration 或 state 组成；
- \(Config\) 上的一个二元关系，记为 \(\rightarrow\)，它满足 \(\rightarrow \subseteq Config \times Config\)；
Inital/Final subset: \(Config\) 的一个子集，分别记为 \(I\) 和 \(T\)。
- 显然我们可以有这样的结论：\(\forall c\in T, c\not\to\).
4: 指令式语言的操作语义（以 SIMP 为例）#
4.3 SIMP 的结构式操作语义#
总体而言，
- 小步语义（small-step semantics）是归约（reduction）的语义，更关心程序的执行过程；
- 大步语义（big-step semantics）是评估（evaluation）的语义，更关心程序的最终结果（我更愿意称之为机器状态改变的情况）
以 SIMP 的小步语义为例，
Configurations 的形式为
$$ \langle P, s \rangle, $$其中 \(P\) 是一个 SIMP 程序，\(s\) 是一个存储（store）。存储的表示形式是一些从地址(locations)到整数(integers) 的偏函数(partial function)。
- \(s\left[ l\mapsto n\right]\) 表示在存储 \(s\) 上更新地址 \(l\) 的值为 \(n\)。
常见的其他记号：\(!l\) 表示解引用.
小步语义的 reduction 即为 configuration 之间的 transition 关系，通常记为 \(\rightarrow\).
SIMP 的小步语义的具体规则可以参考这本书 p78 的 Fig.4.2.
可以推演一个“交换x和y”的程序来体会小步语义的细节（Example 4.8）。（假设\(s(z)= 0, s(x)= 1, s(y)= 2\))
$$ \begin{align} \langle z\coloneqq !x; (x\coloneqq !y; y\coloneqq z), s\rangle \rightarrow& \langle z\coloneqq 1; (x\coloneqq !y; y\coloneqq z), s\rangle\\ \rightarrow& \langle skip,(x\coloneqq !y; y\coloneqq z), s[z\mapsto 1]\rangle \\ \rightarrow& \langle x\coloneqq !y; y\coloneqq z, s[z\mapsto 1]\rangle \\ \rightarrow& \langle x\coloneqq 2; y\coloneqq z, s[z\mapsto 1]\rangle \\ \rightarrow& \langle skip, y\coloneqq z, s[z\mapsto 1,x\mapsto 2]\rangle \\ \rightarrow& \langle y\coloneqq z, s[z\mapsto 1,x\mapsto 2]\rangle \\ \rightarrow& \langle y\coloneqq 1, s[z\mapsto 1,x\mapsto 2]\rangle \\ \rightarrow& \langle skip, s[z\mapsto 1,x\mapsto 2,y\mapsto 1]\rangle \end{align} $$Final configurations即为不可归约(irreducible)的 configuration。（在 SIMP 中它一般是以下这样的形式：
- \(\langle n, s\rangle\)，其中 \(n\) 是一个整数；
- \(\langle b, s\rangle\)，其中 \(b\) 是一个布尔值；
- \(\langle !l, s\rangle\)，其中 \(l\not\in dom(s)\)（相当于是未定义的变量）；
- \(\langle skip, s\rangle\)。
要讨论大步语义，就得先定义 Evaluation 是什么。
大步语义的 evaluation 也是 configuration 之间的 transition 关系，通常记为 \(\Downarrow\).
SIMP 的大步语义的具体规则可以参考这本书 p82 的 Fig.4.3.
对前面的同一个问题，用大步语义分析时可以直接分步使用 (var) 规则和 (seq) 规则。和小步语义对比的话，小步语义必须遵循程序的执行顺序来得到 transition 的过程（非常符合指令式程序的运行直觉），而大步语义则更关注“程序可以从这个状态转变为那个状态”，并且可以直接合理组装所需要的结论得到最终结论。
Others#
WIP