问命题等式的可判性

EN

当

中的两个项具有相同的范式时，称它们在定义上是精确相等的

最高可达αη转换。

和命题等式只是定义等式的数据类型表示

命题相等表示“在实例化一些自由变量后，这两个术语将变得绝对相等”(" some“可以是0，也可以是全部) (" instantiate”也可以不同)。

例如。

double-double : (n : ℕ) -> n + n ≡ 2 * n

显然，n + n在语法上不等于2 * n，但是对于任何规范n (0, 1, 2...)，n + n的结果在语法上等于2 * n的结果--这就是double-double所说的。“对于任何规范的n”这一部分迫使我们通过归纳来证明double-double (尽管，在更复杂的系统中，定义等式是基于超级编译的，或者有一个内置的验证器，n + n在定义上与2 * n是绝对相等的)。

但有时归纳假设应该是什么样子并不明显，例如当你需要推广一个方程时。正如您可能期望的那样，没有“这是任意的东西可以证明吗？”的决策过程。因此命题相等性是不可判定的。此外，你既不能证明也不能反驳像这样的陈述

(λ n -> 1 + n) ≡ (λ n -> n + 1)

不需要额外的假设。

但是，您确实可以检查语法等价性：

_≟_ : ∀ {α} {A : Set α} -> (x y : A) -> Maybe (x ≡ y)

它说“如果两个术语在句法上相等，那么它们在命题上是相等的，否则我们不知道它们在命题上是否相等”。但是Agda没有这样的内置功能。