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

  • $\begingroup$ 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? $\endgroup$ Jun 23 at 6:59
  • $\begingroup$ 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. $\endgroup$
    – mudri
    Jun 23 at 9:43
  • $\begingroup$ 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. $\endgroup$ Jun 23 at 10:52
  • $\begingroup$ 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. $\endgroup$
    – mudri
    Jun 23 at 13:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.