Partial combinatory algebra: Difference between revisions

Revision as of 18:04, 25 February 2025

Revision as of 18:06, 25 February 2025

Line 8:

* A constant <math>a \in A</math> is an expression,

* A variable, from some fixed, countably infinite set of variables <math>V</math>, is an expression,

* 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> where <math>V</math> is the set of varaibles.)

A term is ''closed'' ifwhen 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> and <math>u</math> either do not evaluate to a defined value, or evaluate to the same value.

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

The partial applicative structure ''A'' is said to be ''combinatory complete'' or ''functionally complete'' if, for every term <math>t(x_0, \dots, x_n)</math> (that is, a term <math>t</math> whose variables are among <math>x_0, \dots, x_n</math>), there exists an element <math>a \in A</math> such that: