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. It is often expressed as an algebraic abstraction of combinatory logic.
The following definitions are taken from Hofstra.
A partial applicative structure is a set equipped with a partial binary operation
An application of is indicated by juxtaposition: denotes if (and only if) is defined, i.e., if belongs to the domain of . Homomorphisms between partial applicative structures are defined to be total functions such that , 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 means .
If is a partial applicative structure and is the free magma on the underlying set of , then we have an evident partial function
which evaluates binary words in as elements in , whenever possible, using the partial applicative structure and induction on the structure of the word.
A partial applicative structure is a partial combinatory algebra (a PCA) if there are elements such that
A homomorphism of PCA’s is a homomorphism of the underlying partial applicative structures.
A total combinatory algebra is a PCA whose application is a total function.
Note that appropriate elements , 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 that enjoys a functional completeness property, in the following sense.
Let be a countably infinite set of “variables”, and let denote the magma freely generated from the disjoint sum . Each term , i.e., each element , has finitely many occurring inside it; these are called the free variables of , and we write for the set of free variables. If , then we can think of as giving a partially defined function in variables. That is, we may consider as a term of , and (partially) define the substitution where are elements of , by evaluating at of the composite
where and is elsewhere the identity.
Then, we say is functionally complete if every term , viewed as a partial operation on , is represented by some element in . To be precise: for each term with , there exists an element such that
For all , is defined;
For all , is defined precisely when is defined, and these two elements are equal.
For example, if , are elements which realize as a PCA, then represents the term viewed as belonging to , and represents the term viewed as belonging to .
A partial combinatory algebra is functionally complete.
The idea is to simulate -abstraction , where is a variable and is a term, by induction on . Indeed, given elements that realize as a PCA, put
One then proves equality of partial functions , by induction on .
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 , (or, for that matter, any other system of combinators that provide functional completeness).
Let us check that indeed represents the identity function . This is trivial: we have, for any , equalities between defined terms
Consider the second projection function, corresponding to . Thinking in terms of -terms, this is represented by , or . In other words, we calculate
Following the proof of functional completeness, we have
Finally, consider the classical construction of the fixed-point combinator, . We have firstly
which means
(Kleene’s first algebra.) Suppose given a coding of all partial recursive functions of the form (ranging over ) by elements of , and a coding of elements of over all by elements of . Define a partial applicative structure
where whenever the right side is defined, where is the partial recursive function and is the tuple. It may be checked that and , 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 such that and are retracts of . Then elements form a PCA, in fact a total combinatory algebra, where the applicative structure is
for some chosen retraction . 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 . By this we mean functions , , such that for all , we have . One way of doing this is to put
whereupon we may calculate
That out of the way, let be the power set of and let be a set. Put a preorder structure on as follows: given , let be the set of in such that for all in and in , is defined (that is, is applicable to ), and is an element of . We can turn this into a preorder by taking just in case is inhabited.
The preorder has finite products, finite coproducts, and is cartesian closed. In other words, the preorder is a Heyting prealgebra.
An initial object is given by the constant function taking each to the empty subset , and a terminal object is given by the constant function taking each to the full subset .
Take . For binary products, define
Notice that realizes (since ), and similarly realizes . Furthermore, suppose given , and that realizes and realizes . Then
realizes . Thus is a product in the preorder.
For binary coproducts, define
Then realizes and realizes . Furthermore, suppose realizes and realizes . Then
realizes . Indeed, we have
and similarly . In either case, we see lives in for any .
For cartesian closure, define
where is standard shorthand for “ is defined”. Then for any and , the combinator realizes , and the combinator realizes .
For any function , it is immediate that
is a functor preorder map that preserves Heyting prealgebra structure.
Furthermore, in the case of a projection map , there will be left and right adjoints to , as induced by the union and intersection maps from to .
type I computability | type II computability | |
---|---|---|
typical domain | natural numbers | Baire space of infinite sequences |
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
Last revised on December 13, 2021 at 21:41:25. See the history of this page for a list of all contributions to it.