<p>The most general form of substitution theorems speaks about arbitrary contexts:</p>

<ol>
<li><p>Define what it means to have a substitution <span class="math-container">$\sigma : \Gamma \to \Delta$</span> from a context <span class="math-container">$\Gamma$</span> to a context <span class="math-container">$\Delta$</span> (it's a simultaneous substitution giving a term <span class="math-container">$\Gamma \vdash e : A$</span> for every <span class="math-container">$y : A$</span> appearing in <span class="math-container">$\Delta$</span>, and in case of type dependencies we have to do it recursively).</p></li>
<li><p>Prove that if <span class="math-container">$\Delta \vdash e : A$</span> then <span class="math-container">$\Gamma \vdash e\sigma : A\sigma$</span>.</p></li>
</ol>

<p>In such generality there is no reliance on exchange rules and it all works in dependent type theory as well. The case suggested by Max New in his answer is a special case.</p>

CC BY-SA 4.0
2018-10-30T16:01:26.690Z
2018-10-30T16:16:44.833Z
2018-10-30T16:16:44.833Z
Andrej Bauer
<p>The property, which I would call "typing of substitution" should hold in any type theory, and is not dependent on the <em>exchange</em> property (which I assume is what you mean by permutation)</p>

<p>The key is that you need to generalize the inductive hypothesis to when the variable in t appears in a context. So for a dependent type theory you prove</p>

<ul>
<li>If <span class="math-container">$\Gamma \vdash t_1 : \tau_1$</span> and <span class="math-container">$\Gamma, x : \tau_1, \Delta \vdash t_2 : \tau_2$</span> then <span class="math-container">$\Gamma,\Delta[t_1/x] \vdash t_2[t_1/x] : \tau_2[t_1/x]$</span></li>
</ul>

<p>For a reference, see Lemma 2.3.2 on page 55 in Advanced Topics in Types and Programming Languages. </p>

CC BY-SA 4.0
2018-10-30T08:43:01.937Z
Or even better: prove an even more general version corresponding to parallel substitution.
gallais
CC BY-SA 4.0
2018-10-30T00:00:37.953Z
2018-10-30T18:02:43.270Z
2018-10-30T18:02:43.270Z
Max New
<p>In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution":</p>

<ul>
<li>If <span class="math-container">$\Gamma \vdash v : \tau_1$</span> and <span class="math-container">$(x : \tau_1) \vdash t : \tau_2$</span>,
then <span class="math-container">$\Gamma \vdash [v/x]t : \tau_2 $</span>.</li>
</ul>

<p>However, the proof of this relies on the property of <em>permutation</em>, that we can rearrange contexts and it will preserve typing of terms.</p>

<p>I'm wondering, can we prove a similar property for dependently typed languages? The problem is that, here, permutation may not hold, since telescopes are used in place of environments, and the types themselves may refer to variables. Moreover, since the types and terms overlap, we have to substitute in <span class="math-container">$\Gamma$</span> and <span class="math-container">$\tau_2$</span> as well.</p>

<p>Does anyone have a good reference to proving such a preservation property for a dependently typed language? Are there tricks that are used to avoid the permutations?</p>

<reference-request><pl.programming-languages><type-theory><lambda-calculus><dependent-type>
Preservation under Substitution with Telescopes
Joey Eremondi
# Preservation under Substitution with Telescopes

(Asked by: username_0 on 2018-10-29)

In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution":

* If $\Gamma \vdash v : \tau\_1$ and $(x : \tau\_1) \vdash t : \tau\_2$,
  then $\Gamma \vdash [v/x]t : \tau\_2 $.

However, the proof of this relies on the property of *permutation*, that we can rearrange contexts and it will preserve typing of terms.

I'm wondering, can we prove a similar property for dependently typed languages? The problem is that, here, permutation may not hold, since telescopes are used in place of environments, and the types themselves may refer to variables. Moreover, since the types and terms overlap, we have to substitute in $\Gamma$ and $\tau\_2$ as well.

Does anyone have a good reference to proving such a preservation property for a dependently typed language? Are there tricks that are used to avoid the permutations?

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

---

## 2 answers

### Answer by username_2 on 2018-10-30. Score: 8 | Accepted answer

The property, which I would call "typing of substitution" should hold in any type theory, and is not dependent on the *exchange* property (which I assume is what you mean by permutation)

The key is that you need to generalize the inductive hypothesis to when the variable in t appears in a context. So for a dependent type theory you prove

* If $\Gamma \vdash t\_1 : \tau\_1$ and $\Gamma, x : \tau\_1, \Delta \vdash t\_2 : \tau\_2$ then $\Gamma,\Delta[t\_1/x] \vdash t\_2[t\_1/x] : \tau\_2[t\_1/x]$

For a reference, see Lemma 2.3.2 on page 55 in Advanced Topics in Types and Programming Languages.

> **Comments:**
> **username_3**: Or even better: prove an even more general version corresponding to parallel substitution.  

---

### Answer by username_1 on 2018-10-30. Score: 10

The most general form of substitution theorems speaks about arbitrary contexts:

1. Define what it means to have a substitution $\sigma : \Gamma \to \Delta$ from a context $\Gamma$ to a context $\Delta$ (it's a simultaneous substitution giving a term $\Gamma \vdash e : A$ for every $y : A$ appearing in $\Delta$, and in case of type dependencies we have to do it recursively).
2. Prove that if $\Delta \vdash e : A$ then $\Gamma \vdash e\sigma : A\sigma$.

In such generality there is no reliance on exchange rules and it all works in dependent type theory as well. The case suggested by Max New in his answer is a special case.


---

