Agda没有K那么强大吗？

Question

作为什么是Axiom K的后续行动？,我想知道当你使用Agda --without-k选项时会发生什么.结果不那么强大吗？它是一种不同的语言还是所有以前的程序仍然打字检查？

Answer 1

Martin-Löf型理论和Axiom K的情况在某种程度上类似于欧几里德几何和平行假设.用平行假设可以证明更多的定理,但那些只是关于欧几里德空间.没有平行假设可证明定理也适用于非欧几里德空间,并且可以自由地添加明确的非欧几里德公理.

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相矛盾的公理,使我们能够大致概括我们的类型概念.我们可以假设单价公理和高归纳类型,这本质上给出了同伦类型理论书所涉及的类型理论.

回到欧几里得的类比:平行假设假定空间是平的,所以我们可以证明依赖于空间平坦的东西,但不能说任何关于非平坦空间的东西.Axiom K假设所有类型都有平凡的等式证明,所以我们可以证明依赖于它的陈述,但是我们不能有具有更高维度结构的类型.非欧几里德空间和高维类型都有一些奇怪的因素,但它们最终是丰富而有用的思想来源.

如果我们转向"书"同伦类型理论,那么"具有平凡的平等"就成了我们可以在内部谈论的属性,并证明它适用于具有该属性的特定类型.