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 lambda 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) is an expression,
• If ${\displaystyle e_{1}}$  and ${\displaystyle e_{2}}$  are expressions, then ${\displaystyle e_{1}e_{2}}$  is an expression.

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 free 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.

Notes

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