规范性是否意味着弱规范化？

Question

语境：类型理论。

我的理解：

• 网址：每个项都可以重写为 NF。
• 正规：每个术语都重写为规范形式。

然后它会导致一种直觉，如果规范性成立，那么我们得到 NF = 规范形式，因此 WN 成立。然而，我并没有看到人们经常这样说，比如 这个问题 谈论规范性，但从未提及 NF 或规范化。在 实验室, ，规范形式被认为是规范形式，这证明了我的“NF =规范形式”猜测，但它并没有说 WN 因此成立。因此我怀疑我的直觉。

所以我想知道这是对的（有证据吗？），还是错的（有反例吗？）。

Answer 1

规范性并不意味着弱规范化。首先，让我更准确地表达所涉及的定义：

• 网址：每个开放项都可以化简为正规项
• 正规：每个封闭项都可以简化为规范项

（笔记：在类型论的现代元理论中，更常见的是谈论转换而不是归约，同样谈论范式的唯一存在而不是弱/强规范化。如果我们用“可转换”替换上面的“可还原”，这个答案仍然有效）。

正常术语和规范术语并不相同。例如， x 变量在 x : Bool 上下文是正常的，但不规范。另外，封闭式期限 λ(b : Bool). if true then b else b 是规范的但不正常。

外延类型理论具有规范性，但不具有WN、SN或范式的唯一存在性。这是因为在 ETT 中，可以向上下文添加不一致的定义等式，或者添加图灵完备系统的方程理论。例如，在 ETT 上下文中 n : Nat, p : n = suc n 这 n 变量没有唯一的范式，因为 n 可以任意扩展使用 p.

然而，如果我们有一个封闭的 ETT 术语，我们就不能在上下文中有任何可疑的东西，因此封闭术语仍然可以被评估为规范形式。