2
$\begingroup$

I'd like to ask a question on type theory:

Consider the usual type theoretical definition of the natural numbers. We could give an elimination rule in the form: enter image description here or in the form: enter image description here

I called the costants in the elimination rules $NatCata$ and $NatPara$ for the parallel with catamorphisms and paramorphisms recursion schemas. I also omitted the computation rules, as they are well known.

Now, this two ways to introduce the elimination rules let us build the same functions (in the sense in which a function is his graph), but other details are different (for example, the length of the derivation in the computation of a function; the pseudo-predecessor function expressed with the $NatCata$ version has to recur on all the structure, while with $NatPara$ is always a single step).

What I want to know is this: is there any reason why we insist on having a unique elimination rule?

Examples of such reasons may be theorems which are easier to state/proof, or other meta-theoretic properties.

Could we have different elimination rules, if they are automatically determined by the introduction rules (as in this case?). Would a logician consider this approach tasteful?

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ The elimination rule for nat in dependent type theory has C being a type family over nat and both your elimination rules are special cases of that one. $\endgroup$
    – François G. Dorais
    Commented Jun 26, 2015 at 20:49
  • $\begingroup$ @FrançoisG.Dorais suppose for a moment that I'm not in the dependent setting. It's important for a type theory that the elimination rule is unique, or could we see various elimination rules as various ways to destruct a term, with different computational properties? $\endgroup$
    – meditans
    Commented Jun 26, 2015 at 21:01
  • 1
    $\begingroup$ You may end up with two terms that are 'visibly identical' but not definitionally equal unless you add more rules to fix this. Why not define the first as a special case of the second? Derived rules are fine... $\endgroup$
    – François G. Dorais
    Commented Jun 26, 2015 at 21:10
  • $\begingroup$ You make a great point here. I indeed the simple definitional equality. Thanks! $\endgroup$
    – meditans
    Commented Jun 27, 2015 at 11:27

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .