# 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 a program in the pca's model of computation.

## Definition

A partial applicative structure is simply a set $A$ equipped with a partial binary operation $A\times A\rightharpoonup A$ called application. In the context of realizability, this operation is usually denoted by simple juxtaposition, i.e., $(a,b)\mapsto ab$. It is usually not associative; by convention, the notation $abc$ associates to the left as $(ab)c$, matching the standard convention in λ-calculus.$^{:1}$
The terms (or expressions) over a partial applicative structure $A$ are defined inductively:$^{:2}$$^{:27}$
* A constant $a\in A$ is an expression,
* A variable, from some fixed, countably infinite set of variables, is an expression,
* If $e_{1}$ and $e_{2}$ are expressions, then $e_{1}e_{2}$ is an expression.
(In other words, they form the free magma over the disjoint union $A+V$ where $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 $a\in A$ evaluates to itself, and if the terms $e_{1}$ and $e_{2}$ respectively evaluate to $a_{1}$ and $a_{2}$, then $e_{1}e_{2}$ evaluates to $a_{1}a_{2}$, if this is defined. Note that the evaluation is a partial operation, since not all applications are defined. We write $t\downarrow$ to simultaneously express that the term $t$ evaluates to a defined value and denote this value (this matches standard notation for values of partial functions). We also write $t\simeq u$ when both closed terms $t$ and $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 $t$ is a term, $x$ is a variable and $u$ is another term, $t[u/x]$ denotes the term $t$ with all occurrences of $x$ replaced by $u$.
The partial applicative structure A is said to be combinatory complete or functionally complete if, for every term $t(x_{0},\dots ,x_{n})$ (that is, a term $t$ whose variables are among $x_{0},\dots ,x_{n}$), there exists an element $a\in A$ such that:$^{:27}$$^{:3}$
* $aa_{0}\dots a_{n-1}\downarrow$ for all $a_{0},\dots ,a_{n-1}\in A$,
* $aa_{0}\dots a_{n}\simeq t[a_{0}/x_{0},\dots ,a_{n}/x_{n}]$ for all $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:$^{:28}$$^{:3}$ A partial applicative structure $A$ is combinatory complete if and only if there exist two elements $k,s\in A$ such that:
* $Kxy\downarrow =x$ for all $x,y\in A$,
* $Sxy\downarrow$ for all $x,y\in A$,
* $Sxyz\simeq (xz)(yz)$ for all $x,y,z\in A$.
For the proof, in the forward direction, if $A$ is combinatory complete, it suffices to apply the definition of combinatory completeness to the terms $t_{K}(x,y):=x$ and $t_{S}(x,y,z):=(xz)(yz)$ to obtain $K$ and $S$ with the required properties.
It is the converse that involves abstraction elimination. Assume we have $K$ and $S$ as stated. Given a variable $x$ and a term $t$, we define a term $\langle x\rangle t$ whose variables are those of $t$ minus $x$, which plays a role similar to $\lambda x\cdot t$ in λ-calculus. The definition is by induction on $t$ as follows:$^{:3}$$^{:28}$
* $\langle x\rangle a=Ka$ for a constant $a\in A$,
* $\langle x\rangle x=I$ where $I:=SKK$,
* $\langle x\rangle y=Ky$ if $y$ is a variable different from $x$,
* $\langle x\rangle (uv)=S(\langle x\rangle u)(\langle x\rangle v)$.
Beware that the analogy between $\langle x\rangle t$ and $\lambda x\cdot t$ is not perfect. For example, the terms $(\langle x\rangle t)t'$ and $t[t'/x]$ are not generally equivalent in a reasonable sense, e.g., taking a variable $y$ different from $x$ and $a,b\in A$ constants, we have $(\langle x\rangle y)(ab)=Ky(ab)$, which cannot be considered equivalent to $y$ because the latter always evaluates to $c$ if $y$ is replaced by a constant $c\in A$, while the former may not as $ab$ may be undefined.$^{:4–5}$
However, if $t'$ is a constant $a$, then $(\langle x\rangle t)a$ is indeed equivalent to $t[a/x]$ in the sense that substituting all variables for some constants in these two terms gives the same result (per $\simeq$).$^{:4}$
Moreover, substituting variables by constants in $\langle x\rangle t$ always evaluates to a defined result, even if this would not be the case by substituting variables in $t$. For example, if $a,b\in A$ are two constants, the term $\langle x\rangle (ab)$ (abstracting a variable which does not appear) is equal to $S(Ka)(Kb)$. By the assumptions on $K$ and $S$, this is well-defined, even though $ab$ may not be well-defined.$^{:4}$
These remarks imply that for all term $t(x_{0},\dots ,x_{n})$, the value $a:=\langle x_{0}\rangle \dots \langle x_{n}\rangle t\downarrow$ is well-defined and satisfies the two requirements of combinatory completeness.$^{:4}$

## Examples
### First Kleene algebra

The first Kleene algebra ${\mathcal {K}}_{1}$ consists of the set $\mathbb {N}$ with application $ab:=\phi _{a}(b)$, where $\phi _{a}$ denotes the $a$-th partial recursive function in a standard Gödel numbering.$^{:15}$$^{:29}$
This pca can also be relativized to an oracle $D\subseteq \mathbb {N}$: we define a pca ${\mathcal {K}}_{1}^{D}$ with carrier $\mathbb {N}$ by setting $ab:=\phi _{a}^{D}(b)$, where $\phi _{a}^{D}$ is the $a$-th partial recursive function with oracle $D$.$^{:15}$$^{: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.$^{:23}$$^{:30}$