(This article was originally published at Blog - Alex Polozov. See Substitution mnemonics for more comments and better formatting.)

*(I overheard this at UW, from a graduate student who told me he doesn’t know the original author of this mnemonic either. Please do not attribute it to either of us* ☺*)*.

In PL and formal logic, there exists a common notation, which I personally consider the worst possible notation choice of all times. Let’s say you have an expression *E*, in which you want to replace every occurrence of a variable *x* (or any other fixed subexpression, for that matter) with another variable *y* (again, or any other expression). This operation is called *substitution*^{1}. In formal logic, λ-calculus, etc. there exists a bewildering soup of notations representing this simple transformation:

**E[x → y]**(“*x*is transformed into*y*”)**E[x ← y]**(“*x*is replaced with*y*”)**E[x := y]**(“assign*y*to every occurrence of*x*”)**E[y/x]**(WTF?)

The first two (and their mirrored alternatives) are confusing on its own – you never know which substitution direction the arrow represents (is it “replace *x* with *y*” or “replace *y* with *x*”?). But the last one is notoriously ridiculous in that regard. It is *too symmetric*. How am I supposed to remember which variable substitutes the other one if the only thing denoting this relationship is a meaningless slash character in between? Some say this notation is the easiest to typeset – which is not true, because the third notation also doesn’t use any characters beyond standard ASCII, *and* it is unambiguous. Anyway, I usually tried to avoid the slash notation as much as possible whenever I could.

However, now I know a beautiful mnemonic, which breaks the “almost-symmetrical” relationship between *x* and *y*:

“Think of it as

yfalling over and squishing thex.”

- The actual formal definition of substitution is trickier, because you have to take into account which variables are free in
*E*, and which are bound. The details are outside the scope of this post. ↩