Content deleted Content added
All variables are free… |
Free magma |
||
Line 8:
* A constant <math>a \in A</math> is an expression,
* A variable,
* If <math>e_1</math> and <math>e_2</math> are expressions, then <math>e_1 e_2</math> is an expression.
(In other words, they form the [[free magma]] over the disjoint union <math>A + V</math>.)
A term is ''closed'' if it contains no variables. A closed term may be ''evaluated'' in the natural way: a constant <math>a \in A</math> evaluates to itself, and if the terms <math>e_1</math> and <math>e_2</math> respectively evaluate to <math>a_1</math> and <math>a_2</math>, then <math>e_1 e_2</math> evaluates to <math>a_1 a_2</math>, if this is defined. Note that the evaluation is a partial operation, since not all applications are defined. A substitution operation is also defined in the natural way: if <math>t</math> is a term, <math>x</math> is a variable and <math>u</math> is another term, <math>t[u/x]</math> denotes the term <math>t</math> with all occurrences of <math>x</math> replaced by <math>u</math>. We write <math>t \downarrow</math> to simultaneously express that the term <math>t</math> evaluates to a defined value and denote this value (this matches standard notation for values of [[partial functions]]). We also write <math>t \simeq u</math> when both closed terms <math>t</math> either do not evaluate to a defined value, or evaluate to the same value.
| |||