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 .”

  1. 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.