Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Is Agda without K less powerful?

As a follow-up to What is Axiom K?, I'm wondering what happens when you use Agda with the --without-k option. Is the result less powerful? Is it a different language or do all previous programs still type check?

like image 554
Steven Shaw Avatar asked Sep 01 '16 06:09

Steven Shaw


1 Answers

The situation with Martin-Löf type theory and Axiom K is in some ways analogous to Euclidean geometry and the parallel postulate. With the parallel postulate more theorems can be proven, but those are only about Euclidean spaces. Without the parallel postulate provable theorems are true of non-Euclidean spaces too, and one has the freedom to add explicitly non-Euclidean axioms.

Axiom K roughly says that equality proofs carry no non-trivial information and have no computational content. It's logically equivalent to both following statements:

-- 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

Naturally, both of these are unprovable with --without-K. I give here a couple more specific statements that are unprovable without K, and whose unprovability may seem counter-intuitive at first sight:

{-# 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 seems intuitive, since we defined Agda's propositional equality with a single refl constructor. Why even bother with the mysterious non-refl equality proofs whose existence we can't disprove without K?

If we don't have axiom K, we're free to add axioms that contradict K, enabling us to vastly generalize our notion of types. We can postulate the univalence axiom and higher-inductive types, which essentially gives us the type theory that the Homotopy Type Theory book is about.

Turning back to the Euclidean analogy: the parallel postulate posits that space is flat, so we can prove things that depend on space's flatness, but can't say anything about non-flat spaces. Axiom K posits that all types have trivial equality proofs, so we can prove statements that depend on that, but we can't have types with higher-dimensional structures. Non-Euclidean spaces and higher-dimensional types alike have some factor of weirdness but they're ultimately rich and useful source of ideas.

If we switch to "book" homotopy type theory, then "having trivial equalities" becomes a property that we can talk about internally and prove it for specific types that do have that property.

like image 97
András Kovács Avatar answered Oct 21 '22 18:10

András Kovács