Intuitively, a substitution
Definition
substitution is defined as following
and if . (where is an operator).
Example
Notation Problem
There are various different substitution notations used in the wild:
One big problem is that the forms
Some papers even use of both meaning of the same syntax in the same paper, while made them are hard to read 1
References
- Practical Foundations for Programming Languages Chapter 1
- Smith, Nicholas J.J.. Logic : The Laws of Truth, Princeton University Press, 2012. Chapter 9