我们目前见到的（对 aexp，bexp 和命令的）求值器是以“大步（big-step）” 风格构造的：它们以“单一大步（one big-step）”的方式描述了一个表达式如 何被求值到最终值上（或一个命令及存储被求值到最终存储上）。 对许多目的而言，这种风格非常简单和自然——确实，它的普及者 Gilles Kahn 也把它 叫做'自然语义（natural semantics）'。但仍然有一些它不擅长的事情。 特别是，它并没有提供一种自然的方式来描述'并发（concurrent）'程序语言， 其语义——即，程序如何运行的本质——不仅仅关于输入状态如何被映射到输出状态， 还包括经过的中间状态，因为当代码并发执行时这些中间状态同样可以被观察到。 大步语义风格的另一个缺点更加技术性，但在一些情况下却非常重要。假设我们定义了一个 Imp 的变种，语言的变量是数字'或'数字的列表。这个扩展语言的语法允许我们写下例如 2 + nil 这样的奇怪表达式，而算数表达式的语义则必须描述这样的表达式是如何执行的。 一种方式是把列表也视作数字，并延续每个表达式都被求值到数字上的约定——比如，当上下文 需要一个数字时，列表会被解释为 0。但这样做其实有一点敷衍了事。 另一种更加自然的方式是说像 2+nil 这类表达式的行为是'未定义的（undefined）' ——即，它根本不会被求值到任何结果。我们可以简单地达到这个目的：只需要把 aeval 和 beval 以 Inductive 命题而非 Fixpoints 的方式来编写，这样我们便可 以表达偏函数而非全函数。 然而，现在我们遇到了一个更严重地问题。在这个语言中，有'两种非常不同的原因'导致 一个命令无法把初始状态映射到任何地结束状态：执行进入了无限循环；或者在某个点，程序 尝试进行一个无意义的操作，比如对一个数字和列表求和，由此无法应用任何一个求值规则。 这两种结果——非停机状态 vs. 在错误的结构上卡住（stuck）——不应当被混淆。特别地，我们想要 以添加某种形式的'类型检查（typechecking）'的方式来'允许'第一种情况（这是我们为 了方便地使用像 while 这类通用循环构造所付出的必要代价），但'阻止'第二种情况 （也即错误的程序）。在剩下的课程中，这会是我们主要讨论的话题。作为第一步，我们需要一种 语义来区分非停机状态和错误的“卡住状态（stuck states）”。 因此，出于这些原因，我们希望有一种更精细化的方式来定义和推理程序的行为。这便是本章的话题。 我们的目的是用“小步（small-step）”关系来代替“大步（big-step）”的 eval 关系， 前者对于给定的程序，描述了计算是如何以“不可分步骤（atomic steps）”执行的。

一个玩具语言

为了简化讨论，让我们回过头来考虑一个只含有常量和加法的简单语言。 （我们使用字母——C 和 P（代表常量（Constant）和加法（Plus）—— 简洁地作为构造子的名字。）在本章的最后，我们回看到如何将这些技术应用到 Imp 语言上。

这是我们之前学习的大步语义风格求值器。

这是用同样风格描述的等价求值器，只是用归纳关系来定义。 我们使用记号 t ==> n 来表达“t 求值到 n”。

	(E_Const)
C n ==> n

t1 ==> n1
t2 ==> n2	(E_Plus)
P t1 t2 ==> n1 + n2

现在，我们展示对应的'小步'求值关系。

	(ST_PlusConstConst)
P (C n1) (C n2) --> C (n1 + n2)

t1 --> t1'	(ST_Plus1)
P t1 t2 --> P t1' t2

t2 --> t2'	(ST_Plus2)
P (C n1) t2 --> P (C n1) t2'

值得注意的几点：

• 我们定义的仅仅是单步关系，其中只有一个 P 节点被其值替换。
• 每步找到准备好的'最左侧（leftmost）' P 节点（也即其操作数都是常量）， 并在原地重写它。第一个规则是说如何重写 P 节点自己；剩下的两个是说如何 得到这样的 P。
• 一个常量项无法继续被求值。

让我们暂停一下，并使用 step 关系来推理一些例子…… 如果 t₁ 可向前一步到 t₁'，那么 P t₁ t₂ 可向前一步到 P t₁' t₂:

练习：1 星, standard (test_step_2)

当求和操作的左侧表达式已经完成求值，其右侧表达式可向前一步： 如果 t₂ 可向前一步到 t₂'，那么 P (C n) t₂ 可向前一步到 P (C n) t₂'：

关系

我们将会研究多个不同的单步关系，因此泛化一下这个概念，给出一些关系的一般定义和 定理是十分有帮助的。（可选章 Rel.v 以更细致的方式开发了这个想法；放在这里 可能会对读者有帮助，但内容过于密集。） 集合 X 上的'二元关系（binary relation）'是由 X 中的两个元素参数化的 命题——也即，一个 X 上序对的命题。

本章中，我们主要的例子将会是单步规约关系，-->，以及它的多步版本， -->*（后面会定义），但是也有许多其他例子——比如，“等于”、“小于”、“小于等于” 和数字上“平方数”关系，还有字符串和列表的“前缀”关系。 和 Imp 的大步求值关系一样，--> 关系的一个简单性质是'确定性（deterministic）'。 '定理'：对于每个 t，最多有一个 t' 且 t 向前一步到 t' (t --> t' 是可证的)。这也就是说 --> 是确定性的。 '证明草稿'：我们通过对 step x y₁ 的导出式（derivation）进行归 纳来证明如果 x 同时前进到 y₁ 和 y₂，那么 y₁ 和 y₂ 是相等的。 取决于导出式中最后使用的规则和 step x y₂ 的导出式中最后的规则，我们有许多 情形需要考虑。

• 如果二者皆为 ST_PlusConstConst，那么结果是显然的。
• 对于两个导出式都以 ST_Plus1 或 ST_Plus2 结束的情形，可直接从归纳假设中得证。
• 其中一个是 ST_PlusConstConst 同时另一个是 ST_Plus1 或 ST_Plus2 的情形是不可能发生的，因为这蕴含了 x 形如 P t₁ t₂ 而 t₁ 和 t₂ 都是常量（根据 ST_PlusConstConst）'且' t₁ 或 t₂ 中的一个形如 P _。
• 类似地，一个是 ST_Plus1 同时另一个是 ST_Plus2 的情形也不可能发生， 因为这蕴含了 x 形如 P t₁ t₂ 而 t₁ 同时是 P t₁₁ t₁₂ 和 C n 两种形式。 ☐

形式化地来说：

可以看到在证明中有一些繁琐的重复。每次使用 inversion Hy₂ 会产生 三个子情形，但只有一个是相关的（匹配当前对 Hy₁ 归纳的那个情形）。 剩下的两个子情形需要通过从假设中找到矛盾并对其反演来消解掉。 下面自定义一个叫做 solve_by_inverts 的策略可以简化这些情形。 如果目标可以通过反演某些假设来解决，调用 solve_by_inverts 会证明目标； 否则，它会失败。

关于它是如何工作的细节目前不那么重要，但是它展示了 Coq 中 Ltac 语言的能力以及如何编写特殊目标的策略。它会在当前证明状态中找到一个具有类型 Prop （第二个 match）的假设 H（第一个 match），然后对 H 进行反演（如果参数 n 大于一，那么它会继续递归地调用这个策略）来完成当前目标。 如果这样的假设不存在，这个策略会失败。 我们通常会带上参数 1 来调用 solve_by_inverts（特别是很大的参数会导致 长时间的证明检查），因此我们对它定义一个缩写 solve_by_invert。

让我们看看这个策略如何简化之前定理的证明吧……

值

下一步，我们会使用“值”的概念来稍微重新表述一下单步归约的定义。 为了更好地理解 --> 关系，我们定义一个'抽象机（abstract machine）':

• 在任意时刻，机器的'状态（state）'是一个项（term）。
• 机器的一'步（step）'是一个原子单元的计算，在这里，是一个“加法”操作。
• 机器的'停机状态（halting states）'是指没有后继计算的状态。

我们可以通过以下方式来执行项 t：

• 以 t 作为机器的起始状态。
• 重复使用 --> 关系来找到一个以 t 开始的机器状态序列，序列中每个状态 会转移到下一个。
• 当无法继续进行归约时，'输出（read out）'最终的机器状态作为执行的结果。

直观地来说，可以看到机器的最终状态总是形如 C n 的项。 我们把这些项叫做'值（values）'。

在引入了值的概念后，我们可以使用它来更简洁地定义 --> 关系中的 ST_Plus2 规则：

	(ST_PlusConstConst)
P (C n1) (C n2) --> C (n1 + n2)

t1 --> t1'	(ST_Plus1)
P t1 t2 --> P t1' t2

value v1
t2 --> t2'	(ST_Plus2)
P v1 t2 --> P v1 t2'

再一次地，变量名在这里包含了重要的信息：按照惯例，v₁ 涉及到值， 而 t₁ 和 t₂ 涉及到任意的项。（在这种约定下，显式的 value 假设也 许是多余的。在这里仍然保留它，主要是为了在非形式化的和 Coq 的规则之间 建立起密切的对应关系，但为简单起见，后面的非形式化规则中我们便会省略掉它。） 这些是形式化的规则：

练习：3 星, standard, recommended (redo_determinism)

作为这一改变的完备性检查，让我们重新验证一下确定性。 下面是它的非形式化证明： '证明草稿'：我们必须证明如果 x 向前一步可同时到 y₁ 和 y₂， 那么 y₁ 和 y₂ 相等。考虑 step x y₁ 和 step x y₂ 生成式 中最后使用的规则。

• 如果二者皆为 ST_PlusConstConst，那么结果是显然的。
• 其中一个是 ST_PlusConstConst 同时另一个是 ST_Plue1 或 ST_Plus2 的情形是不可能发生的，因为这蕴含了 x 形如 P t₁ t₂ 而 t₁ 和 t₂ 都是常量'且' t₁ 或 t₂ 中的一个形如 P _。
• 类似地，一个是 ST_Plus1 同时另一个是 ST_Plus2 的情形也不可能发生， 因为这蕴含了 x 形如 P t₁ t₂ 而 t₁ 既形如 P t₁₁ t₁₂ 又是值 （因此形如 C n）。
• 对于两个导出式都以 ST_Plus1 或 ST_Plus2 结束的情形，可直接从归纳假设中得证。☐

本证明中大部分与之前的相同。但为了最大化练习的收益，你应该从零写下形式化的版本， 只有当卡住时再去回顾之前的证明。

强可进性和正规式

这个玩具语言的单步归约定义是十分简单的，但是对于大一点的语言，往往会出现 因为忘记某个规则而导致一些项虽然还不是值但已无法继续前进归约的情况。下面的定理 说明了我们没有犯这样的错误。 '定理'（'强可进性'（Strong Progress））：如果 t 是一个项，那么 t 要么是一个值，要么存在项 t' 使 t --> t'。 '证明'：对 t 进行归纳。

• 假设 t = C n。那么 t 是值。
• 假设 Suppose t = P t₁ t₂，其中 t₁ 或是值，或可前进到某个 t₁'； t₂ 或是值，或可前进到某个 t₂'（根据 IH）。我们需要证明 P t₁ t₂ 要么是值， 要么可前进到某个 t'
  • 如果 t₁ 和 t₂ 都是值，那么根据 ST_PlusConstConst 得 t 可前进一步。
  • 如果 t₁ 是值且 t₂ 可前进一步，那么根据 ST_Plus2 得 t 可前进一步。
  • 如果 t₁ 可前进一步，那么根据 ST_Plus1 得 t 可前进一步。 ☐

或者，形式化地说：

这个重要的定理叫做'强可进性（strong progress）'，因为每个项 要么是值，要么可“前进”到某个其他的项。（修饰语“强”区分另一个不同的版本， 叫做'可进性'，我们在后面的章节中会学校到。） 通过扩展“做出前进”这个概念，我们可以得到一些关于值有趣的事实：在本语言中， 从这个意义上讲，值是'不能'够继续前进的项。 为了形式化地表述这个观察，让我们给不能前进的项起个名字。我们把它叫做 '正规式（normal forms）'。

请注意这个定义规范了对任意集合 X 上的任意关系 R 的正规式，而不仅仅是我们 这里关心的某个单步归约关系的正规式。后面的课程讨论其他关系时我们会继续使用这个术语。 我们可以使用这个术语来一般化对于强可进性定理的观察：在这个语言中， 正规式和值实际上是同一个东西。

这个为什么值得注意呢？ 因为 value 是一个语法概念——它是由项的形式定义的——然而 normal_form 是一个 语义概念——它是由项如何前进定义的。 并不显然这两个概念应当一致！ 确实，容易错误地写下使它们'不'一致的定义。

练习：3 星, standard, optional (value_not_same_as_normal_form1)

我们可能错误地定义了 value 使它包括了还没有完成归约的项。 （如果你不想亲自动手在 Coq 中完成这个和下一个练习， 也请思考一下，尝试找到一个这样的项。）

练习：2 星, standard, optional (value_not_same_as_normal_form2)

或许，我们错误地定义了 step 使它允许继续归约一个值。

练习：3 星, standard, optional (value_not_same_as_normal_form3)

最后，我们还可能通过 value 和 step 定义了某些不是值但已无法继续由 step 关系进行归约的项。这些项被称作'卡住了（stuck）'。在这种情况是由语义 中的错误导致的，但我们也会看到一些情况，即使是正确的语言定义中也会允许一些项卡住。

（请注意 ST_Plus2 是未定义的。）

额外练习

这是另一个非常简单的语言，其项并不是数字和加法表达式，而是布尔值真和假， 以及条件表达式……

练习：1 星, standard (smallstep_bools)

下列哪些命题是可被证明的？（这只是一个思考练习，但如果你想挑战一下自己， 可以尝试在 Coq 中证明你的答案。）

练习：3 星, standard, optional (progress_bool)

我们之前对加法表达式证明了其可进性，我们也可以证明布尔表达式的可进性。

练习：2 星, standard, optional (step_deterministic)

练习：2 星, standard (smallstep_bool_shortcut)

假设我们想要为布尔表达式的单步归约关系添加“短路（short circuit）”， 这样当条件语句的 then 和 else 分支有相同的值时（tru 或 fls）， 便可以用一步化简整个条件表达式到值，尽管其条件还没有被归约到某个值。 比如，我们想要下面的命题可被证明：
         test
            (test tru tru tru)
            fls
            fls
     -->
         fls.

请为单步关系添加一个额外的语句来达到这个目的，并证明 bool_step_prop4。

练习：3 星, standard, optional (properties_of_altered_step)

课程中证明的确定性和强可进性定理对于我们刚刚定义的单步关系也是成立的。 在我们添加了 ST_ShortCircuit 以后……

• step 关系是否仍然是确定的？请回答是或否，并简要解释（一句话即可）你的答案。
  可选：在 Coq 中证明你的答案。

• 强可进性是否成立？请回答是或否，并简要解释（一句话即可）你的答案。
  可选：在 Coq 中证明你的答案。

• 一般来说，如果从原始的单步关系中拿掉一两个构造子，能否使强可进性不再成立？ 请回答是或否，并简要解释（一句话即可）你的答案。

(* 请在此处解答 *)
☐

多步归约

目前为止，我们学习的是'单步归约（single-step reduction）'关系 -->， 它形式化了抽象机执行程序的每一步。 我们可以使用同一个机器来归约程序直到结束——得到它最后的结果。我们这样形式化它：

• 首先，我们定义一个'多步归约关系（multi-step reduction relation）' -->*，如果项 t 可在任意多的单步（包括零步）内到达 t'，那么它关联起 t 和 t'。
• 接着我们定义 t 的“结果（result）”是一个 t 可用多步达到的正规式。

因为我们会反复使用多步归约这个概念，让我们花点功夫一般化地定义它。 如下，给定关系 R（当前为 -->），我们定义关系 multi R 是 R 的'多步闭包（multi-step closure）'。

（在'逻辑基础'的 Rel 一章和 Coq 标准库中，这个关系叫做 clos_refl_trans_1n。出于可读性的考虑，我们给出一个简短的名字。） 这个定义的作用是 multi R 关联起两个元素 x 和 y，如果

• x = y，或
• R x y，或
• 存在某个非空序列 z₁,z₂, ..., zn 使得
             R x z₁
             R z₁ z₂
             ...
             R zn y.

因此，如果 R 刻画了单步计算，那么 z₁ ... zn 则是 x 和 y 的中间计算步骤。 我们为关系 multi step 使用记号 -->*。

关系 multi R 具有多个重要的性质。 首先，显然它是'自反的（reflexive）'（即 ∀ x, multi R x x）。 就 -->* 关系（即 multi step）而言，可以直观地理解为一个项可以执行零步 到它自己。 第二，它包含了 R——也即，单步执行是多步执行的一个特殊情况。（这个事实解释了 “R 的多步闭包（multi-step closure）”中的“闭包（closure）”一词。）

第三， multi R 是'传递的（transitive）'。

特别地，对于项的 multi step 关系可得，如果 t₁ -->* t₂ 且 t₂ -->* t₃， 那么 t₁ -->* t₃。

例子

这里有一些 multi step 关系的例子：

这是使用 eapply 的另一种证明方法，可以避免显式地构造所有的中间项。

练习：1 星, standard, optional (test_multistep_2)

练习：1 星, standard, optional (test_multistep_3)

练习：2 星, standard (test_multistep_4)

再谈正规式

如果 t 可在零步或多步归约到 t' 且 t' 是一个正规式，那么我们说 “t' 是 t 的一个正规式”。

我们已经看到，这这个语言中，单步归约是确定的——也即，给定的项最多只有一种方法 前进一步。从中可推论，如果 t 可以到到某个正规式，那么这个正规式唯一。换句话说， 我们实际上可以把 normal_form t t' 理解为“t' '就是' t 的正规式”。

练习：3 星, standard, optional (normal_forms_unique)

确实，这个语言中还具备更强的性质（尽管不是所有语言都具备）： 任意项 t 最终都会到达一个正规式——即，normal_form_of 是一个全函数。 形式化地讲，我们说 step 关系是'正规化（normalizing）'的。

为了证明 step 的正规性，我们需要几个引理。 首先，我们观察到如果 t 以多步归约到 t'，那么当 t 出现为 P 节点的左子节点时， 可以使用同一个 t 的归约序列。同理，当 P 的左子节点为值时，若 t 出现为 P 的右子节点也适用。

练习：2 星, standard (multistep_congr_2)

使用这些引理，证明的主体是直接进行归纳。 '定理'：step 函数是正规化的——即，对于每个 t 存在某个 t' 使 t 前进到 t'，且 t' 是正规式。 '证明草稿'：对项进行归纳。有两个情形需要考虑：

• t = C n 其中 n 为数字。这里 t 无法前进一步，我们有 t' = t。 我们可以通过自反性证明左手边的项；对于右手边的项，由 nf_same_as_value 可得值是正规式，且由 v_const 可得 t 是一个值。
• t = P t₁ t₂ 其中 t₁ 和 t₂ 为项。由归纳假设，t₁ 和 t₂ 分别有正规式 t₁' 和 t₂'。回忆一下正规式是值（由 nf_same_sa_value）； 我们知道 t₁' = C n₁ 和 t₂' = C n₂ 其中 n₁ 和 n₂ 为项。 我们可以使用 multi_congr_1 和 multi_congr_2 合并 t₁ 和 t₂ 的 -->* 导出式，以此证明 P t₁ t₂ 在多步内归约到 C (n₁ + n₂)。
  显然，我们的选择 t' = C (n₁ + n₂) 是一个值，也是一个正规式。☐

大步语义和小步语义的等价关系

在使用两种不同的方式（大步和小步式）定义了这个小小语言的操作语义后，你可能会 好奇这两种定义是否是等价的！他们确实是，尽管需要一点工作来证明它。 具体细节留做了练习。

练习：3 星, standard (eval__multistep)

证明的核心想法以下面的方式展现：
       P t₁ t₂ --> (by ST_Plus1)
       P t₁' t₂ --> (by ST_Plus1)
       P t₁'' t₂ --> (by ST_Plus1)
       ...
       P (C n₁) t₂ --> (by ST_Plus2)
       P (C n₁) t₂' --> (by ST_Plus2)
       P (C n₁) t₂'' --> (by ST_Plus2)
       ...
       P (C n₁) (C n₂) --> (by ST_PlusConstConst)
       C (n₁ + n₂)

也即，一个形如 P t₁ t₂ 的项的多步归约关系以如下三步的方式进行：

• 首先，使用 ST_Plus1 数次来归约 t₁ 到正规式，也即必须是一个形如 C n₁ 的项（由 nf_same_as_value），其中 n₁ 为某个数字。
• 接着，使用 ST_Plus2 数次来归约 t₂ 到正规式，也即必须是一个形如 C n₂ 的项，其中 n₂ 为某个数字。
• 最后，使用 ST_PlusConstConst 一次把 P (C n₁) (C n₂) 归约到 C (n₁ + n₂)。

为了形式化这个直觉的理解，我们需要使用之前的合同（congruence）引理 （为了帮助后面的证明，你可能需要回顾一下他们），还有一些 -->* 的基础性质： 自反性，传递性，及其蕴含了 -->。

练习：3 星, advanced (eval__multistep_inf)

请为 eval__multi_step 写出详细的非形式化证明。 (* 请在此处解答 *)

对于另一个方向，我们需要一个引理来对单步归约和大步求值建立联系。

练习：3 星, standard (step__eval)

一旦正确地表述了小步归约蕴含了大步求值的事实，它会很容易被证明。 证明是对多步归约序列的归纳，这个序列被假设 normal_form_of t t' 所隐藏了起来。 请确保在开始证明前首先理解了命题。

练习：3 星, standard (multistep__eval)

额外练习

练习：3 星, standard, optional (interp_tm)

请回忆一下我们还通过函数 evalF 定义了对项的大步求值。请证明它等价于其他语义。 （提示：我刚刚证明了 eval 和 multistep 是等价的，因此逻辑上讲你可以任意 选择证明哪个。尽管有一个要比另一个简单！）

练习：4 星, standard (combined_properties)

我们分开考虑了算数和条件表达式，这个练习探索了他们之间如何交互。

之前，我们分开证明了加法和条件表达式的……

• 单步关系是确定的，以及
• 一个强可进行引理，陈述了任意项要么是值，要么可以前进一步。

对于合并起来的语言，请形式化地证明或反驳这两个属性。 （也即，陈述定理表达性质成立或不成立，并证明它们。）

Imp 的小步语义

现在来看一个更严肃的例子：Imp 的小步操作语义。 目前为止，给这个小语言添加算数和布尔表达式的小步归约关系是很直接的扩展。 处于可读性的考虑，我们为他们分别添加记号 -->a 和 -->b。

我们在此不会赘述布尔值的定义，因为 -->b 的定义并不需要他们（为什么？）， 尽管当语言规模更大一些时可能会需要到他们（为什么？）。

命令的语义是真正有趣的部分。我们需要两个小技巧来让们工作：

• 我们把 SKIP 当作一个“命令值（command value）”——即，一个已经到达正规式的命令。
  • 赋值命令归约到 SKIP （和一个更新状态）。
  • 顺序命令等待其左侧子命令归约到 SKIP，然后丢弃它，并继续 对右侧子命令归约。
• 对 WHILE 命令的归约是把 WHILE 命令变换为条件语句，其后紧跟同一个 WHILE 命令。

（也有一些其他的方式来达到后一个技巧同样的效果，但当对循环体进行归约时， 他们都需要将原始的 WHILE 命令保存在某处。）