Partial combinatory algebra

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 ${\displaystyle A}$ equipped with a partial binary operation ${\displaystyle A\times A\rightharpoonup A}$ called application. In the context of realizability, this operation is usually denoted by simple juxtaposition, i.e., ${\displaystyle (a,b)\mapsto ab}$. It is usually not associative; by convention, the notation ${\displaystyle abc}$ associates to the left as ${\displaystyle (ab)c}$, matching the standard convention in λ-calculus.^[1]: 1

The terms (or expressions) over a partial applicative structure ${\displaystyle A}$ are defined inductively:^{[1]: 2 [2]: 27}

• A constant ${\displaystyle a\in A}$ is an expression,
• A variable, from some fixed, countably infinite set of variables, is an expression,
• If ${\displaystyle e_{1}}$ and ${\displaystyle e_{2}}$ are expressions, then ${\displaystyle e_{1}e_{2}}$ is an expression.

(In other words, they form the free magma over the disjoint union ${\displaystyle A+V}$ where ${\displaystyle V}$ is the set of variables.)

A term is closed when it contains no variables. A closed term may be evaluated in the natural way: a constant ${\displaystyle a\in A}$ evaluates to itself, and if the terms ${\displaystyle e_{1}}$ and ${\displaystyle e_{2}}$ respectively evaluate to ${\displaystyle a_{1}}$ and ${\displaystyle a_{2}}$, then ${\displaystyle e_{1}e_{2}}$ evaluates to ${\displaystyle a_{1}a_{2}}$, if this is defined. Note that the evaluation is a partial operation, since not all applications are defined. We write ${\displaystyle t\downarrow }$ to simultaneously express that the term ${\displaystyle t}$ evaluates to a defined value and denote this value (this matches standard notation for values of partial functions). We also write ${\displaystyle t\simeq u}$ when both closed terms ${\displaystyle t}$ and ${\displaystyle u}$ 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 ${\displaystyle t}$ is a term, ${\displaystyle x}$ is a variable and ${\displaystyle u}$ is another term, ${\displaystyle t[u/x]}$ denotes the term ${\displaystyle t}$ with all occurrences of ${\displaystyle x}$ replaced by ${\displaystyle u}$.

The partial applicative structure A is said to be combinatory complete or functionally complete if, for every term ${\displaystyle t(x_{0},\dots ,x_{n})}$ (that is, a term ${\displaystyle t}$ whose variables are among ${\displaystyle x_{0},\dots ,x_{n}}$), there exists an element ${\displaystyle a\in A}$ such that:^{[2]: 27 [1]: 3}

• ${\displaystyle aa_{0}\dots a_{n-1}\downarrow }$ for all ${\displaystyle a_{0},\dots ,a_{n-1}\in A}$,
• ${\displaystyle aa_{0}\dots a_{n}\simeq t[a_{0}/x_{0},\dots ,a_{n}/x_{n}]}$ for all ${\displaystyle a_{0},\dots ,a_{n}\in A}$.

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:^{[2]: 28 [1]: 3} A partial applicative structure ${\displaystyle A}$ is combinatory complete if and only if there exist two elements ${\displaystyle k,s\in A}$ such that:

• ${\displaystyle Kxy\downarrow =x}$ for all ${\displaystyle x,y\in A}$,
• ${\displaystyle Sxy\downarrow }$ for all ${\displaystyle x,y\in A}$,
• ${\displaystyle Sxyz\simeq (xz)(yz)}$ for all ${\displaystyle x,y,z\in A}$.

For the proof, in the forward direction, if ${\displaystyle A}$ is combinatory complete, it suffices to apply the definition of combinatory completeness to the terms ${\displaystyle t_{K}(x,y):=x}$ and ${\displaystyle t_{S}(x,y,z):=(xz)(yz)}$ to obtain ${\displaystyle K}$ and ${\displaystyle S}$ with the required properties.

It is the converse that involves abstraction elimination. Assume we have ${\displaystyle K}$ and ${\displaystyle S}$ as stated. Given a variable ${\displaystyle x}$ and a term ${\displaystyle t}$, we define a term ${\displaystyle \langle x\rangle t}$ whose variables are those of ${\displaystyle t}$ minus ${\displaystyle x}$, which plays a role similar to ${\displaystyle \lambda x\cdot t}$ in λ-calculus. The definition is by induction on ${\displaystyle t}$ as follows:^{[1]: 3 [2]: 28}

• ${\displaystyle \langle x\rangle a=Ka}$ for a constant ${\displaystyle a\in A}$,
• ${\displaystyle \langle x\rangle x=I}$ where ${\displaystyle I:=SKK}$,
• ${\displaystyle \langle x\rangle y=Ky}$ if ${\displaystyle y}$ is a variable different from ${\displaystyle x}$,
• ${\displaystyle \langle x\rangle (uv)=S(\langle x\rangle u)(\langle x\rangle v)}$.

Beware that the analogy between ${\displaystyle \langle x\rangle t}$ and ${\displaystyle \lambda x\cdot t}$ is not perfect. For example, the terms ${\displaystyle (\langle x\rangle t)t'}$ and ${\displaystyle t[t'/x]}$ are not generally equivalent in a reasonable sense, e.g., taking a variable ${\displaystyle y}$ different from ${\displaystyle x}$ and ${\displaystyle a,b\in A}$ constants, we have ${\displaystyle (\langle x\rangle y)(ab)=Ky(ab)}$, which cannot be considered equivalent to ${\displaystyle y}$ because the latter always evaluates to ${\displaystyle c}$ if ${\displaystyle y}$ is replaced by a constant ${\displaystyle c\in A}$, while the former may not as ${\displaystyle ab}$ may be undefined.^[1]: 4–5

However, if ${\displaystyle t'}$ is a constant ${\displaystyle a}$, then ${\displaystyle (\langle x\rangle t)a}$ is indeed equivalent to ${\displaystyle t[a/x]}$ in the sense that substituting all variables for some constants in these two terms gives the same result (per ${\displaystyle \simeq }$).^[1]: 4

Moreover, substituting variables by constants in ${\displaystyle \langle x\rangle t}$ always evaluates to a defined result, even if this would not be the case by substituting variables in ${\displaystyle t}$. For example, if ${\displaystyle a,b\in A}$ are two constants, the term ${\displaystyle \langle x\rangle (ab)}$ (abstracting a variable which does not appear) is equal to ${\displaystyle S(Ka)(Kb)}$. By the assumptions on ${\displaystyle K}$ and ${\displaystyle S}$, this is well-defined, even though ${\displaystyle ab}$ may not be well-defined.^[1]: 4

These remarks imply that for all term ${\displaystyle t(x_{0},\dots ,x_{n})}$, the value ${\displaystyle a:=\langle x_{0}\rangle \dots \langle x_{n}\rangle t\downarrow }$ is well-defined and satisfies the two requirements of combinatory completeness.^[1]: 4

Examples

First Kleene algebra

The first Kleene algebra ${\displaystyle {\mathcal {K}}_{1}}$ consists of the set ${\displaystyle \mathbb {N} }$ with application ${\displaystyle ab:=\phi _{a}(b)}$, where ${\displaystyle \phi _{a}}$ denotes the ${\displaystyle a}$-th partial recursive function in a standard Gödel numbering.^{[1]: 15 [2]: 29}

This pca can also be relativized to an oracle ${\displaystyle D\subseteq \mathbb {N} }$: we define a pca ${\displaystyle {\mathcal {K}}_{1}^{D}}$ with carrier ${\displaystyle \mathbb {N} }$ by setting ${\displaystyle ab:=\phi _{a}^{D}(b)}$, where ${\displaystyle \phi _{a}^{D}}$ is the ${\displaystyle a}$-th partial recursive function with oracle ${\displaystyle D}$.^{[1]: 15 [2]: 30}

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.^{[1]: 23 [2]: 30}

Reflexive domains

Second Kleene algebra

References

1. Jaap van Oosten (2008). Realizability: an introduction to its categorical side. Elsevier Science. p. 328. ISBN 9780444515841.
2. Andrej Bauer (2025-02-21). "Notes on realizability" (PDF). GitHub. Retrieved 2025-02-21.