2
$\begingroup$

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?

$\endgroup$
2
  • 1
    $\begingroup$ Do you mind giving the reference from where you're getting this notation? $\endgroup$
    – cody
    Apr 16 '16 at 3:10
  • 1
    $\begingroup$ The reference is in my answer. $\endgroup$ Apr 16 '16 at 8:03
8
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ 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. $\endgroup$
    – Stefan
    Apr 16 '16 at 13:54

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.