4
$\begingroup$

I'm wondering, is there any existing work on hereditary substitution with inductive type families and dependent eliminators?

In particular, normalizing the application of an eliminator to an inductive value "obviously" halts, since the head of the elimination is structurally smaller each time.

But, I'm wondering, how does it fit into the structurally-shrinking argument of hereditary substitution? For example, in Harper and Licata's presentation, hereditary substitution is always strictly decreasing, structurally in the value being substituted into, or in the shape of the type of the variable being replaced.

But, if we have:

$natElim: (m : Nat \to Set) \to m\ 0 \to (k : Nat \to m\ k \to m (succ\ k) ) \to (k : Nat) \to m\ k$

and we are computing $[1/x](natElim\ m\ z\ (\lambda k\ p\ldotp t_1)\ x)$, we must compute:

  • $[0/x](natElim\ m\ z\ s\ x) = t_2$,
  • $[0/k]t_2 = t_3$
  • $[t_2/p]t_3 =t_4$ to get a result of $t_4$.

But these are not decreasing in either the type of $x$ or the term being substituted into. The first two are decreasing in the value replacing the variable, but the third is not.

Is their prior work on this? I can think of ad-hoc ways to make the decreasing size argument work for Nat, Vec, etc. But is there a general argument for inductive types?

This is possibly related to my previous question question: I'm not sure if this falls under the "large eliminators" described there. If this only works for "small eliminators", I'm still interested in a reference for this.

Improve this question
$\endgroup$
1
  • 2
    $\begingroup$ Just my two cents, but I don't think you'll get anywhere without a significantly more subtle ordering, based on this (possibly incorrect) intuition: termination of hereditary substitution implies the normalization of the underlying calculus, which in turn can only be proven with a sufficiently strong meta-theory or assuming well-foundedness of a large order. In particular, the ordinal for simple types/LF only requires $\omega^2$, so a lex order will suffice, but system T will need at least $\varepsilon_0$, so expect a multiset ordering. $\endgroup$
    – cody
    Feb 8, 2019 at 20:57

0

Reset to default

Your Answer

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