<p>Substitutions form a monoid and they <a href="https://en.wikipedia.org/wiki/Semigroup_action">act on terms</a>. We have a choice of writing them as either <em>left</em> or <em>right</em> actions. <a href="http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-54.pdf">Sometime in the previous millenium someone decided they act on the right</a> (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.</p>

<p>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.</p>

CC BY-SA 3.0
2016-04-16T13:54:21.817Z
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
CC BY-SA 3.0
2016-04-16T07:59:13.630Z
2016-04-16T08:05:08.427Z
2016-04-16T08:05:08.427Z
Andrej Bauer
<p>In the classical λσ calculus of explicit substitutions, there is the following rewrite rule:</p>

<pre><code>(a[s])[t]  ==&gt;  a[s ∘ t]
</code></pre>

<p>where <code>a[s]</code> denotes the application of substitution <code>s</code> to term <code>a</code>.</p>

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

<p>What is the reasoning behind this notation?</p>

CC BY-SA 3.0
2016-04-16T03:10:13.623Z
Do you mind giving the reference from where you're getting this notation?
cody
CC BY-SA 3.0
2016-04-16T08:03:00.820Z
The reference is in my answer.
Andrej Bauer
<lambda-calculus><term-rewriting-systems>
Composition in explicit substitutions
Stefan
# Composition in explicit substitutions

(Asked by: username_0 on 2016-04-16)

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?

**Tags:** lambda-calculus, term-rewriting-systems

> **Comments:**
> **username_1**: Do you mind giving the reference from where you're getting this notation?  
> **username_2**: The reference is in my answer.  

---

## 1 answers

### Answer by username_2 on 2016-04-16. Score: 8 | Accepted answer

Substitutions form a monoid and they [act on terms](https://en.wikipedia.org/wiki/Semigroup_action). 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](http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-54.pdf) (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.

> **Comments:**
> **username_0**: 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.  

---

