Kが少ないAgdaはあまり強力ではありませんか？

Question

What is Axiom K?のフォローアップとして、--without-kオプションでAgdaを使用するとどうなるのだろうかと思います。結果はそれほど強力ではありませんか？それは別の言語ですか、それとも以前のプログラムはすべてタイプチェックですか？

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とunprovableです。我々は、単一のreflコンストラクタとAgdaの命題平等を定義したので、

{-# 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は、直感的なようだ：私はここのカップルより具体的なKなしunprovableある文、およびそのunprovability一目で直感的に見えるかもしれませんを与えます。なぜなら、謎の非refl平等プルーフを気にするのはなぜですか？私たちはKがなければ反証できません。

私たちが公理Kを持っていなければ、Kと矛盾する公理を自由に追加することができ、私たちはタイプの概念を大いに一般化することができます。我々は本質的に私たちにHomotopy Type Theory本がある型理論を与えるユニヴァンテンス公理と高誘導型を仮定することができます。

ユークリッドの類推に戻って：平行四辺形は空間が平らであると仮定しているので、空間の平面度に依存するものを証明できますが、非平面空間については何も言えません。公理Kは、すべての型は簡単な等価証明を持っていると仮定しているため、それに依存する文を証明できますが、より高次の構造を持つ型を持つことはできません。非ユークリッド空間と高次元の型は、どちらも奇妙な要素を持っていますが、最終的には豊富で有用なアイデアです。

「本」ホモトピー型の理論に切り替えると、「些細な平等」は、内部的に話すことができ、その性質を持つ特定のタイプについて証明できるプロパティになります。