11
$\begingroup$

I've read about hereditary substitution for the Simple Lambda Calculus and for The Logical Framework with distinct terms and types.

I'm wondering, are there any examples of hereditary substitution in a dependently typed system with a universe hierarchy? i.e. where $ True : Set_0 : Set_1:Set_2$ etc.

I'm wondering in particular how to establish an induction measure in such a system. The simply typed version is structurally decreasing in the type of the variable being replaced. This doesn't work work with dependent types, to for LF the paper I linked uses the simply-typed erasure of the terms, performing induction on the shape of the type.

However, erasing to simple types doesn't work with a universe hierarchy, since if you have something like this:

  • $ f : (x : Set_1)\to x \to True$ implies that
  • $ f\ ((y : True) \to True \to True ): True \to True \to True$

i.e. applying a function resulted in a structurally larger type.

I'm assuming the solution has something to do with the universe indexes, but if there's an existing technique for establishing that the induction is well founded, I'd prefer to cite it rather than coming up with something up on my own.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
8
$\begingroup$

Here's a reference for predicative System F. The measure indeed includes the multiset of universe levels in a type. I can't say much about whether this approach generalizes to predicative dependent type theory.

Improve this answer
$\endgroup$
9
$\begingroup$

As of November 2018, how to do this for dependent type theories with large eliminations is an open question.

Establishing that the recursion is well-founded is not too bad; you can use Pataraia's theorem to prove the fixed point you want exists. See Robert Harper's *Constructing Type Systems Over an Operational Semantics for a how-to. (You can also do this via an inductive-recursive definition.)

The hard part is actually formulating the hereditary substitution in a nice way -- the natural direction leads you towards substituting not one term, but an entire substitution for a context, and this raises a lot of questions about when and how to establish properties of things like compositions of (hereditary) substitutions.

If it turned out to be impossible, I would be utterly shocked. However, at present no one has done it. If you want to work on this, I would suggest getting in touch with Andreas Abel, Dan Licata and Mike Shulman. (Or me, for that matter.)

Improve this answer
$\endgroup$
10
  • $\begingroup$ Isn't the consistency strength of a hereditary substitutions theorem for a type theory with a universe hierachy quite strong? After you've go the theorem, what else is needed to derive consistency of the theory? $\endgroup$
    – Andrej Bauer
    Commented Nov 23, 2018 at 19:10
  • 1
    $\begingroup$ @NeelKrishaswami: do you mean it's an open problem even without a universe hierachy? How much exactly do you assume about your type theory, precisely? $\endgroup$
    – Andrej Bauer
    Commented Nov 23, 2018 at 23:53
  • 2
    $\begingroup$ I second @AndrejBauer's confusion: doesn't the definition of hereditary substitution implicitly contain a termination argument for reduction of well-typed terms? The argument for simple types seems to even explicitly contain an order which decreases when the substitution is carried-out, which is finicky even for System T (it's open whether such an order exists for SN) and hopeless for system F. $\endgroup$
    – cody
    Commented Nov 24, 2018 at 4:13
  • 1
    $\begingroup$ @AndrejBauer: If you write down a hereditary substitution operation, you have to prove that it terminates before you can really call it a function. The proof of termination is unlikely to be terribly hard, because MLTT with a countable universe hierarchy can be shown to normalize using intuitionistic bounded ZF. What is open is actually giving the correct definition of the hereditary substitution operation. Right now it's unclear whether it is a difficult bureaucratic problem, or a difficult problem full stop. My hunch is the former, but who can really say without doing the work? $\endgroup$
    – Neel Krishnaswami
    Commented Nov 26, 2018 at 16:17
  • 1
    $\begingroup$ @Blaisorblade: yeah, adding large eliminations leads to a really big jump in the expressive power of the theory. Once you have large eliminations, the metatheory you prove consistency/normalization in has to support induction-recursion at a minimum. $\endgroup$
    – Neel Krishnaswami
    Commented Feb 20, 2019 at 10:19

Your Answer

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

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