In the classical λσ calculus of explicit substitutions, there is the following rewrite rule:
(a[s])[t] ==> a[s ∘ t]
a[s] denotes the application of substitution
s to term
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?