Small Step 操作语义

0X00 问题引入

其实说实话，作为一个功底特别差的学生刚看到这一章节的标题的时候是有点傻的， 因为大多数情况下我们对一个语言讨论的时候都是说的语言的语法。但是其实语义(semetic)也是一个比较重要的概念。例如对于表达式 1 * 2 + 2 * 2， 单纯从语法的角度来说，我们只能说也许某种正规的文法规则下面这个表达式是合法的，但是至于它具体是怎样计算的，等于几，就属于语义的范畴。

简单的说，如果在求值的过程中我们一口气把就把加法算出来如类似下面（懒得写真代码了）：

Def eval:
| tadd a b : (eval a) + (eval b)

这就是Big-Step 语义或者也叫自然语义。但是实际的使用过程中，这个其实有一个问题，这里有一个隐含的过程歧义，先算eval a还是先算eval b。在语言的实际使用中并发又很常见，这样的语义操作起来有点不方便，中间状态不好处理。同时在实现的过程中还会遇到诸如nil之类的麻烦事情。
所以把步骤拆分的更加细致是一种比较常见的做法。

Def eval:
| tadd1 a b:  (eval a) + b
| tadd2 a b:  a + (eval b)

0X01 尝试使用

少女抄书中

首先为了方便说明，还是用最最基础的算术来定义23333，就像大部分编译原理是从四则运算一样，在这里定义一种非常简单的语法结构，只包含了值(C)和加法运算(P)。

Inductive tm : Type :=
  | C : nat → tm           (* 常量 *)
  | P : tm → tm → tm.      (* 加法 *)
(* tm 是 term *)

big-step语义是非常容易写的,和一开始说的差不多。

Reserved Notation " t '==>' n " (at level 50, left associativity).
Inductive eval : tm → nat → Prop :=
  | E_Const : ∀n,
      C n ==> n
  | E_Plus : ∀t1 t2 n1 n2,
      t1 ==> n1 →
      t2 ==> n2 →
      P t1 t2 ==> (n1 + n2)
where " t '==>' n " := (eval t n).

可以看到E_Plus中我们直接吧左右在一个case算完了，所以改写成small step其实只要把这一条拆两条就可以了。

Reserved Notation " t '-->' t' " (at level 40).
Inductive step : tm → tm → Prop :=
  | ST_PlusConstConst : ∀n1 n2,
      P (C n1) (C n2) --> C (n1 + n2)
  | ST_Plus1 : ∀t1 t1' t2,
      t1 --> t1' →
      P t1 t2 --> P t1' t2
  | ST_Plus2 : ∀n1 t2 t2',
      t2 --> t2' →
      P (C n1) t2 --> P (C n1) t2'

  where " t '-->' t' " := (step t t').

这里有一点需要注意的是，当拆分成两步之后有之前说的一个先后问题，在这里，我们先假设左边先求值，所以在ST_Plus2被使用来求值的时候 t1已经完成了求值，应该是一个值了所以表达为(C n1)

0X02 操作语义的性质

讨论完了两种定义方式，自然是需要讨论操作语义能够有什么常见性质，能够让我们在证明过程中使用起来。

在讨论性质之前先，先引入值(Value)的概念.
明确一下命令式编程的计算模型， 定义如下的抽象机(Abstract Machine)

• 机器状态(state)是一个term
• 原子操作是step函数
• 停机状态(halting state)是机器没有后继计算的状态
  其中机器在执行的过程中不断的发生状态转移，如果最终停在某个状态且没有后继状态，也就是说无法使用step定义中的任何一条规则进行规约，这时的输出(read out)被称为值(value).

说白了就是一个状态机，value就是输出。

在之前定义的例子当中值就是C n

确定性(Deterministic)

Theorem:
对于所有单步步进关系-->,对于所有t至多有一个t'使得步进关系t --> t'成立。
形式化的有：

Definition deterministic {X : Type} (R : relation X) :=
  ∀x y1 y2 : X, R x y1 → R x y2 → y1 = y2.
Theorem step_deterministic:
  deterministic step.

(* 也就是说 *)
(* ∀ x y1  y2, (x --> y1) -> (x --> y2) -> y1=y2 *)

首先，观察容易的到这个定理的构成是两个单步操作构成的，猜想思路，对两个步进操作进行归纳并且去除所有不可能的部分。考虑到我们其实是为了证明y1 y2一一对应，而每一个y1 对应的应该是一个不同的y2所以需要generalize dependent y2.
Proof:
首先generalize dependent y2得goal

∀ y2, (x --> y2) -> y1=y2

之后对(x --> y1)进行归纳证明.

• 对于step的第一种情况：ST_PlusConstConst,没有递归, 稍大一些的结论中应该有x --> y1 = P (C n1) (C n2) --> C (n1 + n2),也就是说 x取P (C n1) (C n2), y1取C (n1 + n2), 此时代入得到新goal

∀y2, P (C n1) (C n2) --> y2 -> C (n1 + n2) = y2

此时对于 P (C n1) (C n2) --> y2进行反演(这一步也可以用归纳)，直接加两个值显然只能步进到一种情况，容易得到 y2 = C (n1 + n2) ，重写goal,得证。

• 情况2： ST_Plus1: 这里存在递归, 有 x --> y1 = (t1 --> t1') -> (P t1 t2 --> P t1' t2),比较以后容易得到， 引入新条件t1 --> t1'后 稍微大一点的结论中x 取 P t1 t2, y1 取 P t1' t2，代入得到新goal:

∀y2, P t1 t2 --> y2 -> P t1' t2 = y2

此时原先的结论变为归纳假设IH：

∀y2, t1 --> y2 -> t1' = y2

反演 P t1 t2 --> y2可发现，当y2=C (n1 + n2)的时候，反推可以得到t1=C n1, t2=C n2,而此时由于 t1 --> t1'，t1作为一个值无法步进，此情况排除。y2也取ST_Plus1, 那么有t1 --> t1'0则根据归纳假设，容易证明. y2如果取ST_Plus2, 这种情况要求t1是value，这与条件t1 --> t1'存在矛盾，排除。

• 情况3： ST_Plus2: 类似情况2，其中只有y2取ST_Plus时原命题有意义，通过归纳假设容易得出。
  综上，原命题成立。

Q.E.D.

强可进性(Strong Progress)

这条性质是说，如果一种操作语义使得抽象机在步进中只有两种状态： 输出(值)， 可步进到下一状态。
形式化的有如下定义：
Theorem

Theorem strong_progress : 
  ∀t, value t ∨ (∃t', t --> t').

尝试给我们之前定义的玩具语言证明一下这个性质
Proof
对变量t进行归纳证明,term有两种可能

• 当t为C n时,此时t符合value的定义，命题成立。
• 当t为P t1 t2时，代入原goal得到：

 value (P t1 t2) ∨  (∃ t' : tm, P t1 t2 --> t')

此时不难看出有两个规模较小的问题作为归纳假设:

 IHt1 : value t1 ∨  (∃  t' : tm, t1 --> t')
 IHt2 : value t2 ∨ (∃  t' : tm, t2 --> t')

根据假设，如果t1 t2都是value，那么t1 t2可以写成(C n)的形式，代入goal中可得

 value (P (C n) (C n0)) ∨  (∃ t' : tm, P (C n) (C n0) --> t')

不难发现此时可以使用ST_PlusConstConst进行步进。成立。
如果 t1 是value，t2不是.那么t2 --> t',此时观察条件和goal，正好满足ST_Plus2可进行步进。成立。
如果 t1-->t', 此时不难发现满足ST_Plus1.成立。
综上，之前定义的玩具语言的单步操作语义具有强可进性。
Q.E.D

对与强可进的讨论中，有一种情况我们没有涉及， 不满足的情况。
先给出一个定义：
在抽象机执行过程中，如果没有后继状态，那么此时的状态被称为正规形式(normal form)。

有的操作语义是可能导致在执行步进的过程中出现虽然满足了normal form但是却不符合值的定义，这可能是因为语义本身存在错误，也可能是别的什么原因，比如动态强类型语言可能会写出因为类型已经改变而发生类型不匹配。这种情况被称为阻塞(stuck)。

0X03 多步操作语义

在我们之前的定义过程中，每一个step操作都是原子的。我们当然也可以通过闭包(closure)，来定义一个多步的操作，记作-->*。
形式化的有

Inductive multi {X : Type} (R : relation X) : relation X :=
  | multi_refl : ∀(x : X), multi R x x
  | multi_step : ∀(x y z : X),
                    R x y →
                    multi R y z →
                    multi R x z.

Notation " t '-->*' t' " := (multi step t t') (at level 40).

从步进操作的过程不难看出多步规约操作是单步操作的一个自反传递闭包，因为如果只有0次step那么必然等于自己，而t1多不到t2,t2多步到t3,那么t1显然是能到t3的，我们之前证明过强可进了，这个不难。

有了多步操作让我们再来仔细定义一下normal form.
如果t经过多步步进操作后最终能到达t',此时t'没有后继的步进状态，那么称t'是t的正规形式(normal form).
形式化的有：

Definition normal_form {X : Type} (R : relation X) (t : X) : Prop :=
  ¬∃t', R t t'.

而如果有一种语义其能够保证任何一个项目t最终都能化为一个正规式，那么则称这个语义是正规化的(normalizing). 这个说的很玄乎，其实很简单，比如函数式要求，函数是清真的total的，不允许无限递归，死循环。

---

累死了，证明等我喝水。。。。

---