pattern-matching - 没有 K 的 Agda 是否不那么强大？

Question

作为What is Axiom K?的后续，我想知道当你使用 Agda 和 --without-k 时会发生什么？选项。结果不那么强大吗？它是一种不同的语言还是所有以前的程序仍然进行类型检查？

Answer 1

Martin-Löf 类型理论和 Axiom K 的情况在某些方面类似于欧几里得几何和平行假设。有了平行假设，可以证明更多的定理，但这些只是关于欧几里得空间。没有平行假设的可证明定理也适用于非欧式空间，并且可以自由地添加明确的非欧式公理。

公理 K 粗略地说，等式证明不携带重要信息，也没有计算内容。它在逻辑上等同于以下两个语句:

-- uniqueness of identity proofs
UIP : {A : Set}(x y : A)(p p' : x ≡ y) → p ≡ p'

-- reflexive equality elimination
EqRefl : {A : Set}(x : A)(p : x ≡ x) → p ≡ refl

当然，这两者都无法用 --without-K 证明。 .我在这里给出了一些更具体的陈述，这些陈述在没有 K 的情况下是无法证明的，而且其不可证明性乍一看似乎与直觉相反:

{-# OPTIONS --without-K #-}

open import Relation.Binary.PropositionalEquality
open import Data.Bool
open import Data.Empty

-- this one is provable, we're just making use of it below
coerce : {A B : Set} → A ≡ B → A → B
coerce refl a = a

coerceTrue : (p : Bool ≡ Bool) → coerce p true ≡ true
coerceTrue = ? -- unprovable

data PointedSet : Set₁ where
  pointed : (A : Set) → A → PointedSet

BoolNEq : pointed Bool true ≡ pointed Bool false → ⊥
BoolNEq = ? -- unprovable

公理 K 看起来很直观，因为我们用单个 refl 定义了 Agda 的命题等式。构造函数。为什么还要打扰神秘的非 refl如果没有 K，我们就无法反驳其存在的等式证明？

如果我们没有公理 K，我们可以随意添加与 K 相矛盾的公理，使我们能够极大地概括我们的类型概念。我们可以假设单价公理和更高归纳类型，这基本上给了我们类型理论 Homotopy Type Theory书是关于。

回到欧几里得的类比:平行假设假定空间是平坦的，因此我们可以证明依赖于空间平坦性的事物，但不能说明非平坦空间。公理 K 假定所有类型都有平凡的等式证明，因此我们可以证明依赖于它的陈述，但我们不能拥有具有更高维结构的类型。非欧式空间和高维类型都具有一些奇怪的因素，但它们最终是丰富而有用的思想来源。

如果我们切换到“书本”同伦类型理论，那么“具有平凡的等式”成为我们可以在内部讨论并为确实具有该属性的特定类型证明它的属性。