求值正规化 | Codeboy's Blog

形式陈述

求值正规化（NbE）把规范化分成“解释”与“读回”两步。对语境 $\Gamma$ 中的 $t:A$ ，先建立把自由变量映为反射中立值的语义环境 $\rho_\Gamma$ ，再定义

\mathsf{nbe}_{\Gamma,A}(t) =\mathsf{reify}_{A} (\llbracket t\rrbracket\rho_\Gamma).

$\llbracket-\rrbracket$ 在语义域中执行 β/ι 计算；中立项是以自由变量、metavariable 或无法进一步观察的消去为头的 stuck 形式。 $\mathsf{reflect}_A$ 把类型为 $A$ 的中立语法嵌入语义域， $\mathsf{reify}_A$ 则把语义值读回 η-long 或所选口径的规范形。函数型再化展示二者如何配合：

\mathsf{reify}_{\Pi(x:A).B}(v) =\lambda x. \mathsf{reify}_{B} \bigl(v(\mathsf{reflect}_A(x))\bigr),

其中余类型 $B$ 也要按语义实参实例化。宇宙和依赖族要求同时再化类型与项，不能把简单类型 λ 演算的无类型闭包直接照搬。

针对选定定义相等，正确性通常拆成 soundness 与 completeness：

\Gamma\vdash t:A \Longrightarrow \Gamma\vdash t\equiv\mathsf{nbe}(t):A,

\Gamma\vdash t\equiv u:A \Longrightarrow \mathsf{nbe}(t)=\mathsf{nbe}(u) \quad\text{（语法相同）}.

若求值/再化对所有良型输入终止，且规范形的语法相等可判定，便可用 NbE 判定 conversion。这个算法建立某个理论的正规化性质或利用已知正规化保证；方法、定理与最终决定过程是三个不同层次。

直觉

直接重写像在纸上不断寻找 redex，NbE 则先把表达式送进一个会真正应用函数的语义世界，让行政性 β-redex 自然消失，再把结果按类型“打印”回最规整的语法。遇到自由变量时无法继续求值，就把它反射成中立值保存；读回函数时再喂给一个新鲜中立变量，因而自动完成 η 展开。

这解释了 NbE 为什么不是普通解释器。解释器可以返回宿主值便结束，NbE 必须把开放项和 stuck elimination 完整残留为语法，还要保证读回结果与原项在对象理论中定义相等。宿主语言的函数只是实现语义应用的工具，不等于未经证明地把对象函数相等交给宿主。

例子与边界

考虑闭合于宇宙参数的项

t=\lambda(A:\mathcal U_0).\lambda(f:A\to A).\lambda(x:A). f\bigl((\lambda y.y)\,x\bigr).

求值时 $A,f,x$ 分别被反射为中立值；内部恒等函数实际应用于 $x$ ，语义结果化为 $f(x)$ 。按 Π 类型逐层再化得到

\mathsf{nbe}(t)= \lambda A.\lambda f.\lambda x.f\,x.

对开放项 $f\,x$ ，NbE 不会报“无法求值”，而是保存以 $f$ 为头、 $x$ 为 spine 的中立项。若系统采用函数 η，单独的中立函数 $f:A\to B$ 会再化为 $\lambda x.f\,x$ ；若 η 不属于定义相等，读回策略就不能擅自加入该展开。

边界由理论规则决定。带一般递归的项可能使语义求值不终止；quotient、effect 或任意用户重写需要新的语义结构；把 univalence 仅作为无计算公理加入普通 MLTT，会留下无法按类型读回成预期构造形的常量。立方类型论可以为路径、Glue 与 univalence 另建计算性 NbE，但那不是上述 Π/自然数算法的自动扩展。NbE 也通常不给出一条对象语言小步归约轨迹，所以若任务要求成本或步数证明，还需操作语义。

推论与应用

NbE 可同时服务于实现和元理论：编译器用它比较依赖类型，证明用逻辑关系、PER 或 gluing 说明 reify/reflect 总是定义良好，再推出 conversion 可判定与 Π 构造器可辨识。按需求求值和共享语义闭包还能避免反复替换造成的语法膨胀，但缓存、de Bruijn level 与新鲜变量管理必须保持 readback 的 α-稳定性。

方法的模块边界很清楚：增加一个类型形成子，需要给出它的语义解释、中立消去、反射、再化以及正确性分支。只有这些部分闭合，才能声称新的 NbE 覆盖扩展理论；“现有项看起来能跑”不足以推出 normalization theorem 或 type checker completeness。

参考资料

Andreas Abel, Thierry Coquand, and Peter Dybjer, “Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements,” LICS 2007, pp. 3–12, DOI 10.1109/LICS.2007.33，typed NbE、PER 模型与 equality decidability。
Thierry Coquand and Peter Dybjer, “Intuitionistic Model Constructions and Normalization Proofs,” Mathematical Structures in Computer Science 7(1), 1997, pp. 75–94，语义模型与正规化证明。
Ulrich Berger and Helmut Schwichtenberg, “An Inverse of the Evaluation Functional for Typed λ-Calculus,” LICS 1991, pp. 203–211，反射/再化式 NbE 的经典来源。

形式陈述 ​

形式陈述