notations for variable substitution
- categories
- notation
The following are all accepted notations for “substitute term \( t_2 \) for variable \( x \) in term \( t_1 \)”:
- \( [t_2 / x]t_1 \);
- \( [x / t_2]t_1 \);
- \( t_1[t_2 / x] \);
- \( t_1[x / t_2] \);
- \( t_1[x \mapsto t_2]\);
- \( t_1[x \coloneq t_2]\).
Yes, both \( [t_2 / x] \) and \( [x / t_2] \) are accepted notations. The former is more common; read “\( t_2 \) for \( x \).” Also, prefix notations like \( [-]t \) are more common than suffix notations like \( t[-] \). Think of it as: the stuff inside the brackets is the literal form of a particular kind of function, and applications of such functions are written in the usual prefix form, just without parentheses.
Some treatments take a higher-level view in which a substitution is a mapping from variable names to terms. By analogy with the above notations, such treatments may denote the action of a substitution \( \sigma \) on a term \( t \) by one of the following:
- \( [\sigma]t \);
- \( t[\sigma] \).
However, they may also use standard function application notation; e.g., \( \sigma(t) \) or \( \sigma t \).