Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
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?
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.
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.
$\endgroup$