Intuitively, a substitution changes all free occurrence of the variable in to .

Definition

substitution is defined as following

  1. and if .
  2. (where is an operator).

Example

Notation Problem

There are various different substitution notations used in the wild: substitution notations.png

One big problem is that the forms and are frequently used for substitution, but are also widely used for another purpose: function update (also called map update or storage update):

Some papers even use of both meaning of the same syntax in the same paper, while made them are hard to read 1

References

Footnotes

  1. Invited Talk - Guy Steele - YouTube