依赖类型论的规范性

形式陈述

规范性（canonicity）必须相对于一套具体Martin-Löf 依赖类型论和一个数据类型陈述。对含自然数而无未解释常量的纯内涵核心，典型的判断式自然数规范性是

\varnothing\vdash t:\mathbb N \Longrightarrow \exists n\in\mathbb N, \quad \varnothing\vdash t\equiv\overline n:\mathbb N,

其中 $\overline n=\mathsf{succ}^n(\mathsf{zero})$ 。操作式版本可要求 $t\longrightarrow^*\overline n$ ；弱规范性有时只给出恒等项 $p:\mathsf{Id}_{\mathbb N}(t,\overline n)$ 。三种结论强度不同，不能都简称“算出 numeral”。对布尔型，规范形应为 true 或 false；对函数型，canonical form 通常是 λ，但 canonicity 一词最常用于闭合可观察数据。

一条常见证明链是先建立强正规化或合适的正规化定理，再证明良型闭合正规形的 canonical forms lemma：自然数正规形不可能是自由变量为头的中立项，也不能是 λ 或 Π，故只能是零或后继。也可用逻辑关系、gluing 或 NbE 直接证明每个闭项落入可计算性谓词。无论采用哪条路线，闭合性和签名中没有任意自然数常量都是不可删的前提。

直觉

类型安全说程序不会以类型错误卡住，正规化说计算不会永远走下去，规范性再说明终点确实长成该数据类型承诺的构造器。三者回答不同问题：一个终止的自然数项若停在神秘常量 oracleNat 上，已经正规化，却没有告诉我们它是哪一个数。

规范性因此是“证明即程序”具有可观察内容的关键环节。闭合证明项没有外部假设可等待，闭合自然数程序也没有自由变量可阻塞；若规则全有计算意义，最终结果就应暴露构造器。开放项则允许以变量为头的中立形，不能要求同样结论。

例子与边界

取自然数递归子定义的加法，闭项

t=\mathsf{rec}_{\mathbb N} (\overline1) (\lambda k.\lambda r.\mathsf{succ}(r)) (\overline1)

先在后继分支计算，再在零分支结束，得到 $t\longrightarrow^*\overline2$ 。同一语法若把最后参数换成变量 $x:\mathbb N$ ，则递归子以 $x$ 为主参数卡住，形成合法中立项；这不反驳定理，因为语境已非空。若签名直接加入无计算规则的 $c:\mathbb N$ ，闭项 $c$ 也是正规形却不是 numeral，朴素规范性立即失败。

对 univalence 的边界更细。把 $\mathsf{ua}$ 仅作为普通 MLTT 的公理常量加入时，沿 $\mathsf{ua}(e)$ 的 transport 没有判断式 reduction。例如布尔自等价 $e:\mathsf{Bool}\simeq\mathsf{Bool}$ 可形成

\mathsf{transport}_{\lambda X.X}(\mathsf{ua}(e),\mathsf{true}):\mathsf{Bool},

它在公理式 HoTT 核心中可能停住，而不是判断式化为 true 或 false。语义模型能证明该理论一致，不等于提供了严格计算 canonicity。CCHM 立方类型论通过 interval、composition 与 Glue 赋予 univalence 计算内容，Huber 对相应 cubical theory 证明自然数规范性；这是另一套规则的定理，不能倒灌到仅加公理的 MLTT。

推论与应用

自然数规范性推出闭合可计算函数的结果可实际读取，并常用于证明逻辑一致性：若空类型有闭合项，规范形式分析会找不到任何构造器。它还为程序抽取、内核测试和编译器求值提供基准——定理保证结果形状，具体归约器则负责有效算出该形状。

扩展理论时，canonicity 是比“有一个模型”更敏感的计算验收。新公理、新 quotient 或新路径构造器即便保持一致，也可能产生 stuck closed term；若为它们补 judgmental computation，又必须重证类型保持与正规化。现代 cubical、observational 或 two-level 方案的价值正在于重新安排规则以恢复某种计算规范性，但每项结果都应注明数据类型、闭项范围和等式强度。

参考资料

Bengt Nordström, Kent Petersson, and Jan M. Smith, Programming in Martin-Löf’s Type Theory, Oxford University Press, 1990，evaluation、canonical objects 与纯 MLTT 的计算解释。
The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013，Ch. 1 与公理式 univalence 的 computation caveat。
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg, “Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom,” LIPIcs TYPES 2015 69, 2018, Article 5，计算性 univalence 的独立理论框架。
Simon Huber, “Canonicity for Cubical Type Theory,” Journal of Automated Reasoning 63, 2019, pp. 173–210，自然数 canonicity 定理。

形式陈述 ​

形式陈述