企业官网建设流程全解析

• 形式化验证
• 编程语言

导读

本文依据 doc/sphinx/language/core/conversion.rst 系统讲解 Rocq Prover（Coq）内核中的转换规则（conversion rules）：在归纳构造演算 CiC 中，两个项何时"按定义相等"（definitionally equal）、可转换（convertible）由 β、δ、ι、ζ 归约与 η 展开共同决定。读完本文你将掌握：各归约规则的语法形式与形式化推理规则、正常形（normal form）与弱头正常形的概念、可转换性的判定定义，以及如何使用Eval、cbv等命令/策略在实际证明中应用这些规则，并能对照内核源码理解其底层实现。补充章节 Applying conversion rules 与内核归约实现 kernel/cClosure.ml、kernel/conversion.ml、kernel/redFlags.ml 提供了与本文配套的实战与源码视角。

转换规则总览：归约与展开

Rocq Prover 提供一套转换规则，用来判定两个项在 CiC 中是否按定义相等（convertible，可转换）。转换规则由两类组成：

• 归约（Reductions）：把项逐步转化为更接近其正常形的形式。例如 ζ-归约消除项中的let @ident := @term1 in @term2，把@term1替换到@term2中所有出现@ident的地方，得到的项可能比原项更长或更短。
• 展开（Expansions）：按相反方向应用的归约。例如把2 + 2展开为let i := 2 in i + i。

归约的结果是唯一的，但展开可能不唯一：2 + 2既可以展开为let i := 2 in i + i，也可以展开为let i := 2 in i + 2。那些具有唯一逆展开的归约称为收缩（contraction）。

两个项相等的判定过程是：把双方都归约到正常形（normal form），然后检查它们是否语法相等（忽略绑定变量名称的差异，即按 α-可转换性比较）。正常形定义为反复应用某一组转换规则（β、δ、ι、ζ 归约和 η 展开）直到任何规则都无法再应用时得到的结果。有时归约结果是一个简单的值，例如用cbv beta delta iota把2*3+4归约为10，这需要多次反复应用若干条规则；另一些时候结果可能含有无法归约的变量、公理或不透明常量。

官方文档给出一个 ζ-归约的直观例子（可通过Eval命令验证）：

Eval cbv zeta in let i := 1 in i + i.

文档中的该示例由 Sphinx 的rocqtop指令驱动执行（见 conversion.rst 中Eval cbv zeta in let i := 1 in i + i.），cbv zeta表示只应用 ζ-归约，将let i := 1 in i + i中的i替换为1，得到1 + 1。

八种核心转换规则速查表

原文档给出了全部可用的转换规则，除 η-展开外，其余均可通过cbv等转换策略显式应用：

从源码看，这六条可选择性应用的归约在 kernel/redFlags.ml 中被编码为位标志，内核按位运算组合它们：

let fBETA = FLAG 0b000001 let fDELTA = FLAG 0b000010 let fMATCH = FLAG 0b000100 let fFIX = FLAG 0b001000 let fCOFIX = FLAG 0b010000 let fZETA = FLAG 0b100000

同一文件还预定义了常用的归约组合，例如beta（仅 β）、betaiota（β + match/fix/cofix）、betaiotazeta、all（全部六种）等，供cbv/lazy策略及内核转换使用：

let all = mkfullflags [fBETA;fDELTA;fZETA;fMATCH;fFIX;fCOFIX] let allnolet = mkfullflags [fBETA;fDELTA;fMATCH;fFIX;fCOFIX] let beta = mkflags [fBETA] let betadeltazeta = mkfullflags [fBETA;fDELTA;fZETA] let betaiota = mkflags [fBETA;fMATCH;fFIX;fCOFIX] let betaiotazeta = mkflags [fBETA;fMATCH;fFIX;fCOFIX;fZETA] let betazeta = mkflags [fBETA;fZETA] let delta = mkfullflags [fDELTA] let zeta = mkflags [fZETA] let nored = no_red

可以看到iota正是match fix cofix三者的并集（位标志0b000100 | 0b001000 | 0b010000），与文档中"iota-reduction 是 match-、fix- 和 cofix-归约合称"的描述一一对应。归约标志之外，内核还通过TransparentState（见 kernel/transparentState.mli）记录哪些常量/投影/变量可被 δ-展开。

α-转换（α-conversion）

两个项是α-可转换（α-convertible）的，当且仅当它们在语法上相等，忽略表达式内绑定变量名称的差异。例如forall x, x + 0 = x与forall y, y + 0 = y是 α-可转换的。

值得指出的是，Rocq 内部使用de Bruijn 索引表示这两项（构造项类型constr的Rel分支即 de Bruijn 索引，见 kernel/constr.mli 中"Constructs a de Bruijn index (DB indices begin at 1)"的注释），因此实际上并不需要显式执行 α-转换——绑定变量名字不同并不会带来语法差异，比较可以直接进行。

β-归约（β-reduction）

β-归约归约一个β-redex，即形如(fun x => t) u的项（"β-redex"是"β-reducible expression，β 可约表达式"的简称，术语源自 λ 演算）。

形式化地，在任意全局环境 $E$ 与局部上下文 $Γ$ 中，β-归约规则为：

E[Γ] ⊢ ((λx:T. t) u) ▸_β t[x:=u]

这里 $t[x:=u]$ 称为 $((λx:T.~t)~u)$ 的β-收缩（β-contraction）；反之，$((λx:T.~t)~u)$ 称为 $t[x:=u]$ 的β-展开（β-expansion）。

原文档指出，归纳构造演算的项享有合流性（confluence）、强规范化（strong normalization）、主题归约（subject reduction）等基本性质，这些结果理论意义重大，但文档未展开论述，感兴趣的读者可参阅其引用的 Coq85 文献。在实现层面，β-归约由惰性归约机在弱头位置即时执行——例如 kernel/reduction.ml 中的beta_applist通过"边应用边归约"（application with on-the-fly reduction）来避免先构造完整 λ 项：

let beta_applist c l = let rec app subst c l = match kind c, l with | Lambda(_,_,c), arg::l -> app (arg::subst) c l | _ -> Term.applist (substl subst c, l) in app [] c l

δ-归约（δ-reduction）

δ-归约把定义在局部上下文中的变量或定义在全局环境中的常量替换为它们的值；展开（unfold）即用定义替换常量的过程。形式化规则有两条：

局部定义: (x:=t:T) ∈ Γ ⇒ E[Γ] ⊢ x ▸_δ t 全局定义: (c:=t:T) ∈ E ⇒ E[Γ] ⊢ c ▸_δ t

δ-归约在不透明（opaque）设置允许时才展开常量。因此"不透明/透明"机制直接决定 δ-归约能否进行：

• 封存式不透明（Sealed）：以Qed结尾的定理被永久标记为 opaque，永远不会被展开，也无法转为透明。
• 可变地不透明或透明（Changeably opaque or transparent）：以Defined结尾的定理以及Definition、Fixpoint、CoFixpoint、Function等命令定义的常量默认透明（可展开），随时可用Opaque/Transparent命令切换（默认作用域限于当前 section 或 module）。
• Strategy 命令可提供更细粒度的展开策略控制（均为可变设置）。

Opaque还会影响内核转换算法：在检查两个不同的应用常量是否可转换时，它会尽可能推迟展开被标记的常量。此外，用About命令可以查看某个符号是透明还是不透明。以上内容对应 Applying conversion rules 章节中关于透明度控制的完整说明，其中Opaque/Transparent命令的语法见 equality.rst，Strategy命令见 equality.rst。

在实现层面，δ-归约是否允许展开由 kernel/transparentState.mli 的TransparentState.t记录，并通过 kernel/redFlags.ml 的red_set查询：

let red_set red = function | FLAG f -> red.flags land f != 0 | CONST kn -> TransparentState.is_transparent_constant red.ts kn | PROJ p -> TransparentState.is_transparent_projection red.ts p | VAR id -> TransparentState.is_transparent_variable red.ts id

惰性归约机在展开引用时实际调用的入口是 kernel/cClosure.ml 的unfold_ref_with_args（其接口注释说明：若参数不足返回None，否则把ZPrimitive压入栈；若引用被判定为不可相关且以create_conv_infos创建了上下文，则产生FIrrelevant）。

ι-归约（ι-reduction）

与全局环境中的归纳对象相关联有一条专门的转换规则（其精确规则在文档的 Well-formed-inductive-definitions 章节给出）：作用于构造子构造的对象上的析构器（destructor）行为符合预期。这条规则称为ι-归约，即match-、fix- 与 cofix-归约的合称：

• match消去对构造子的match；
• fix把fix替换为一个 β-redex，并把对符号的递归调用替换为fix项本身；
• cofix与fix类似，针对余归纳结构。

在 kernel/redFlags.ml 中betaiota、betaiotazeta、all等预定义组合都同时包含了fMATCH、fFIX、fCOFIX三个标志，印证了iota的定义。虚拟机中fix/cofix的展开则由 kernel/vm.mli 的reduce_fix/reduce_cofix提供（reduce_fix : int -> vfix -> vfun array * values array）。

ζ-归约（ζ-reduction）

ζ-归约消去项中的 let-in 定义（let x := u in t，语法定义见 definitions.rst），把被定义变量替换为它的值。与 δ-归约的一个关键区别是：ζ-归约把声明从项中完全移除。形式化规则为：

E[Γ] ⊢ u : U 且 E[Γ::(x:=u:U)] ⊢ t : T ⇒ E[Γ] ⊢ let x := u : U in t ▸_ζ t[x:=u]

η-展开（η-expansion）

另一个重要概念是η-展开：允许把任意具有函数类型 $∀ x:T,~U$ 的项 $t$ 与其 η-展开

λx:T. (t x)

等同看待（$x$ 是在 $t$ 中新的任意变量名）。

原文档特别强调：Rocq刻意不定义 η-归约：

λx:T. (t x) 不▸_η t

原因在于，一般情况下 $t$ 的类型未必与 $λx:T. (t x)$ 的类型可转换。例如取 $f : ∀ x:\Type(2),~\Type(1)$，则 $λx:\Type(1).~(f~x) : ∀ x:\Type(1),~\Type(1)$；此时不能允许 $λx:\Type(1).~(f~x)~\triangleright_η~f$，因为归约结果的类型 $∀ x:\Type(2),~\Type(1)$ 无法与原始项的类型 $∀ x:\Type(1),~\Type(1)$ 转换。在实现上，转换算法会在需要时执行 η-展开比较，例如 kernel/cClosure.mli 暴露了eta_expand_stack与eta_expand_ind_stack（后者用于把作为原始记录归纳类型居民的项与构造子应用比较，若归纳类型不是原始记录或构造子部分应用则抛出Not_found）。

示例：组合应用 δ、fix、β 与 match 归约

原文档用一个完整示例演示了各归约规则的分步组合。+是Nat.add的记号（见 Notations），而Nat.add是用Fixpoint定义的。下面的证明脚本用cbv分别指定不同的归约步：

Print Nat.add. Goal 1 + 1 = 2. Proof. cbv delta. (* 展开 Nat.add 的定义 *) cbv fix. (* 对 fix 归约 *) cbv beta. (* 对函数应用归约 *) cbv match. (* 对 match 归约 *)

上述每一步都在目标中应用对应的单一归约规则。也可以直接用cbv（不带参数）一步完成全部归约：

Goal 1 + 1 = 2. Proof. cbv.

cbv归约到弱头正常形：先把表达式的头部规约为弱头正常形（即求值被变量、不透明常量、公理、已构造形式如 λ 表达式/构造子/余归纳点/归纳类型/乘积类型/排序，或规则标志禁止归约的 redex 所阻塞的状态），然后对子项递归应用同样的策略。求值到弱头正常形有两种策略：惰性（lazy，即lazy策略）的按需调用（call-by-need）策略，带共享归约，适合含死代码的表达式；按值调用（call-by-value，即cbv策略）会系统性地先弱求值函数实参，更接近 ML 语言求值语义，对纯计算表达式通常更高效。hnf与red则只对项的头部应用归约规则，simpl/cbn是注重可读性的"智能"归约，vm_compute/native_compute面向性能（详见 Applying conversion rules 对这些策略的分类说明）。

原文档还指出：归约结果可能含有变量、公理或不透明常量而无法进一步归约——例如match x with ... end、(fix f x {struct x} := ...) x这类被变量/不透明常量阻塞的形式，这正是"弱头正常形"概念的用武之地。归约策略的语法（reductions ::= {+ @reduction }，其中reduction可取beta、delta {? @delta_reductions }、match、fix、cofix、iota、zeta、head等）见 equality.rst；delta加-前缀表示展开所有未列出的常量，且注意delta不会作用于项内部 let-in 绑定的变量（那需要zeta）。

证明无关性（Proof Irrelevance）

在严格命题 $A : \SProp$ 中，任意两个类型为 $A$ 的项都被视为等同。严格命题中的项因此被称为无关（irrelevant）的。这是可转换性判定的一个额外组成部分——转换算法在比较含此类证明的项时将其视为不可区分，对应 kernel/cClosure.ml 中evar_handler的evar_irrelevant/qvar_irrelevant字段与FIrrelevant构造子（见 kernel/cClosure.mli 与 kernel/cClosure.mli）。此外，以Qed结束的定理永久不透明，也与数学实践中"证明无关"的惯例一致（见 equality.rst）。

可转换性（Convertibility）的定义

记 $E[Γ] ⊢ t \triangleright u$ 表示在全局环境 $E$ 与局部上下文 $Γ$ 中，用前述 β、δ、ι、ζ 之一对 $t$ 进行归约（语境闭包）得到 $u$。两个项 $t_1$ 与 $t_2$ 称为βδιζη-可转换（简称可转换（convertible）或定义相等（definitionally equal）），当且仅当存在 $u_1, u_2$ 使得

E[Γ] ⊢ t1 ▸ … ▸ u1 且 E[Γ] ⊢ t2 ▸ … ▸ u2

且满足下列条件之一：

1. $u_1$ 与 $u_2$ 在忽略无关子项后完全一致；
2. 它们在 η-展开意义下可转换：$u_1$ 形如 $λx:T.~u_1'$，且 $u_2 x$ 与 $u_1'$ 递归可转换；或对称地，$u_2$ 形如 $λx:T.~u_2'$，且 $u_1 x$ 与 $u_2'$ 递归可转换。

此时记 $E[Γ] ⊢ t_1 =_{βδιζη} t_2$。

除上述基本情形外，可转换性还覆盖以下多态与累积归纳类型的情形（详见 polymorphicuniverses 一章）：

• 多态/累积归纳类型实例：对多态且累积（见第 polymorphicuniverses 章）的归纳类型，若两个方向的子类型关系同时成立，即

  E[Γ] ⊢ t w1 … wm ≤_{βδιζη} t w1' … wm' 且 E[Γ] ⊢ t w1' … wm' ≤_{βδιζη} t w1 … wm

  则视为可转换：

  E[Γ] ⊢ t w1 … wm =_{βδιζη} t w1' … wm'

• 不同宇宙实例的同一构造子：若 $c$ 与 $c'$ 是同一归纳类型（仅宇宙层级不同）的不同实例的相同构造子，且对应实参逐一可转换（$E[Γ] ⊢ v_i =_{βδιζη} v_i'$），两个应用都有类型且类型本身可转换：

  E[Γ] ⊢ c v1 … vm : t w1 … wm E[Γ] ⊢ c' v1' … vm' : t w1' … wm' E[Γ] ⊢ t w1 … wm =_{βδιζη} t w1' … wm'

  则E[Γ] ⊢ c v1 … vm =_{βδιζη} c' v1' … vm'。

可转换关系允许引入一条新的类型规则：两个可转换的良构类型拥有相同的居民（即若 $t_1$ 与 $t_2$ 可转换，则 $t_1$ 的任意居民也是 $t_2$ 的居民，反之亦然）——这正是类型检查中"转换判定（conversion checking）"的根基。

在内核实现中，判定可转换性的核心函数在 kernel/conversion.mli 中声明为conv（转换，CONV 问题）与conv_leq（累积/子类型，CUMUL 问题）：

type conv_pb = CONV | CUMUL val conv : constr extended_conversion_function val conv_leq : types extended_conversion_function

其中conv_pb区分"转换（相等）"与"累积（子类型）"两种比较问题；conv与conv_leq都是扩展的转换函数，支持?l2r、?reds（透明状态，即允许哪些 δ 展开）与?evars（evars 处理）等参数。整个转换算法建立在 kernel/cClosure.ml 的惰性归约机（lazy reduction machine with sharing，由 Bruno Barras 于 1996 年 11 月实现、Hugo Herbelin 于 2000 年 10 月加入 ζ-归约，见 kernel/conversion.ml 的注释）之上：项被转换为闭包形式fconstr（kernel/cClosure.mli），应用实参被压入栈（stack，见 kernel/cClosure.mli），转换比较在栈式弱头归约的过程中逐步完成。归约组合由 kernel/redFlags.ml 的reds记录携带，CClosure.create_conv_infos（kernel/cClosure.mli）据此创建带透明状态与 evar 处理器的转换上下文。内核的类型检查（如常量类型化 kernel/constant_typing.ml）在需要比对类型时即调用这些转换函数。

如何在实践中应用转换规则

除了Eval命令（Eval @red_expr in @term对指定项做归约并显示结果与类型，Compute @term是Eval vm_compute in @term的简写，见 equality.rst）与证明脚本中的归约策略外，还可以用Declare Reduction @ident := @red_expr为归约表达式注册短名（如lazy beta delta [foo bar]），随后在Eval @ident in中使用（见 equality.rst）。Eval是查询命令，可用目标选择器限定作用目标。一个常见用法是定义归约策略后在Definition等命令的Eval子句中化简定义体——测试套件中便有大量:= Eval cbv in ...的实例（如 test-suite/bugs/bug_14014.v 的Eval cbv in @adjust_of_sprop_idempotent A x y pf），以及组合多规则的Eval cbv beta iota zeta delta ...（见 test-suite/bugs/bug_3330.v），可以作为可运行的真实用例参考。

最后需要注意：转换规则不只服务于Eval与归约策略。其他策略（如reflexivity、apply等依赖统一与类型匹配的策略）也会在检查目标与结论是否相等时使用可转换性判定——但除red外，转换策略即使上下文未改变也会成功，且它们通常只改变存在性变量的类型与上下文而保持证明项不变（vm_compute/native_compute例外，它们会在证明项中加入显式强制转换以告知内核使用哪种归约引擎，见 type-cast 相关说明）。这些内容在 Applying conversion rules 中有完整描述。

• 形式化验证
• 编程语言