Substitution mnemonic

(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 ¹. In formal logic, $\lambda$-calculus, etc. there exists a bewildering soup of notations representing this simple transformation:

• $E[x \to y]$ (“$x$ is transformed into $y$”)
• $E[x \gets 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 $y$ falling over and squishing the $x$.”