Partial combinatory algebra

In theoretical computer science and mathematical logic, a partial combinatory algebra (pca) is an algebraic structure which can be viewed as an abstraction of a model of computation. The definition of pcas uses an idea from combinatory logic. Pcas are used to define realizability toposes.

Definition

A partial applicative structure^[1]: 1 is simply a set ${\displaystyle A}$  equipped with a partial binary operation ${\displaystyle A\times A\rightharpoonup A}$ . 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.

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

• A constant ${\displaystyle a\in A}$  is an expression,
• A variable, from some fixed, countably infinite set of variables ${\displaystyle V}$ , 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}$ .)

A term is closed if 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. 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}$ . 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}$  either do not evaluate to a defined value, or evaluate to the same value.

The partial applicative structure A is said to be combinatorially complete^[1]: 3 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:

• ${\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^[1]: 3 (pca) is a combinatorially 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 proof since application is not always defined in a pca.

Theorem:^[1]: 3 A partial applicative structure ${\displaystyle A}$  is combinatorially complete if and only if there exist two elements ${\displaystyle k,s\in A}$  such that:

• ${\displaystyle Kxy=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}$ .

Notes

1. Jaap van Oosten (2008). Realizability: an introduction to its categorical side. Elsevier Science. p. 328. ISBN 9780444515841.