2

I am trying to find more information (preferably an academic paper) for the concept of "dependent elimination". I understand the concept itself: it means constructing a type by eliminating a term i.e. eliminating a term into the large universe of types. But I would like to know if there is some paper or thesis or dissertation or book that I could cite. I know that this Stack Exchange question exists but I'm not sure it is exactly citeable.

I've read two papers that mention this concept, but unfortunately they don't add a citation for it:

Bottom line: is there somewhere I could read more about "dependent elimination" that I could also cite?

Valmir Junior
  • 25
  • 4
  • As far as I know, there isn't a unified technical meaning of "dependent elimination". For specific type constructions one can discuss dependent vs. non-dependent eliminators, but these are done on a case-by-case basis. The non-dependent eliminators are called "recursors". – Andrej Bauer Apr 05 '23 at 21:41
  • 1
    I was mistaken about "large elimination" and "dependent elimination" being the same thing: "large elimination" means creating a type by eliminating a term and "dependent elimination" means adding knowledge about some pattern being eliminated to the context. I still haven't found citeable information about either of these concepts but your help made me understand them better. Thanks! – Valmir Junior Apr 10 '23 at 13:35

1 Answers1

1

AFAIK, dependent elimination was introduced by Coquand in '92, under the name "dependent pattern matching", in the paper Pattern Matching with Dependent Types

Famously implemented in the Agda system, the main idea (and difference with, say, the default matching in Coq) is that there is additional information added in the right hand side of a case definition: say if you have

datatype Fin : nat -> Type = Zero : Fin (S 0) | Succ : forall k, Fin k -> Fin (S k)

f : forall n, Fin n -> nat
f _ Zero = ???
f _ (Succ f) = ???

Then in the first ???, you "know" the equation n = S 0 and in the second ??? you know n = S k, which in turn can allow you to typecheck some terms that would otherwise be ill-typed. Indeed, if there is no possible well-typed right hand side (say if you knew n = 0) then you wouldn't even need to write that case!

It turns out that to recover the entire power of this kind of pattern matching, it suffices to add the axiom K (which roughly states that every proof of x = x is refl) as described in Goguen, McBride and McKinna Eliminating Dependent Pattern Matching. Coquand had previously noticed that K is provable in the presence of dependent pattern matching, so the two are roughly equivalent (up to some computational rules).

Large elimination is the ability to eliminate to Type, e.g. defining f 0 = Bool, f (S n) = Nat -> f n. One can notice that this enables proving $0 \not = 1$, e.g. by defining f 0 = False and f (S _) = True and doing some simple rewriting. In a system like Coq, it is otherwise impossible to prove such a simple fact! Not sure who first noticed this.

cody
  • 13,861
  • 1
  • 49
  • 103