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

<p>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 <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.423.1623" rel="noreferrer">*Constructing Type Systems Over an Operational Semantics</a> for a how-to. (You can also do this via an inductive-recursive definition.)</p>

<p>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. </p>

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

CC BY-SA 4.0
2018-11-23T19:10:57.683Z
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
CC BY-SA 4.0
2018-11-23T20:15:08.243Z
@AndrejBauer not much is needed, hereditary substitution returns normal forms, and simple induction on normal forms shows consistency.
András Kovács
CC BY-SA 4.0
2018-11-23T22:00:50.663Z
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
CC BY-SA 4.0
2018-11-23T23:51:27.010Z
Large elimination means elimination into types, e.g., constructing a type family `P`over `bool` by specifying `P false` and `P true`.
Andrej Bauer
CC BY-SA 4.0
2018-11-23T23:53:07.840Z
@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
CC BY-SA 4.0
2018-11-24T04:13:30.420Z
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
CC BY-SA 4.0
2018-11-26T16:17:35.397Z
@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
CC BY-SA 4.0
2019-02-14T23:07:05.877Z
@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
CC BY-SA 4.0
2019-02-19T22:34:56.780Z
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
CC BY-SA 4.0
2019-02-20T10:19:16.353Z
@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
CC BY-SA 4.0
2018-11-23T12:06:54.350Z
2018-11-23T12:06:54.350Z
Neel Krishnaswami
<p>Here's a <a href="https://arxiv.org/pdf/1508.00455.pdf" rel="nofollow noreferrer">reference</a> 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. </p>

CC BY-SA 4.0
2018-11-23T07:47:21.480Z
2018-11-23T15:57:54.390Z
2018-11-23T15:57:54.390Z
András Kovács
<p>I've read about hereditary substitution for the <a href="https://www.cs.cmu.edu/~fp/papers/andrews08.pdf" rel="noreferrer">Simple Lambda Calculus</a> and for <a href="https://www.cs.cmu.edu/~rwh/papers/mech/jfp07.pdf" rel="noreferrer">The Logical Framework</a> with distinct terms and types.</p>

<p>I'm wondering, are there any examples of hereditary substitution in a dependently typed system with a universe hierarchy? i.e. where <span class="math-container">$ True : Set_0 : Set_1:Set_2$</span> etc.</p>

<p>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.</p>

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

<ul>
<li><span class="math-container">$ f : (x : Set_1)\to x \to True$</span> implies that</li>
<li><span class="math-container">$ f\ ((y : True) \to True \to True ): True \to True \to True$</span></li>
</ul>

<p>i.e. applying a function resulted in a structurally larger type.</p>

<p>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.</p>

<reference-request><lo.logic><pl.programming-languages><type-theory><lambda-calculus>
Hereditary substitution with a universe hierarchy
Joey Eremondi
# Hereditary substitution with a universe hierarchy

(Asked by: username_0 on 2018-11-22)

I've read about hereditary substitution for the [Simple Lambda Calculus](https://www.cs.cmu.edu/~fp/papers/andrews08.pdf) and for [The Logical Framework](https://www.cs.cmu.edu/~rwh/papers/mech/jfp07.pdf) 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.

**Tags:** reference-request, lo.logic, pl.programming-languages, type-theory, lambda-calculus

---

## 2 answers

### Answer by username_3 on 2018-11-23. Score: 8 | Accepted answer

Here's a [reference](https://arxiv.org/pdf/1508.00455.pdf) 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.


---

### Answer by username_1 on 2018-11-23. Score: 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](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.423.1623) 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.)

> **Comments:**
> **username_2**: 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?  
> **username_3**: @AndrejBauer not much is needed, hereditary substitution returns normal forms, and simple induction on normal forms shows consistency.  
> **username_0**: 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}$?  
> **username_2**: Large elimination means elimination into types, e.g., constructing a type family `P`over `bool` by specifying `P false` and `P true`.  
> **username_2**: @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?  
> **username_4**: 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.  
> **username_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?  
> **username_0**: @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.  
> **username_5**: 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?  
> **username_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.  

---

