4
$\begingroup$

I'm studying type theory (mostly Coq) and often encounter the term "large elimination", usually when talking about type universes hierarchy consistency, for example:

impredicative polymorphism + excluded middle + large elimination => false

While I have an intuitive understanding of what it means, I wasn't been able to find or construct a more formal definition of what precisely is "large elimination".

In my understanding, large elimination is when a term t : T is eliminated (destructed) to get a value of type D, where D depends on the value of t.

For example, if vec_bool : nat -> Type is a type constructor for the boolean list of a fixed size with data constructors

nil  : vec_bool 0
cons : forall n:nat, bool -> vec_bool n -> vec_bool (S n)

the following recursive definition performs a large elimination on n:

Fixpoint construct_false_list (n:nat) : vec_bool n :=
   match n with
   | 0      => nil
   | Succ m => cons m false (construct_false_list m)
   end.

Is my understanding correct, or am I missing something?

$\endgroup$
  • 1
    $\begingroup$ section 3 of github.com/jdolson/hott-notes/blob/pdfs/pdfs/notes_week5.pdf may help. There are also videos for the entire class if you want to dig in. $\endgroup$ – user833970 Mar 7 '18 at 16:25
  • 1
    $\begingroup$ "a term t : T is eliminated (destructed) to get a value of type D, where D depends on the value of t" <- this is called "dependent elimination" $\endgroup$ – Jason Gross Mar 7 '18 at 20:29
6
$\begingroup$

You are incorrect about the definition of large elimination: it refers to the ability to build values of type $\mathrm{Type}$ by eliminating an inductive value. The canonical example:

bool_to_type : bool -> Type := fun b =>
     match b with
         | true => Unit
         | false => Empty

Where Unit and Empty are inductive types with 1 and 0 constructors, respectively. Notably, this allows you to prove the proposition $0 \not= 1$, which cannot be proven without this ability.

As noted in another answer (https://cstheory.stackexchange.com/a/21878/3984) a good resource that explains this is the following github repo: https://github.com/FStarLang/FStar/issues/360

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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