Partial combinatory algebra

In theoretical computer science and mathematical logic, specifically in realizability, a partial combinatory algebra 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 equipped with a partial binary operation called application. In the context of realizability, this operation is usually denoted by simple juxtaposition, i.e.,. It is usually not associative; by convention, the notation associates to the left as, matching the standard convention in λ-calculus.
The terms over a partial applicative structure are defined inductively:

A constant is an expression,
A variable, from some fixed, countably infinite set of variables, is an expression,
If and are expressions, then is an expression.

A term is closed when it contains no variables. A closed term may be evaluated in the natural way: a constant evaluates to itself, and if the terms and respectively evaluate to and, then evaluates to, if this is defined. Note that the evaluation is a partial operation, since not all applications are defined. We write to simultaneously express that the term evaluates to a defined value and denote this value. We also write when both closed terms and 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 is a term, is a variable and is another term, denotes the term with all occurrences of replaced by.
The partial applicative structure A is said to be combinatory complete or functionally complete if, for every term , there exists an element such that:

for all,
for all.

A partial combinatory algebra is a combinatory complete partial applicative structure. A total combinatory algebra 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 is combinatory complete if and only if there exist two elements such that:

for all,
for all,
for all.

For the proof, in the forward direction, if is combinatory complete, it suffices to apply the definition of combinatory completeness to the terms and to obtain and with the required properties.
It is the converse that involves abstraction elimination. Assume we have and as stated. Given a variable and a term, we define a term whose variables are those of minus, which plays a role similar to in λ-calculus. The definition is by induction on as follows:

for a constant,
where,
if is a variable different from,
.

Beware that the analogy between and is not perfect. For example, the terms and are not generally equivalent in a reasonable sense, e.g., taking a variable different from and constants, we have, which cannot be considered equivalent to because the latter always evaluates to if is replaced by a constant, while the former may not as may be undefined.
However, if is a constant, then is indeed equivalent to in the sense that substituting all variables for some constants in these two terms gives the same result.
Moreover, substituting variables by constants in always evaluates to a defined result, even if this would not be the case by substituting variables in. For example, if are two constants, the term is equal to. By the assumptions on and, this is well-defined, even though may not be well-defined.
These remarks imply that for all term, the value is well-defined and satisfies the two requirements of combinatory completeness.

Examples

First Kleene algebra

The first Kleene algebra consists of the set with application, where denotes the -th partial recursive function in a standard Gödel numbering.
This pca can also be relativized to an oracle : we define a pca with carrier by setting, where is the -th partial recursive function with oracle.

Untyped λ-calculus

We can form a pca by quotienting the set of closed λ-terms by β-equivalence and taking the application to be the one inherited from λ-calculus.