# 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 , in which you want to replace every occurrence of a variable (or any other fixed subexpression, for that matter) with another variable (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:

- (“ is transformed into ”)
- (“ is replaced with ”)
- (“assign to every occurrence of )
- (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 with ” or “replace with ”?). 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 and :

“Think of it as falling over and squishing the .”

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