# Composition in explicit substitutions

In the classical λσ calculus of explicit substitutions, there is the following rewrite rule:

(a[s])[t]  ==>  a[s ∘ t]


where a[s] denotes the application of substitution s to term a.

This seems backward/counterintuitive to me: if we consider substitutions as sorts of functions, then (a[s])[t] can be thought of as t(s(a)), which we could write as (t ∘ s)(a) aka a[t ∘ s] and not a[s ∘ t].

What is the reasoning behind this notation?

• Do you mind giving the reference from where you're getting this notation? – cody Apr 16 '16 at 3:10
• The reference is in my answer. – Andrej Bauer Apr 16 '16 at 8:03

Substitutions form a monoid and they act on terms. We have a choice of writing them as either left or right actions. Sometime in the previous millenium someone decided they act on the right (page 5). A right action should satisfy $a [s \circ t] = (a[s])[t]$, so it makes sense to define the operation $\circ$ that conforms to action on the right. That's all.
You could do entirely the same thing with functions and write them as $x \mathbin{//} f$ (as Mathematica does) in which case you would be seriously tempted to define $x \mathbin{//} (f \circ g) = (x \mathbin{//} f) \mathbin{//} g$. In essence you'd move from the category of sets to its opposite.
• Ha! And here I was thinking that f∘g always means "apply g and then apply f". I guess it's the first time I see this composition notation used on what you call "right actions" (which I tend to think as postfix operations). Thanks. – Stefan Apr 16 '16 at 13:54