基于小步语义：已知C1总能终止，如何证明C1;C2可执行至C2？

前置定义回顾 #

• 小步关系ctran的核心顺序组合规则：
  1. 若 (C, s) ∈ ctran (C', s')，则 (C; C₂, s) ∈ ctran (C'; C₂, s')
  2. (term; C₂, s) ∈ ctran (C₂, s)
• ctran*是ctran的传递自反闭包，满足：
  • 自反性：任意配置cfg，cfg ∈ ctran* cfg
  • 传递性：若cfg₁ ∈ ctran* cfg₂且cfg₂ ∈ ctran* cfg₃，则cfg₁ ∈ ctran* cfg₃

证明过程 #

已知(C₁, s) ∈ ctran* (term, t)，目标证明(C₁; C₂, s) ∈ ctran* (C₂, t)，采用基于ctran*推导长度的结构归纳法：

基础情况（推导长度为0） #

此时(C₁, s) = (term, t)（自反性）。根据顺序组合规则2，(term; C₂, s) ∈ ctran (C₂, s)，而s = t，因此(term; C₂, s) ∈ ctran (C₂, t)。由于ctran*包含所有单步ctran关系，故(C₁; C₂, s) ∈ ctran* (C₂, t)。

归纳步骤（推导长度为k+1） #

假设：对于任意C₁'、s'，若(C₁', s') ∈ ctran* (term, t)的推导长度为k，则(C₁'; C₂, s') ∈ ctran* (C₂, t)成立。

现在考虑(C₁, s) ∈ ctran* (term, t)的推导长度为k+1：

1. 推导的第一步必然是(C₁, s) ∈ ctran (C₁', s')，剩余部分是(C₁', s') ∈ ctran* (term, t)（长度为k）。
2. 根据顺序组合规则1，(C₁; C₂, s) ∈ ctran (C₁'; C₂, s')。
3. 由归纳假设，(C₁'; C₂, s') ∈ ctran* (C₂, t)。
4. 根据ctran*的传递性，结合步骤2和3的结果，可得(C₁; C₂, s) ∈ ctran* (C₂, t)。

综上，所有情况均成立，原命题得证。

内容的提问来源于stack exchange，提问作者Huan Sun