# Contents

## Idea

A partial combinatory algebra is a generalization of a model of the untyped lambda calculus allowing for application to be only partially defined.

## Definition

The following definitions are taken from Hofstra.

A partial applicative structure is a set equipped with a partial binary operation

$m:A×A\to A$m \colon A \times A \to A

An application of $m$ is indicated by juxtaposition: $ab$ denotes $m\left(a,b\right)$ if (and only if) $m\left(a,b\right)$ is defined, i.e., if $\left(a,b\right)$ belongs to the domain of $m$. Homomorphisms between partial applicative structures $A,B$ are defined to be total functions $f:A\to B$ such that $f\left(ab\right)=f\left(a\right)f\left(b\right)$, meaning the right side is defined whenever the left side is. In other words, in the locally posetal bicategory of sets and relations, we have a 2-cell

$\begin{array}{ccc}A×A& \stackrel{f×f}{\to }& B×B\\ m↓& \le & ↓m\\ A& \underset{f}{\to }& B\end{array}$\array{ A \times A & \stackrel{f \times f}{\to} & B \times B \\ m \downarrow & \leq & \downarrow m \\ A & \underset{f}{\to} & B }

By convention, unbracketed juxtapositions are associated to the left, so that for example $xyz$ means $\left(xy\right)z$.

If $A$ is a partial applicative structure and $\mathrm{Magma}\left(A\right)$ is the free magma on the underlying set of $A$, then we have an evident partial function

$\alpha :\mathrm{Magma}\left(A\right)\to A$\alpha \colon \mathbf{Magma}(A) \to A

which evaluates binary words in $A$ as elements in $A$, whenever possible, using the partial applicative structure and induction on the structure of the word.

###### Definition

A partial applicative structure $A$ is a partial combinatory algebra (a PCA) if there are elements $k,s\in A$ such that

• For all $a,b\in A$, $ka$ and $kab$ are defined and $kab=a$.
• For all $a,b\in A$, $sa$ and $sab$ are defined and for all $c$, $\left(ac\right)\left(bc\right)$ is defined if and only if $sabc$ is defined, and $sabc=\left(ac\right)\left(bc\right)$.

A homomorphism of PCA’s is a homomorphism of the underlying partial applicative structures.

A total combinatory algebra is a PCA $A$ whose application $m:A×A\to A$ is a total function.

Note that appropriate elements $k$, $s$ are not considered part of the structure (to be preserved under homomorphism) – here one is interested only in the property that such elements exist. Indeed, they need not be uniquely determined within the PCA.

## Functional completeness

The definition of PCA given above is traditional but somewhat opaque at first glance. The real point of the definition is that a PCA is the same thing as a partial applicative structure $A$ that enjoys a functional completeness property, in the following sense.

Let $X$ be a countably infinite set of “variables”, and let $A\left[X\right]$ denote the magma freely generated from the disjoint sum $A+X$. Each term $t$, i.e., each element $t\in A\left[X\right]$, has finitely many ${x}_{i}\in X$ occurring inside it; these are called the free variables of $t$, and we write $\mathrm{FV}\left(t\right)$ for the set of free variables. If $\mathrm{FV}\left(t\right)\subseteq \left\{{x}_{0},{x}_{1},\dots ,{x}_{n}\right\}$, then we can think of $t$ as giving a partially defined function in $n+1$ variables. That is, we may consider $t$ as a term of $\mathrm{Magma}\left(A+\left\{{x}_{0},\dots ,{x}_{n}\right\}\right)$, and (partially) define the substitution $t\left[{a}_{0}/{x}_{0},\dots ,{a}_{n}/{x}_{n}\right]$ where ${a}_{0},\dots ,{a}_{n}$ are elements of $A$, by evaluating at $t$ of the composite

$\mathrm{Magma}\left(A+\left\{{x}_{0},\dots ,{x}_{n}\right\}\right)\stackrel{\mathrm{Magma}\left(\varphi \right)}{\to }\mathrm{Magma}\left(A\right)\stackrel{\alpha }{\to }A$\mathbf{Magma}(A + \{x_0, \ldots, x_n\}) \stackrel{\mathbf{Magma}(\phi)}{\to} \mathbf{Magma}(A) \stackrel{\alpha}{\to} A

where $\varphi \left({x}_{i}\right)={a}_{i}$ and is elsewhere the identity.

Then, we say $A$ is functionally complete if every term $t\in A\left[X\right]$, viewed as a partial operation on $A$, is represented by some element in $A$. To be precise: for each term $t$ with $\mathrm{FV}\left(t\right)\subseteq \left\{{x}_{0},\dots ,{x}_{n}\right\}$, there exists an element $a\in A$ such that

• For all ${a}_{0},\dots ,{a}_{n-1}\in A$, $a{a}_{0}\dots {a}_{n-1}$ is defined;

• For all ${a}_{0},\dots ,{a}_{n}\in A$, $t\left[{a}_{0}/{x}_{0},\dots ,{a}_{n}/{x}_{n}\right]$ is defined precisely when $a{a}_{0}\dots {a}_{n}$ is defined, and these two elements are equal.

For example, if $k$, $s$ are elements which realize $A$ as a PCA, then $k$ represents the term $t={x}_{0}$ viewed as belonging to $\mathrm{Magma}\left(A+\left\{{x}_{0},{x}_{1}\right\}\right)$, and $s$ represents the term $\left({x}_{0}{x}_{2}\right)\left({x}_{1}{x}_{2}\right)$ viewed as belonging to $\mathrm{Magma}\left(A+\left\{{x}_{0},{x}_{1},{x}_{2}\right)\right\}$.

###### Theorem

A partial combinatory algebra is functionally complete.

###### Proof

The idea is to simulate $\lambda$-abstraction $\lambda x.t$, where $x\in X$ is a variable and $t$ is a term, by induction on $t$. Indeed, given elements $k,s$ that realize $A$ as a PCA, put

$\begin{array}{cccc}\lambda x.x& ≔& skk& \\ \lambda x.t& ≔& kt& \mathrm{if}x\notin \mathrm{FV}\left(t\right)\\ \lambda x.tt\prime & ≔& s\left(\lambda x.t\right)\left(\lambda x.t\prime \right)\end{array}$\array{ \lambda x. x & \coloneqq & s k k & \\ \lambda x. t & \coloneqq & k t & if x \notin FV(t) \\ \lambda x. t t' & \coloneqq & s(\lambda x. t)(\lambda x. t') }

One then proves equality of partial functions $\left(\lambda x.t\right)\left(a\right)=t\left[a/x\right]$, by induction on $t$.

Hofstra defines a PCA to be a functionally complete partial applicative structure. This is an unbiased definition, in the sense that it does not privilege certain elements $k$, $s$ (or, for that matter, any other system of combinators that provide functional completeness).

### Examples of combinators

1. Let us check that $skk$ indeed represents the identity function $I$. This is trivial: we have, for any $a\in A$, equalities between defined terms

$skka=\left(ka\right)\left(ka\right)=a.$s k k a = (k a)(k a) = a.
2. Consider the second projection function, corresponding to ${x}_{1}\in \mathrm{Magma}\left(A+\left\{{x}_{0},{x}_{1}\right\}\right)$. Thinking in terms of $\lambda$-terms, this is represented by $\lambda x.\lambda y.y=\lambda x.skk=k\left(skk\right)$, or $kI$. In other words, we calculate

$kIab=\left(\left(kI\right)a\right)b=Ib=b.$k I a b = ((k I) a) b = I b = b.
3. Following the proof of functional completeness, we have

$\lambda x.xx=s\left(\lambda x.x\right)\left(\lambda x.x\right)=sII$\lambda x. x x = s(\lambda x. x)(\lambda x. x) = s I I
4. Finally, consider the classical construction of the fixed-point combinator, $Y=\lambda y.\left(\lambda x.y\left(xx\right)\right)\left(\lambda x.y\left(xx\right)\right)$. We have firstly

$\lambda x.y\left(xx\right)=s\left(\lambda x.y\right)\left(\lambda x.xx\right)=s\left(ky\right)\left(sII\right)$\lambda x. y(x x) = s(\lambda x. y)(\lambda x. x x) = s(k y)(s I I)

which means

$\begin{array}{ccc}Y& =& \lambda y.\left(sII\right)\left(s\left(ky\right)\left(sII\right)\right)\\ & =& s\left(\lambda y.sII\right)\left(\lambda y.s\left(ky\right)\left(sII\right)\right)\\ & =& s\left(k\left(sII\right)\right)\left(s\left(\lambda y.s\left(ky\right)\right)\left(\lambda y.sII\right)\\ & =& s\left(k\left(sII\right)\right)\left(s\left(s\left(ks\right)\left(\lambda y.ky\right)\right)\right)\left(k\left(sII\right)\right)\\ & =& s\left(k\left(sII\right)\right)\left(s\left(s\left(ks\right)\left(s\left(kk\right)I\right)\right)\right)\left(k\left(sII\right)\right)\end{array}$\array{ Y & = & \lambda y. (s I I)(s(k y)(s I I)) \\ & = & s(\lambda y. s I I)(\lambda y. s(k y)(s I I)) \\ & = & s(k (s I I))(s(\lambda y. s(k y))(\lambda y. s I I) \\ & = & s(k (s I I))(s(s (k s)(\lambda y. k y)))(k (s I I)) \\ & = & s(k (s I I))(s(s (k s)(s(k k)I)))(k (s I I)) }

## Examples of PCA’s

1. (Kleene’s first algebra.) Suppose given a coding of all partial recursive functions of the form

${ℕ}^{k}\to ℕ$\mathbb{N}^k \to \mathbb{N}

(ranging over $k=0,1,2,\dots$) by elements of $ℕ$, and a coding of elements of ${ℕ}^{k}$ over all $k$ by elements of $ℕ$. Define a partial applicative structure

$ℕ×ℕ\to ℕ$\mathbb{N} \times \mathbb{N} \to \mathbb{N}

where $pq=\left\{p\right\}\left(\left[q\right]\right)$ whenever the right side is defined, where $\left\{p\right\}$ is the ${p}^{\mathrm{th}}$ partial recursive function and $\left[q\right]$ is the ${q}^{\mathrm{th}}$ tuple. It may be checked that $k$ and $s$, defined extensionally in the obvious way, are partial recursive functions, so we get in this way a PCA.

2. Suppose we have a cartesian closed category generated by an object $X$ such that $X×X$ and ${X}^{X}$ are retracts of $X$. Then elements $1\to X$ form a PCA, in fact a total combinatory algebra, where the applicative structure is

$X×X\stackrel{r×{1}_{X}}{\to }{X}^{X}×X\stackrel{\mathrm{eval}}{\to }X$X \times X \stackrel{r \times 1_X}{\to} X^X \times X \stackrel{eval}{\to} X

for some chosen retraction $r$. In other words, models of the untyped lambda calculus give PCA’s.

## Realizability toposes

From any PCA, a corresponding “realizability tripos” can be constructed, from which, in turn, a corresponding “realizability topos” can be constructed, as outlined in the article on triposes.

A preliminary technical task is to encode pairing and unpairing functions by elements of $A$. By this we mean functions $p:A×A\to A$, $l:A\to A$, $r:A\to A$ such that for all $\left(a,a\prime \right)\in A×A$, we have $\left(a,a\prime \right)=\left(l\left(p\left(a,a\prime \right)\right),r\left(p\left(a,a\prime \right)\right)\right)$. One way of doing this is to put

• $p=\lambda x.\lambda y.\lambda z.zxy$

• $l=\lambda p.p\left(\lambda x.\lambda y.x\right)$

• $r=\lambda p.p\left(\lambda x.\lambda y.y\right)$

whereupon we may calculate

$\begin{array}{ccc}paa\prime & =& \lambda z.zaa\prime \\ l\left(paa\prime \right)& =& \left(\lambda z.zaa\prime \right)\left(\lambda x.\lambda y.x\right)\\ & =& \left(\lambda x.\lambda y.x\right)aa\prime \\ & =& \left(\lambda y.a\right)a\prime =a\end{array}$\array{ p a a' & = & \lambda z. z a a' \\ l(p a a') & = & (\lambda z. z a a')(\lambda x. \lambda y. x) \\ & = & (\lambda x. \lambda y. x) a a' \\ & = & (\lambda y. a) a' = a }
$\begin{array}{ccc}r\left(paa\prime \right)& =& \left(\lambda z.zaa\prime \right)\left(\lambda x.\lambda y.y\right)\\ & =& \left(\lambda x.\lambda y.y\right)aa\prime \\ & =& \left(\lambda y.y\right)a\prime =a\prime \end{array}$\array{ r(p a a') & = & (\lambda z. z a a')(\lambda x. \lambda y. y) \\ & = & (\lambda x. \lambda y. y) a a' \\ & = & (\lambda y. y) a' = a' }

That out of the way, let $P\left(A\right)$ be the power set of $A$ and let $X$ be a set. Put a preorder structure on $P\left(A{\right)}^{X}$ as follows: given $f,g\in P\left(A{\right)}^{X}$, let $\mathrm{Hom}\left(f,g\right)$ be the set of $a$ in $A$ such that for all $x$ in $X$ and $a\prime$ in $f\left(x\right)$, $a$ applied to $a\prime$ is defined and an element of $g\left(x\right)$. We will of course take $f\le g$ just in case $\mathrm{Hom}\left(f,g\right)$ is inhabited.

###### Theorem

The preorder $P\left(A{\right)}^{X}$ has finite products, finite coproducts, and is cartesian closed. In other words, the preorder $P\left(A{\right)}^{X}$ is a Heyting prealgebra.

###### Proof

An initial object is given by the constant function taking each $x$ to the empty subset $\varnothing \subseteq A$, and a terminal object is given by the constant function taking each $x$ to the full subset $A\subseteq A$.

Take $f,g:X\to P\left(A\right)$. For binary products, define

$\left(f\wedge g\right)\left(x\right)=\left\{paa\prime \mid a\in f\left(x\right)\wedge a\prime \in g\left(x\right)\right\}$(f \wedge g)(x) = \{p a a' | a \in f(x) \wedge a' \in g(x)\}

Notice that $l$ realizes $f\wedge g\le f$ (since $l\left(paa\prime \right)=a$), and similarly $r$ realizes $f\wedge g\le g$. Furthermore, suppose given $h:X\to P\left(A\right)$, and that $t\in A$ realizes $h\le f$ and $u\in A$ realizes $h\le g$. Then

$v=\lambda b.p\left(tb\right)\left(ub\right)$v = \lambda b. p (t b)(u b)

realizes $h\le f\wedge g$. Thus $f\wedge g$ is a product in the preorder.

For binary coproducts, define

$\left(f\vee g\right)\left(x\right)=\left\{pla\mid a\in f\left(x\right)\right\}\cup \left\{pra\prime \mid a\prime \in g\left(x\right)\right\}$(f \vee g)(x) = \{p l a | a \in f(x)\} \cup \{p r a' | a' \in g(x)\}

Then $pl$ realizes $f\le f\vee g$ and $pr$ realizes $g\le f\vee g$. Furthermore, suppose $t$ realizes $f\le h$ and $u$ realizes $g\le h$. Then

$v=\lambda b.l\left(b\right)\left(p\left(t\left(rb\right)\right)\left(u\left(rb\right)\right)\right)$v = \lambda b. l(b)(p(t(r b))(u(r b)))

realizes $f\vee g\le h$. Indeed, we have

$\begin{array}{ccc}v\left(pla\right)& =& l\left(pla\right)\left(p\left(t\left(r\left(pla\right)\right)\right)\left(u\left(r\left(pla\right)\right)\right)\right)\\ & =& l\left(p\left(ta\right)\left(ua\right)\right)\\ & =& ta\end{array}$\array{ v(p l a) & = & l(p l a)(p(t(r(p l a)))(u(r(p l a)))) \\ & = & l(p(t a)(u a)) \\ & = & t a }

and similarly $v\left(pra\prime \right)=ua\prime$. In either case, we see $v\left(b\right)$ lives in $h\left(x\right)$ for any $b\in \left(f\vee g\right)\left(x\right)$.

For cartesian closure, define

$\left(f⇒g\right)\left(x\right)=\left\{a\prime \mid \forall a\in f\left(x\right)a\prime a↓\wedge a\prime a\in g\left(x\right)\right\}$(f \Rightarrow g)(x) = \{a' | \forall a \in f(x) a' a \downarrow \wedge a' a \in g(x)\}

where $a\prime a↓$ is standard shorthand for ”$a\prime a$ is defined”. Then for any $f$ and $g$, the combinator $\lambda b.l\left(b\right)r\left(b\right)$ realizes $\left(f⇒g\right)\wedge f\le g$, and the combinator $\lambda b.\lambda a.pab$ realizes $g\le f⇒\left(f\wedge g\right)$.

For any function $f:X\to Y$, it is immediate that

$P\left(A{\right)}^{f}:P\left(A{\right)}^{Y}\to P\left(A{\right)}^{X}$P(A)^f \colon P(A)^Y \to P(A)^X

is a functor preorder map that preserves Heyting prealgebra structure.

Furthermore, in the case of a projection map $f:Z×Y\to Y$, there will be left and right adjoints to $P\left(A{\right)}^{f}:P\left(A{\right)}^{Y}\to P\left(A{\right)}^{Z×Y}\left(\cong \left(P\left(A{\right)}^{Z}{\right)}^{Y}\right)$, as induced by the union and intersection maps from $P\left(A{\right)}^{Z}$ to $P\left(A\right)$.

## References

Pieter J.W. Hofstra, Partial Combinatory Algebras and Realizability Toposes, (web) (pdf)

Revised on September 8, 2012 00:48:59 by Todd Trimble (67.81.93.25)