constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A partial combinatory algebra is a generalization of a model of the untyped lambda calculus allowing for application to be only partially defined.
The following definitions are taken from Hofstra.
A partial applicative structure is a set equipped with a partial binary operation
An application of $m$ is indicated by juxtaposition: $a b$ denotes $m(a, b)$ if (and only if) $m(a, b)$ is defined, i.e., if $(a, b)$ belongs to the domain of $m$. Homomorphisms between partial applicative structures $A, B$ are defined to be total functions $f \colon A \to B$ such that $f(a b) = f(a)f(b)$, 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
By convention, unbracketed juxtapositions are associated to the left, so that for example $x y z$ means $(x y)z$.
If $A$ is a partial applicative structure and $\mathbf{Magma}(A)$ is the free magma on the underlying set of $A$, then we have an evident partial function
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.
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$, $k a$ and $k a b$ are defined and $k a b = a$. * For all $a, b \in A$, $s a$ and $s a b$ are defined and for all $c$, $(a c)(b c)$ is defined if and only if $s a b c$ is defined, and $s a b c = (a c)(b c)$.
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 \colon A \times 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.
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[X]$ denote the magma freely generated from the disjoint sum $A + X$. Each term $t$, i.e., each element $t \in A[X]$, has finitely many $x_i \in X$ occurring inside it; these are called the free variables of $t$, and we write $FV(t)$ for the set of free variables. If $FV(t) \subseteq \{x_0, x_1, \ldots, x_n\}$, 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 $\mathbf{Magma}(A + \{x_0, \ldots, x_n\})$, and (partially) define the substitution $t[a_0/x_0, \ldots, a_n/x_n]$ where $a_0, \ldots, a_n$ are elements of $A$, by evaluating at $t$ of the composite
where $\phi(x_i) = a_i$ and is elsewhere the identity.
Then, we say $A$ is functionally complete if every term $t \in A[X]$, viewed as a partial operation on $A$, is represented by some element in $A$. To be precise: for each term $t$ with $FV(t) \subseteq \{x_0, \ldots, x_n\}$, there exists an element $a \in A$ such that
For all $a_0, \ldots, a_{n-1} \in A$, $a a_0 \ldots a_{n-1}$ is defined;
For all $a_0, \ldots, a_n \in A$, $t[a_0/x_0, \ldots, a_n/x_n]$ is defined precisely when $a a_0 \ldots 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 $\mathbf{Magma}(A + \{x_0, x_1\})$, and $s$ represents the term $(x_0 x_2)(x_1 x_2)$ viewed as belonging to $\mathbf{Magma}(A + \{x_0, x_1, x_2)\}$.
A partial combinatory algebra is functionally complete.
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
One then proves equality of partial functions $(\lambda x. t)(a) = t[a/x]$, 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).
Let us check that $s k k$ indeed represents the identity function $I$. This is trivial: we have, for any $a \in A$, equalities between defined terms
Consider the second projection function, corresponding to $x_1 \in \mathbf{Magma}(A + \{x_0, x_1\})$. Thinking in terms of $\lambda$-terms, this is represented by $\lambda x. \lambda y. y = \lambda x. s k k = k(s k k)$, or $k I$. In other words, we calculate
Following the proof of functional completeness, we have
Finally, consider the classical construction of the fixed-point combinator, $Y = \lambda y. (\lambda x. y(x x))(\lambda x. y(x x))$. We have firstly
which means
(Kleene’s first algebra.) Suppose given a coding of all partial recursive functions of the form $\mathbb{N}^k \to \mathbb{N}$ (ranging over $k = 0, 1, 2, \ldots$) by elements of $\mathbb{N}$, and a coding of elements of $\mathbb{N}^k$ over all $k$ by elements of $\mathbb{N}$. Define a partial applicative structure
where $p q = \{p\}([q])$ whenever the right side is defined, where $\{p\}$ is the $p^{th}$ partial recursive function and $[q]$ is the $q^{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.
Suppose we have a cartesian closed category generated by an object $X$ such that $X \times 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
for some chosen retraction $r$. In other words, models of the untyped lambda calculus give PCA’s.
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 \colon A \times A \to A$, $l \colon A \to A$, $r \colon A \to A$ such that for all $(a, a') \in A \times A$, we have $(a, a') = (l(p(a, a')), r(p(a, a')))$. One way of doing this is to put
$p = \lambda x. \lambda y. \lambda z. z x y$
$l = \lambda p. p(\lambda x. \lambda y. x)$
$r = \lambda p. p(\lambda x. \lambda y. y)$
whereupon we may calculate
That out of the way, let $P(A)$ be the power set of $A$ and let $X$ be a set. Put a preorder structure on $P(A)^X$ as follows: given $f, g \in P(A)^X$, let $Hom(f, g)$ be the set of $a$ in $A$ such that for all $x$ in $X$ and $a'$ in $f(x)$, $a$ applied to $a'$ is defined and an element of $g(x)$. We will of course take $f \leq g$ just in case $Hom(f, g)$ is inhabited.
The preorder $P(A)^X$ has finite products, finite coproducts, and is cartesian closed. In other words, the preorder $P(A)^X$ is a Heyting prealgebra.
An initial object is given by the constant function taking each $x$ to the empty subset $\emptyset \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 \colon X \to P(A)$. For binary products, define
Notice that $l$ realizes $f \wedge g \leq f$ (since $l (p a a') = a$), and similarly $r$ realizes $f \wedge g \leq g$. Furthermore, suppose given $h \colon X \to P(A)$, and that $t \in A$ realizes $h \leq f$ and $u \in A$ realizes $h \leq g$. Then
realizes $h \leq f \wedge g$. Thus $f \wedge g$ is a product in the preorder.
For binary coproducts, define
Then $p l$ realizes $f \leq f \vee g$ and $p r$ realizes $g \leq f \vee g$. Furthermore, suppose $t$ realizes $f \leq h$ and $u$ realizes $g \leq h$. Then
realizes $f \vee g \leq h$. Indeed, we have
and similarly $v(p r a') = u a'$. In either case, we see $v(b)$ lives in $h(x)$ for any $b \in (f \vee g)(x)$.
For cartesian closure, define
where $a' a \downarrow$ is standard shorthand for “$a' a$ is defined”. Then for any $f$ and $g$, the combinator $\lambda b. l(b)r(b)$ realizes $(f \Rightarrow g) \wedge f \leq g$, and the combinator $\lambda b. \lambda a. p a b$ realizes $g \leq f \Rightarrow (f \wedge g)$.
For any function $f \colon X \to Y$, it is immediate that
is a functor preorder map that preserves Heyting prealgebra structure.
Furthermore, in the case of a projection map $f \colon Z \times Y \to Y$, there will be left and right adjoints to $P(A)^f \colon P(A)^Y \to P(A)^{Z \times Y} (\cong (P(A)^Z)^Y)$, as induced by the union and intersection maps from $P(A)^Z$ to $P(A)$.
type I computability | type II computability | |
---|---|---|
typical domain | natural numbers $\mathbb{N}$ | Baire space of infinite sequences $\mathbb{B} = \mathbb{N}^{\mathbb{N}}$ |
computable functions | partial recursive function | computable function (analysis) |
type of computable mathematics | recursive mathematics | computable analysis, Type Two Theory of Effectivity |
type of realizability | number realizability | function realizability |
partial combinatory algebra | Kleene's first partial combinatory algebra | Kleene's second partial combinatory algebra |
Lecture notes include