<p>For simply typed λ-calculus, a simultaneous substitution from <span class="math-container">$\Gamma$</span> to <span class="math-container">$\Delta$</span> is concretely a type-preserving map from variables in <span class="math-container">$\Delta$</span> to terms in <span class="math-container">$\Gamma$</span>. See, for example, <a href="https://plfa.github.io/Substitution/#2405" rel="nofollow noreferrer">Programming Language Foundations in Agda (PLFA)</a> for a rigorous definition (uppercase <code>Subst</code>). Similarly, a simultaneous <em>renaming</em> from <span class="math-container">$\Gamma$</span> to <span class="math-container">$\Delta$</span> is a type-preserving map from variables in <span class="math-container">$\Delta$</span> to <em>variables</em> in <span class="math-container">$\Gamma$</span>. The functions <code>subst</code> and <code>rename</code> from PLFA interpret such a substitution or renaming as a function of type <span class="math-container">$\forall A.~(\Delta \vdash A) \to (\Gamma \vdash A)$</span>, that is, a function mapping any term of arbitrary type <span class="math-container">$A$</span> in context <span class="math-container">$\Delta$</span> to a term of type <span class="math-container">$A$</span> in context <span class="math-container">$\Gamma$</span>.</p>
<p>My intuition is that simultaneous substitutions can be characterised more abstractly by saying that a simultaneous substitution from <span class="math-container">$\Gamma$</span> to <span class="math-container">$\Delta$</span> is a family of derivations from <span class="math-container">$\Delta \vdash A$</span> to <span class="math-container">$\Gamma \vdash A$</span> natural* in <span class="math-container">$A$</span>. Similarly, a simultaneous renaming can be characterised as such a family of derivations using only structural rules. These definitions should characterise the range of the functions <code>subst</code> and <code>rename</code>.</p>
<p>The abstract definitions should be related to the more concrete definitions by the Yoneda lemma, or something like that. Have they been worked out and written down? In particular, it feels like the abstract definitions could be quite sensitive to the presentation of the calculus, or else appear circular. For example, the family of derivations for the substitution from <span class="math-container">$A \to B, A$</span> to <span class="math-container">$B$</span> looks like the following. But it relies on substitution (bottom) and explicit weakening (right). Maybe that doesn't matter, though, given that, in practice, we'll always use <code>subst</code> to construct the required transformations.
<span class="math-container">$$
{\overline{A \to B, A \vdash A \to B} \qquad \overline{A \to B, A \vdash A} \over A \to B, A \vdash B} \qquad {B \vdash C \over A \to B, A, B \vdash C}
\over
A \to B, A \vdash C
$$</span></p>
<p>Also, where I have put a * next to “natural”, I don't know what the categorical structure should be. It feels like naturality because we can't use any specifics of each individual <span class="math-container">$A$</span> to construct the substitution (in contrast to <span class="math-container">$\Gamma$</span> and <span class="math-container">$\Delta$</span>). However, naturality in <span class="math-container">$A$</span> could be wrong. For instance, we know that substitutions preserve a lot of the structure of the <span class="math-container">$\Delta \vdash A$</span> derivation, modifying only the free variables. I don't know whether naturality in <span class="math-container">$A$</span> is enough to derive this.</p>

CC BY-SA 4.0
2021-06-23T06:59:34.823Z
What is a "derivation from $\Delta \vdash A$ to $\Gamma \vdash A$? In fact, what do you mean by $\Gamma \vdash A$, that $A$ is a well-formed type in context $\Gamma$, or that it is inhabited? You should also explain what you mean by "natural in $A$". Natural with respect to what categorical structure?
Andrej Bauer
CC BY-SA 4.0
2021-06-23T09:43:22.437Z
I'll edit to clarify. For the earlier questions, the example at the bottom is a derivation from $B \vdash C$ to $A \to B, A \vdash C$ – take the former as an axiom and derive the latter. As for what exactly “natural” means, that's part of the question. I hope someone else has worked it out because I don't know.
mudri
CC BY-SA 4.0
2021-06-23T10:52:33.997Z
Are you also looking for references that explain renamings and sustitutions in ways that your question does not anticpate? For example, there is a well-known setup in which substiutions are the morphisms of a Kleisly category for the syntax-forming monad.
Andrej Bauer
CC BY-SA 4.0
2021-06-23T13:19:50.897Z
Yes, I think I would find the details of that setup useful. Maybe I should say: I'm particularly interested in anything that will generalise beyond contexts being Cartesian products, to instead be general monoidal products. I have a notion of simultaneous substitution for linear STλC (in the QTT/semiring-annotated style), and I'm trying to find a way to explain/motivate/justify it. Maybe there's some category of finite multisets, or otherwise “resourceful” sets, in which I could replay the usual universal algebra stuff.
mudri
<reference-request><pl.programming-languages><type-theory>
Reference request: characterisation of simultaneous substitution
mudri
# Reference request: characterisation of simultaneous substitution

(Asked by: username_0 on 2021-06-22)

For simply typed λ-calculus, a simultaneous substitution from $\Gamma$ to $\Delta$ is concretely a type-preserving map from variables in $\Delta$ to terms in $\Gamma$. See, for example, [Programming Language Foundations in Agda (PLFA)](https://plfa.github.io/Substitution/#2405) for a rigorous definition (uppercase `Subst`). Similarly, a simultaneous *renaming* from $\Gamma$ to $\Delta$ is a type-preserving map from variables in $\Delta$ to *variables* in $\Gamma$. The functions `subst` and `rename` from PLFA interpret such a substitution or renaming as a function of type $\forall A.~(\Delta \vdash A) \to (\Gamma \vdash A)$, that is, a function mapping any term of arbitrary type $A$ in context $\Delta$ to a term of type $A$ in context $\Gamma$.

My intuition is that simultaneous substitutions can be characterised more abstractly by saying that a simultaneous substitution from $\Gamma$ to $\Delta$ is a family of derivations from $\Delta \vdash A$ to $\Gamma \vdash A$ natural\* in $A$. Similarly, a simultaneous renaming can be characterised as such a family of derivations using only structural rules. These definitions should characterise the range of the functions `subst` and `rename`.

The abstract definitions should be related to the more concrete definitions by the Yoneda lemma, or something like that. Have they been worked out and written down? In particular, it feels like the abstract definitions could be quite sensitive to the presentation of the calculus, or else appear circular. For example, the family of derivations for the substitution from $A \to B, A$ to $B$ looks like the following. But it relies on substitution (bottom) and explicit weakening (right). Maybe that doesn't matter, though, given that, in practice, we'll always use `subst` to construct the required transformations.
$$
{\overline{A \to B, A \vdash A \to B} \qquad \overline{A \to B, A \vdash A} \over A \to B, A \vdash B} \qquad {B \vdash C \over A \to B, A, B \vdash C}
\over
A \to B, A \vdash C
$$

Also, where I have put a \* next to “natural”, I don't know what the categorical structure should be. It feels like naturality because we can't use any specifics of each individual $A$ to construct the substitution (in contrast to $\Gamma$ and $\Delta$). However, naturality in $A$ could be wrong. For instance, we know that substitutions preserve a lot of the structure of the $\Delta \vdash A$ derivation, modifying only the free variables. I don't know whether naturality in $A$ is enough to derive this.

**Tags:** reference-request, pl.programming-languages, type-theory
> **Comments:**
> **username_1**: What is a "derivation from $\Delta \vdash A$ to $\Gamma \vdash A$? In fact, what do you mean by $\Gamma \vdash A$, that $A$ is a well-formed type in context $\Gamma$, or that it is inhabited? You should also explain what you mean by "natural in $A$". Natural with respect to what categorical structure?  
> **username_0**: I'll edit to clarify. For the earlier questions, the example at the bottom is a derivation from $B \vdash C$ to $A \to B, A \vdash C$ – take the former as an axiom and derive the latter. As for what exactly “natural” means, that's part of the question. I hope someone else has worked it out because I don't know.  
> **username_1**: Are you also looking for references that explain renamings and sustitutions in ways that your question does not anticpate? For example, there is a well-known setup in which substiutions are the morphisms of a Kleisly category for the syntax-forming monad.  
> **username_0**: Yes, I think I would find the details of that setup useful. Maybe I should say: I'm particularly interested in anything that will generalise beyond contexts being Cartesian products, to instead be general monoidal products. I have a notion of simultaneous substitution for linear STλC (in the QTT/semiring-annotated style), and I'm trying to find a way to explain/motivate/justify it. Maybe there's some category of finite multisets, or otherwise “resourceful” sets, in which I could replay the usual universal algebra stuff.  

---

## 0 answers

