没有 K 的 Agda 是否更强大？

Question

作为的后续，我想知道当您将 Agda 与 --without-k 选项一起使用时会发生什么。结果不那么强大？它是一种不同的语言还是所有以前的程序仍然类型检查？

Answer 1

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

Axiom 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

Axiom K 似乎很直观，因为我们用单个 refl 构造函数定义了 Agda 的命题相等性。为什么还要费心研究神秘的非 refl 等式证明，如果没有 K 我们就无法反驳它们的存在？

如果我们没有公理 K，我们可以自由添加与 K 相矛盾的公理，使我们能够极大地概括我们的类型概念。我们可以假设单价公理和高归纳类型，这本质上为我们提供了 Homotopy Type Theory 这本书所讲述的类型理论。

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

如果我们切换到 "book" 同伦类型理论，那么 "having trivial equalities" 就变成了属性我们可以在内部讨论并针对具有 [=34] 的特定类型进行证明=].

没有 K 的 Agda 是否更强大？

Is Agda without K less powerful?

pattern-matching

agda

dependent-type