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?

$\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$ 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
    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$ Jun 26, 2015 at 21:10
  • $\begingroup$ You make a great point here. I indeed the simple definitional equality. Thanks! $\endgroup$
    – meditans
    Jun 27, 2015 at 11:27

0

Your Answer

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

Browse other questions tagged or ask your own question.