11

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.

Bjørn Kjos-Hanssen
  • 4,485
  • 2
  • 25
  • 40
Joey Eremondi
  • 2,832
  • 15
  • 29

2 Answers2

9

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.)

Neel Krishnaswami
  • 32,528
  • 1
  • 100
  • 165
  • 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? – Andrej Bauer Nov 23 '18 at 19:10
  • @AndrejBauer not much is needed, hereditary substitution returns normal forms, and simple induction on normal forms shows consistency. – András Kovács Nov 23 '18 at 20:15
  • When you say "large eliminations", do you mean with eliminators for large inductive data types? Or does this include LF-like systems with just $\lambda,\Pi$ and $\mathsf{Set}$? – Joey Eremondi Nov 23 '18 at 22:00
  • Large elimination means elimination into types, e.g., constructing a type family Pover bool by specifying P false and P true. – Andrej Bauer Nov 23 '18 at 23:51
  • 1
    @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? – Andrej Bauer Nov 23 '18 at 23:53
  • 2
    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. – cody Nov 24 '18 at 04:13
  • 1
    @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?

     – Neel Krishnaswami Nov 26 '18 at 16:17
  • @NeelKrishnaswami You say this is hard for large eliminations. Do you have any resources or intuitions for hereditary substitution with small-eliminations? i.e. a nat-fold that where the result is restricted to be of a small type? Either way, thanks for the answer, this is very helpful. – Joey Eremondi Feb 14 '19 at 23:07
  • How would one reconcile this with https://cstheory.stackexchange.com/a/21543/989 ? "For weak logics (anything up to first-order logic without induction, roughly), you can prove normalization syntactically, using the technique of hereditary substitution". Or would the termination proof for hsubst go beyond PA and not be fully syntactic? – Blaisorblade Feb 19 '19 at 22:34
  • 1
    @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. – Neel Krishnaswami Feb 20 '19 at 10:19
8

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.

András Kovács
  • 1,629
  • 9
  • 8