Partial combinatory algebra: Difference between revisions

Revision as of 18:15, 20 February 2025

Revision as of 18:24, 20 February 2025

Line 3:

==Definition==

A ''partial applicative structure''{{r|van-oosten|p=1}} is simply a set <math>A</math> equipped with a [[partial function|partial]] binary operation <math>A \times A \rightharpoonup A</math>. In the context of realizability, this operation is usually denoted by simple juxtaposition, i.e., <math>(a, b) \mapsto a b</math>. It is usually ''not'' associative; by convention, the notation <math>a b c</math> associates to the left as <math>(a b) c</math>, matching the standard convention in [[lambda calculus]].

The ''terms''{{r|van-oosten|p=2}} (or ''expressions'') over a partial applicative structure <math>A</math> are defined inductively:

Line 11:

* If <math>e_1</math> and <math>e_2</math> are expressions, then <math>e_1 e_2</math> is an expression.

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.

The partial applicative structure ''A'' is said to be ''combinatorially complete''{{r|van-oosten|p=3}} or ''functionally complete'' if, for every term <math>t(x_0, \dots, x_n)</math> (that is, a term <math>t</math> whose free variables are among <math>x_0, \dots, x_n</math>), there exists an element <math>a \in A</math> such that:

* For all <math>a a_0, \dots, a_{n-1} \in Adownarrow</math>, thefor applicationall <math>a a_0, \dots, a_{n-1} \in A</math> is defined, and

* For all <math>a a_0, \dots, a_n \insimeq A</math>, the evaluation of <math>t[a_0/x_0, \dots, a_n/x_n]</math> isfor defined if and only ifall <math>a a_0, \dots, a_n</math> is\in defined, and if these are defined, they are equal as elements of <math>A</math>.

A '''partial combinatory algebra'''{{r|van-oosten|p=3}} (pca) is a combinatorially complete partial applicative structure. A '''total combinatory algebra''' (tca) is a pca whose application operation is total.

Informally, the combinatory completeness condition requires an analogue of the abstraction operation from lambda calculus to exist inside the pca.