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.Template:R

The terms (or expressions) over a partial applicative structure $A$ are defined inductively:Template:RTemplate:R

• 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:Template:RTemplate:R

• $a{a}_0\dots a_{n-1}\downarrow$ for all $a_0,\dots ,a_{n-1}\in A$,
• $a{a}_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:Template:RTemplate:R 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 $⟨x⟩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:Template:RTemplate:R

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

Beware that the analogy between $⟨x⟩t$ and $\lambda x\cdot t$ is not perfect. For example, the terms $(⟨x⟩t)t^{\prime }$ and $t[t^{\prime }/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 $(⟨x⟩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.Template:R

However, if $t^{\prime }$ is a constant $a$, then $(⟨x⟩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$).Template:R

Moreover, substituting variables by constants in $⟨x⟩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 $⟨x⟩(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.Template:R

These remarks imply that for all term $t(x_0,\dots ,x_n)$, the value $a:=⟨x_0⟩\dots ⟨x_n⟩t\downarrow$ is well-defined and satisfies the two requirements of combinatory completeness.Template:R

Examples

First Kleene algebra

The first Kleene algebra ${𝒦}_1$ consists of the set $\mathbb{N}$ with application $ab:={\varphi }_a(b)$, where ${\varphi }_a$ denotes the $a$-th partial recursive function in a standard Gödel numbering.Template:RTemplate:R

This pca can also be relativized to an oracle $D\subseteq \mathbb{N}$: we define a pca ${𝒦}_1^D$ with carrier $\mathbb{N}$ by setting $ab:={\varphi }_a^D(b)$, where ${\varphi }_a^D$ is the $a$-th partial recursive function with oracle $D$.Template:RTemplate:R

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.Template:RTemplate:R