<p>The key observation is that whether the substitution theorem holds, <em>depends on the definition of substitution</em>. </p>

<p>For the usual definition of substitution of terms for variables, the substitution theorem is only true for substituting synthesizing terms for variables. </p>

<p>Indeed, if you introduce separate grammatical classes for synthesizing and checking terms, then using the usual substitution operation to replace a variable with a checking term will leave you with an ungrammatical expression. So this suggests that the usual substitution operation is the wrong definition.</p>

<p>However, this leaves you with the option of defining a <em>different</em> substitution operation. The keyword to search for is "hereditary substitution". It's based on two key observations: </p>

<ol>
<li><p>If you replace a variable with an introduction form at an elimination site (eg, replace the <span class="math-container">$f$</span> in <span class="math-container">$f\;x$</span> with a lambda) then you can just do the reduction as part of the substitution. </p></li>
<li><p>Next, you can turn synthesizing terms into checking terms by <span class="math-container">$\eta$</span>-expanding them. That is, if <span class="math-container">$f$</span> is a variable of type <span class="math-container">$X \to Y$</span>, you can turn it into the introduction form <span class="math-container">$\lambda x:X.\;f\,x$</span>.</p></li>
</ol>

<p>One paper you might want to look at in addition to the ones that gallais pointed you at is my paper with Nick Benton, <a href="https://www.cl.cam.ac.uk/~nk480/icfp11-krishnaswami-benton.pdf" rel="noreferrer"><em>A Semantic Model of Graphical User Interfaces</em></a>, which defines and proves the correctness of hereditary substitution for a mixed linear/intuitionistic calculus (in section 5). </p>

CC BY-SA 4.0
2018-11-02T16:48:27.227Z
You have a special talent for naming your papers. Actually, the talent extends to writing abstracts. Who would ever begin an abstract with "We give a denotational model for graphical user interface (GUI) programming using the Cartesian closed category of ultrametric spaces?"
Andrej Bauer
CC BY-SA 4.0
2018-11-02T11:29:46.523Z
2018-11-02T11:29:46.523Z
Neel Krishnaswami
<p>One solution is indeed to restrict to substituting with synthesizing expressions. You can only hope to replace variables with terms of the same mode (i.e. inferrable terms), anything else just won't fit. It is not that restrictive in the sense that usually a checkable term together with a type annotation gives you an inferrable term. This embedding is typically called <code>cut</code> because well... this is what it is. This restriction is described (and deployed) in <a href="https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf" rel="noreferrer">I Got Plenty o’ Nuttin’</a>.</p>

<p>Alternatively (which is also mentioned in IGPoN) you can define <a href="https://www.cs.cmu.edu/afs/cs.cmu.edu/Web/People/fp/papers/types03.pdf" rel="noreferrer">hereditary substitution</a> (<a href="http://www.cs.nott.ac.uk/~psztxa/publ/msfp10.pdf" rel="noreferrer">a formalised account for STLC</a>) whereby if you are about to form a redex because of the checkable you just plugged in, you fire it. And again. And again. And again. Until your substitution is not creating any new redexes.</p>

CC BY-SA 4.0
2018-11-02T09:46:34.363Z
2018-11-02T11:40:01.420Z
2018-11-02T11:40:01.420Z
gallais
<p>In most typed lambda calculi, we have the following lemma:</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>However, I'm wondering how we'd phrase such a lemma in a bidirectional typing system, with synthesis <span class="math-container">$\Rightarrow$</span> and checking <span class="math-container">$\Leftarrow$</span> judgements.</p>

<p>The main problem is that substitution does not preserve synthesis. For example, in most systems, <span class="math-container">$\Gamma \vdash x \Rightarrow T$</span> if <span class="math-container">$x : T \in \Gamma$</span>, but  <span class="math-container">$[(\lambda y \ldotp t)/x]x$</span> won't synthesize any type if there are only checking rules for <span class="math-container">$\lambda$</span>.</p>

<p>Potential solutions I can think of:</p>

<ol>
<li><p>Restrict to substituting with synthesizing expressions. This seems like it would give us the induction hypothesis we need (since, in most systems, all synthesizing expressions also check), but is very restrictive.</p></li>
<li><p>Only show that substitution preserves checking. This is a weaker result, and I'm unsure of whether it gives us a strong enough inductive hypothesis, since it would be difficult to rebuild typing derivations with synthesis judgements in the premises.</p></li>
</ol>

<p>This seems like a pretty basic metatheoretic property, so I'm sure I'm not the first one to have encountered this. Does anyone have a reference to a bidirectional system that cleanly solves these issues? Is there an obvious solution I am missing?</p>

CC BY-SA 4.0
2018-11-01T20:00:35.313Z
I'll try to find a reference but I think 1 is the right answer: the trick is if you want to substitute a checking-expression you just add a type annotation.
Max New
<pl.programming-languages><type-theory><lambda-calculus><type-systems><typed-lambda-calculus>
Typing of substitution in a bidirectional type system
Joey Eremondi
# Typing of substitution in a bidirectional type system

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

In most typed lambda calculi, we have the following lemma:

* 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]$

However, I'm wondering how we'd phrase such a lemma in a bidirectional typing system, with synthesis $\Rightarrow$ and checking $\Leftarrow$ judgements.

The main problem is that substitution does not preserve synthesis. For example, in most systems, $\Gamma \vdash x \Rightarrow T$ if $x : T \in \Gamma$, but $[(\lambda y \ldotp t)/x]x$ won't synthesize any type if there are only checking rules for $\lambda$.

Potential solutions I can think of:

1. Restrict to substituting with synthesizing expressions. This seems like it would give us the induction hypothesis we need (since, in most systems, all synthesizing expressions also check), but is very restrictive.
2. Only show that substitution preserves checking. This is a weaker result, and I'm unsure of whether it gives us a strong enough inductive hypothesis, since it would be difficult to rebuild typing derivations with synthesis judgements in the premises.

This seems like a pretty basic metatheoretic property, so I'm sure I'm not the first one to have encountered this. Does anyone have a reference to a bidirectional system that cleanly solves these issues? Is there an obvious solution I am missing?

**Tags:** pl.programming-languages, type-theory, lambda-calculus, type-systems, typed-lambda-calculus
> **Comments:**
> **username_1**: I'll try to find a reference but I think 1 is the right answer: the trick is if you want to substitute a checking-expression you just add a type annotation.  

---

## 2 answers

### Answer by username_2 on 2018-11-02. Score: 7 | Accepted answer

The key observation is that whether the substitution theorem holds, *depends on the definition of substitution*.

For the usual definition of substitution of terms for variables, the substitution theorem is only true for substituting synthesizing terms for variables.

Indeed, if you introduce separate grammatical classes for synthesizing and checking terms, then using the usual substitution operation to replace a variable with a checking term will leave you with an ungrammatical expression. So this suggests that the usual substitution operation is the wrong definition.

However, this leaves you with the option of defining a *different* substitution operation. The keyword to search for is "hereditary substitution". It's based on two key observations:

1. If you replace a variable with an introduction form at an elimination site (eg, replace the $f$ in $f\;x$ with a lambda) then you can just do the reduction as part of the substitution.
2. Next, you can turn synthesizing terms into checking terms by $\eta$-expanding them. That is, if $f$ is a variable of type $X \to Y$, you can turn it into the introduction form $\lambda x:X.\;f\,x$.

One paper you might want to look at in addition to the ones that gallais pointed you at is my paper with Nick Benton, [*A Semantic Model of Graphical User Interfaces*](https://www.cl.cam.ac.uk/~nk480/icfp11-krishnaswami-benton.pdf), which defines and proves the correctness of hereditary substitution for a mixed linear/intuitionistic calculus (in section 5).

> **Comments:**
> **username_3**: You have a special talent for naming your papers. Actually, the talent extends to writing abstracts. Who would ever begin an abstract with "We give a denotational model for graphical user interface (GUI) programming using the Cartesian closed category of ultrametric spaces?"  

---

### Answer by username_4 on 2018-11-02. Score: 7

One solution is indeed to restrict to substituting with synthesizing expressions. You can only hope to replace variables with terms of the same mode (i.e. inferrable terms), anything else just won't fit. It is not that restrictive in the sense that usually a checkable term together with a type annotation gives you an inferrable term. This embedding is typically called `cut` because well... this is what it is. This restriction is described (and deployed) in [I Got Plenty o’ Nuttin’](https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf).

Alternatively (which is also mentioned in IGPoN) you can define [hereditary substitution](https://www.cs.cmu.edu/afs/cs.cmu.edu/Web/People/fp/papers/types03.pdf) ([a formalised account for STLC](http://www.cs.nott.ac.uk/~psztxa/publ/msfp10.pdf)) whereby if you are about to form a redex because of the checkable you just plugged in, you fire it. And again. And again. And again. Until your substitution is not creating any new redexes.


---

