In theoretical computer science and mathematical logic, specifically in realizability, a partial combinatory algebra (pca) is an algebraic structure which abstracts a model of computation. The definition of pcas uses an idea from combinatory logic. The realizability topos over a pca is a model of higher-order intuitionistic logic where informally every function is computable in the model of computation specified by the pca.
Definition.
A "partial applicative structure" is simply a set formula_1 equipped with a partial binary operation formula_2 called "application". In the context of realizability, this operation is usually denoted by simple juxtaposition, i.e., formula_3. It is usually "not" associative; by convention, the notation formula_4 associates to the left as formula_5, matching the standard convention in λ-calculus.
The "terms" (or "expressions") over a partial applicative structure formula_1 are defined inductively:
A term is "closed" when it contains no variables. A closed term may be "evaluated" in the natural way: a constant formula_7 evaluates to itself, and if the terms formula_8 and formula_9 respectively evaluate to formula_16 and formula_17, then formula_10 evaluates to formula_19, if this is defined. Note that the evaluation is a partial operation, since not all applications are defined. We write formula_20 to simultaneously express that the term formula_21 evaluates to a defined value and denote this value (this matches standard notation for values of partial functions). We also write formula_22 when both closed terms formula_21 and formula_24 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 formula_21 is a term, formula_26 is a variable and formula_24 is another term, formula_28 denotes the term formula_21 with all occurrences of formula_26 replaced by formula_24.
The partial applicative structure "A" is said to be "combinatory complete" or "functionally complete" if, for every term formula_32 (that is, a term formula_21 whose variables are among formula_34), there exists an element formula_7 such that:
A partial combinatory algebra (pca) is a combinatory 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.
Characterization by combinators.
In the same way as there is a translation from λ-terms to terms of the SKI combinator calculus by eliminating λ-abstractions using combinators, pcas can be characterized by the existence of elements which satisfy equations analogous to the S and K combinators. Note, however, that some care must be taken in the statement and proof since application is not always defined in a pca.
Theorem: A partial applicative structure formula_1 is combinatory complete if and only if there exist two elements formula_41 such that:
For the proof, in the forward direction, if formula_1 is combinatory complete, it suffices to apply the definition of combinatory completeness to the terms formula_49 and formula_50 to obtain formula_51 and formula_52 with the required properties.
It is the converse that involves abstraction elimination. Assume we have formula_51 and formula_52 as stated. Given a variable formula_26 and a term formula_21, we define a term formula_57 whose variables are those of formula_21 minus formula_26, which plays a role similar to formula_60 in λ-calculus. The definition is by induction on formula_21 as follows:
Beware that the analogy between formula_57 and formula_60 is not perfect. For example, the terms formula_72 and formula_73 are not generally equivalent in a reasonable sense, e.g., taking a variable formula_67 different from formula_26 and formula_76 constants, we have formula_77, which cannot be considered equivalent to formula_67 because the latter always evaluates to formula_79 if formula_67 is replaced by a constant formula_81, while the former may not as formula_82 may be undefined.
However, if formula_83 is a constant formula_84, then formula_85 is indeed equivalent to formula_86 in the sense that substituting all variables for some constants in these two terms gives the same result (per formula_87).
Moreover, substituting variables by constants in formula_57 "always" evaluates to a defined result, even if this would not be the case by substituting variables in formula_21. For example, if formula_76 are two constants, the term formula_91 (abstracting a variable which does not appear) is equal to formula_92. By the assumptions on formula_51 and formula_52, this is well-defined, even though formula_82 may not be well-defined.
These remarks imply that for all term formula_32, the value formula_97 is well-defined and satisfies the two requirements of combinatory completeness.
Examples.
First Kleene algebra.
The first Kleene algebra formula_98 consists of the set formula_99 with application formula_100, where formula_101 denotes the formula_84-th partial recursive function in a standard Gödel numbering.
This pca can also be relativized to an oracle formula_103: we define a pca formula_104 with carrier formula_99 by setting formula_106, where formula_107 is the formula_84-th partial recursive function with oracle formula_109.
Untyped λ-calculus.
We can form a pca (in fact a tca) by quotienting the set of closed (untyped) λ-terms by β-equivalence and taking the application to be the one inherited from λ-calculus.