45

I've noticed the discussion of "Axiom K" comes up more often since HoTT. I believe it's related to pattern matching. I'm surprised that I cannot find a reference in TAPL, ATTAPL or PFPL.

  • What is Axiom K?
  • Is it used for ML-style pattern matching as in SML (or just dependent pattern matching)?
  • What's an appropriate reference for Axiom K?
4
  • Normally dependent pattern matching requires K, but Agda also allows you to do it without K, so neither dependent pattern matching nor axiom K implies the other. Axiom K is basically saying that 2 proofs of the same term are equal, eliminating the higher groupoid structure of types.
    – 盛安安
    Commented Aug 31, 2016 at 16:36
  • @盛安安 had I started to ask (in the second bullet point), "Is it required" and why I changed it to "Is it used". So it seems it is usually used but you can avoid it (with Agda at least). Commented Sep 1, 2016 at 6:10
  • 2
    @盛安安 "eliminating the higher groupoid structure of types" — does this only apply when looking at types through the lens of HoTT (or do other TTs have higher groupoid structure or am I making no sense)? Commented Sep 1, 2016 at 7:27
  • 6
    In MLTT, the higher groupoid structure is kind of boring because everything can only be refl (Although you can not formally say that in the system without axiom K).
    – 盛安安
    Commented Sep 2, 2016 at 3:09

1 Answer 1

46

Axiom K is also called the principle of uniqueness of identity proofs, and it is an axiom about the nature of the identity type in Martin-Löf's dependent type theory. This type doesn't exist (and in fact cannot be defined) in simpler type theories such as System F, so that is probably the reason why you haven't encountered it in the books you mention.

The identity type is written as Id(A,x,y) or also x = y and encodes the property that x and y are equal (under the Curry-Howard correspondence). There is one basic way to give a proof of the identity type, and that is refl : Id(A,x,x), i.e. the proof that x is equal to itself.

When investigating the identity type in his thesis, Thomas Streicher introduced a new eliminator for the identity type which he called K (as the next letter in the alphabet after J, the standard eliminator for the identity type). It states that any proof p of an equality of the form x = x is itself equal to the trivial proof refl. From this, it follows that any two proofs p and q of any equation x = y are equal, hence the alternative name "uniqueness of identity proofs". What's remarkable is that he proved that this does not follow from the standard rules of type theory. I recommend reading Dan Licata's article on the homotopy type theory blog if you want to understand why not, he explains it much better than I could.

To answer the second part of your question: ML-style pattern matching is unrelated to K, since ML doesn't have an identity type and hence cannot even formulate the K axiom. On the other hand, K is required for dependent pattern matching as introduced by Thierry Coquand in "Pattern matching with dependent types (1992)". The reason for this is that it is very easy to prove K by pattern matching on the constructor refl of the identity type:

K : (p : x = x) -> p = refl
K refl = refl

In fact, Conor McBride showed in his thesis ("Dependently typed functional programs and their proofs (2000)") that K is the only thing that dependent pattern matching really adds to dependent type theory.

My own interest in this subject is to understand exactly why dependent pattern matching requires K and how it can be restricted so it doesn't anymore. The result was a paper and a new implementation of the --without-K option in Agda. The basic idea is that the unification algorithm used for case analysis during dependent pattern matching shouldn't delete equations of the form x = x, because doing so requires K. I recommend you read the (introduction of) the paper if you want to know more.

3
  • 2
    If Id {A : Set a} : a -> a -> Set _ is defined in terms of the sole constructor refl : forall {x : A}. Id x x, then what is problematic about matching a value of type Id x x with refl?
    – Cactus
    Commented Sep 1, 2016 at 8:27
  • 4
    The reason is that Id is not a family of inductively defined datatypes, but rather an inductively defined family of datatypes. This means you can in principle only match on a value of Id x y if x and y are distinct variables. This would be pretty annoying so Agda uses unification to allow matching on refl in more situations: it unifies the indices x; x of the datatype with the indices x', x' of the constructor. After one step this results in x = x, but this is exactly where we need K again to get rid of this equation (read my paper for the longer version).
    – Jesper
    Commented Sep 1, 2016 at 13:11
  • 2
    Worth pointing out that Coq has something it calls (rightly, in my view) dependent pattern matching, but in a weaker form that does not entail axiom K. Actually, I'm surprised to hear Coquand's original paper required Axiom K. I would look for myself but I'm on my phone and I can only find a #!*%@$! .ps file … Commented Mar 31, 2018 at 18:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.