UNIFYING TYPED AND UNTYPED REALIZABILITY
========================================
John Longley, May 1999
1. Introduction
---------------
In the recent paper "Matching typed and untyped realizability",
I tried to relate realizability over typed structures
(in particular the term models for various programming languages)
to the more familiar notion of realizability over untyped structures (PCAs),
via a condition called (constructive) LOGICAL FULL ABSTRACTION (LFA). E.g.
Plotkin's T^omega_re is LFA for PCF++
van Oosten's BB_re is LFA for PCF+catch (or for mu-PCF, or for
quite a big non-functional fragment of ML.)
Kleene's K_1 is LFA for PCF+quote.
Kleene's K_2re is LFA for PCF+"timeout"
The picture I had in the paper is of a typed world and an untyped world
which "touch" at various points. However, as I now realize, it's really
quite easy to define a big category that subsumes both these worlds,
and in this (2-)category, one often finds that a known programming language
is *equivalent* to a known PCA. This notion of APPLICATIVE EQUIVALENCE
is much stronger than LFA, and implies (for instance) that the two
structures in question yield the same realizability model. Of the four
examples above, at least the first three give examples of applicative
equivalence (see below).
The big category in question is an easy generalization of the 2-category
of PCAs and applicative morphisms (as in my thesis) to accommodate "typed"
structures; it seems to be a natural setting for developing all the parts
of the standard theory of realizability models that don't specifically
exploit the untypedness of the PCA. Other people have also thought about
typed realizability (e.g. Abramsky; Birkedal et al), so my ideas must be
related to theirs, but I don't think they're identical.
The objects of my 2-category are PARTIAL COMBINATORY TYPE STRUCTURES (PCTSs).
From any PCTS one can build a realizability category which is at least
locally cartesian-closed and exact (indeed, it seems that one can
characterize exactly those categories that arise in this way).
In the special case of PCAs, this category is the standard realizability topos.
APPLICATIVE MORPHISMS between PCTSs induce certain functors between the
realizability categories, and (hence) applicatively equivalent PCTSs
yield equivalent categories. The interesting thing is that quite often a
syntactically constructed programming language can be equivalent to a
nice mathematically constructed PCA, which means in effect that they are
the same thing from the point of view of realizability/computability.
This all seems to fit well with the general philosophy that "realizability
models embody notions of computability".
Realizability over partial combinatory type structures
------------------------------------------------------
Definition 1: A TYPE WORLD is any non-empty set T of (names for) *types*,
equipped with binary operations x and -> for forming product and arrow types.
(There is no requirement that T be freely generated in any sense.)
Definition 2: A PARTIAL COMBINATORY TYPE STRUCTURE (or PCTS) over a
type world T is just a family of non-empty sets
(A_t | t \in T)
together with partial "application" functions
\cdot_{tu}: A_{t->u} \times A_t \arrow A_u
such that for all types t,u,v there exist elements
k_{tu} \in A_{t->u->t}
s_{tuv} \in A_{(t->u->v)->(t->u)->(t->v),
pair_{tu} \in A_{t->u->txu},
fst_{tu} \in A_{txu->t},
snd_{tu} \in A_{txu->u}
satisfying the following for all appropriately typed a,b,c
(we suppress mention of the application functions).
kab = a
sabc >= (ac)(bc) (i.e. if (ac)(bc) is defined, so is sabc
and they're equal)
fst(pair a b) = a
snd(pair a b)=b.
(Note: we don't require EXTENSIONALITY or anything like it.)
For some purposes one doesn't even need the product types, but if one is
looking for a good mathematical theory they're a very worthwhile investment,
as we shall see below.
We have two main classes of motivating examples for the above definition:
Example 1: Let 1 be the singleton type world {*} (with *->* = *x* = *).
Then PCTSs over 1 are just PCAs in the usual sense (with a mild relaxation
of the usual condition for s.) Note that in this special case it doesn't
matter whether we include the product types in the definition or not,
since pair,fst,snd are definable from k,s.
Example 2: Let LL be any reasonable typed programming language with
product and arrow types. Then the closed term model for LL (modulo
any reasonable equivalence relation containing at least computational
equality) is a PCTS. (Note that for call-by-value languages we need to
take just the *terminating* closed terms of LL.)
Definition 3: Given a PCTS A over T, we may define the category of ASSEMBLIES
over A as follows (this is a simple typed version of the usual definition).
An assembly X consists of
a type t(X) \in T,
an underlying set |X|,
for each x \in |X|, a non-empty set ||x|| \subseteq A_{t(X)}
of REALIZERS for x.
An assembly X is a MODEST SET if for all x,y \in |X| and a \in A_{t(X)},
a \in ||x|| and a \in ||y|| implies x=y.
A morphism of assemblies f : X -> Y is a function f : |X| -> |Y|
such that there exists r \in A{t(X)->t(Y)} which tracks f in the usual way:
a \in ||x|| implies ra \in ||f(x)||.
Assemblies and their morphisms always form a category; we write it as
Ass(A), and write Mod(A) for the full subcategory of modest sets.
Theorem 1:
(i) Ass(A) is cartesian-closed
(ii) Ass(A) is regular, and is equipped with exact faithful functors
\Gamma: Ass(A) -> Set and \nabla: Set -> Ass(A)
such that \Gamma is left adjoint to \nabla and \Gamma\nabla \iso id.
(Note: Part (ii) says that Ass(A) is a \Gamma\nabla-category
in the sense of my thesis, Section 1.4.)
Interestingly, these conditions completely characterize categories of the
form Ass(A):
Theorem 2: Every cartesian-closed \Gamma\nabla category (with \Gamma faithful)
is equivalent to the category of assemblies over some PCTS.
Sketch of proof: One can exhibit any such category \CC as a "category of
assemblies over itself" in a rather trivial way. More precisely, the
image of \CC under \Gamma gives us a PCTS A, and we can show \CC \equiv Ass(A)
essentially by showing that \CC already contains all the required subquotients.
Remarks:
1. It is easy to see concretely that Ass(A) is always locally cartesian-closed
(or abstractly that any CC \Gamma\nabla-category is).
2. In my thesis, I prove that (in the case of realizability over PCAs),
the category Ass(A) is the free \Gamma\nabla-category over Mod(A)
in a certain sense. Presumably this result holds in the present
more general setting.
3. One can also define the REALIZABILITY CATEGORY RC(A) to be the
exact completion of the regular category Ass(A).
In the untyped case, RC(A) is just the standard realizability topos
over the PCA A. I expect one could also give a reasonable abstract
characterization of categories of the form RC(A).
Note that even when RC(A) is not a topos, the categories RC(A), Ass(A), Mod(A)
all have enough structure to allow us to interpret first-order logic.
(Actually, we don't yet have disjunction since RC(A) doesn't automatically
have binary coproducts. But under a mild extra condition that we can
"simulate" the booleans within A, we do.)
In the case of term models for typed programming languages, the
interpretation of first-order logic in these categories is exactly the
TYPED REALIZABILITY interpretation discussed in my paper.
Applicative morphisms between PCTSs
-----------------------------------
In my thesis I introduced and studied the notion of APPLICATIVE MORPHISM
between PCAs, and the corresponding functors between realizability categories.
We now see that all this theory lifts in a straightforward way to the
typed setting.
Definition 4: Let A be a PCTS over T, and B a PCTS over U.
(i) An APPLICATIVE MORPHISM (f,\gamma) from A to B consists of
a function f : T -> U (no special properties required);
for each t \in T, a total relation \gamma_t from A_t to B_{ft}
such that
for all t,u \in T there is an element r \in B_{f(t->u)->f(t)->f(u)}
such that
(\gamma_{t->u}(a,a') and \gamma_t(b,b') and ab defined)
implies \gamma_u(ab,ra'b').
(ii) If (f,\gamma) and (g,\delta) are applicative morphisms A->B,
we say there is an APPLICATIVE TRANSFORMATION from f to g if
for each t \in T there exists r \in B_{f(t)->g(t)} such that
\gamma_t(a,a') implies \delta_t(a,ra').
We write \PCTS for the 2-category of PCTSs, applicative morphisms and
applicative transformations.
Example 3: Applicative morphisms between PCTSs over {*} are exactly
applicative morphisms in the original sense.
Example 4: In "The SR functionals" we define a notion of SIMULATION
between extensional partial type structures (essentially,
extensional total PCTSs over the simple types over N_\bot).
A simulation \gamma: A->B is a family of total relations
\gamma_t: A_t -> B_t such that \gamma_0 is the identity on N_\bot, and
\gamma_{t->u}(f,g) and \gamma_t(x,y) implies \gamma_u(fx,gy).
Clearly, such simulations are just a special kind of applicative morphism
between extensional PTSs.
Example 5: Likewise, in the "Matching..." paper we define a TRANSLATION \theta
between (simply-)typed programming languages \LL and \LL' to be a
family of functions \theta_\sigma from \LL-terms of type \sigma to
\LL'-terms of type \sigma that respect free variables and
commute with projections, application, and evaluation of ground type terms.
If \LL^0 /~ and \LL'^0 /~' are closed term models (viewed as PCTSs),
\theta induces an applicative morphism (f,\gamma) between them, where
f is the identity on types, and \gamma is given by all instances of
\gamma ([M],[\theta M]).
Translations are thus a special kind of morphism as in Example 4.
Exactly as in the untyped case, we have:
Theorem 5: Applicative morphisms A->B give rise (in a functorial way) to
exact functors Ass(A)->Ass(B) that commute with \Gamma and \nabla up to
natural isomorphism. Similarly, applicative transformations give rise to
natural transformations between such functors. Thus the construction
Ass(-) extends to a 2-functor from \PCTS to \Cat.
Corollary 6: If A,B are APPLICATIVELY EQUIVALENT (i.e. equivalent in \PCTS),
then the corresponding categories Ass(A), Ass(B) are equivalent.
Moreover, I believe that (as in the untyped case) *every* exact
\Gamma\nabla-functor Ass(A)->Ass(B) arises in this way from an applicative
morphism, and every natural transformation between such functors arises
from an applicative transformation.
(I haven't yet checked that all the details of the proof go through,
but there shouldn't be any problem.)
This would imply that the converse to Corollary 6 also holds.
Examples of applicative equivalences
------------------------------------
We can now revisit the examples of matching pairs of typed and untyped
realizability models in my paper, and see that in many cases we simply
have an applicative equivalence between the closed term model of the
typed programming language (modulo observational equivalence) and the
corresponding PCA. It is easy to see that this equivalence implies
LOGICAL FULL ABSTRACTION, since both PCTSs give rise to the same
category of assemblies, and both realizability interpretations are just
the interpretation of first-order logic in this category.
(In fact, logical full abstraction is weaker than applicative equivalence,
and seems to correspond something like the fact that the relevant SUB-LOGOSES
of the two categories of assemblies are equivalent...)
Example 6: PCF++ (i.e. PCF+parallel-or+exists) and T^\omega_{re}.
Let A be the closed term model for PCF++ (modulo obs.eq.),
and let B=T^\omega_{re}, considered as PCTSs.
Since T^\omega_{re} can be simulated by the PCF++ type nat->nat
(or even nat->bool), we have an applicative morphism \delta:B->A.
Moreover, since in the effective Scott model all the PCF++ types are
retracts of T^\omega_{re} (see Plotkin's T^\omega paper), we have
an applicative morphism \gamma:B->A.
The equivalence \delta\gamma ~ \id_A comes from the fact that the
required embeddings/retractions are PCF++ definable;
the equivalence \gamma\delta _ \id_B is pretty trivial.
So "realizability over PCF++" and "realizability over T^\omega_{re}"
are exactly the same thing. (In particular, RC(PCF++) is a topos!)
Example 7: PCF+H and \BB_{2re}. Exactly the same holds, because of the
universality of type 2 in the effective SR functionals (see my paper
"The Sequentially Realizable Functionals").
Example 8: What about PCF and the untyped model L_U of Streicher et al.?
Well, we can't simulate L_U within PCF in the appropriate sense, because
PCF doesn't possess a universal type (folklore; consequence of games models).
In fact, for this reason, it seems pretty clear that RC(PCF) won't be
a topos, and hence PCF can't be applicatively equivalent to any PCA.
However, the language FPC (morally, PCF with recursive types) does
contain the required universal type which allows us to simulate L_U,
and so FPC and L_U are applicatively equivalent.
(This last example shows, incidentally, that applicative equivalence
is strictly stronger than logical full abstraction.)
Now the non-functional languages:
Example 9: PCF+quote and K_1 are applicatively equivalent: no problem,
since K_1 can be appropriately simulated by the type nat.
(In fact, PCF+quote is a slightly dishonest language, since once we have
quote around, our language might as well be untyped!)
Example 10: PCF+catch and BB_re (probably the best example so far).
To simulate PCF+catch in BB_re, we use the fact that PCF+catch has
a semantics in effective sequential algorithms, and BB_re is universal
for (enough of) the effective sequential algorithms model (again see
my paper on the SR functionals).
Simulating BB_re in type nat->nat of PCF+catch is easy.
So we have applicative morphisms both ways; we want to show that these
constitute an equivalence. The interesting bit is to show that for any
type t there's a PCF+catch term
algorithm_for : t -> (nat->nat)
which extracts from any term its underlying sequential algorithm.
(This is exactly the fact that I use to show LFA in "Matching...".)
Note that PCF+catch here could be replaced by muPCF, or indeed by a
fragment of SML including (mildly constrained) uses of exceptions and
even references. (We claim that these languages are all applicatively
equivalent to one another and hence to BB_re.) Thus, realizability over
this fragment of SML yields exactly the topos RT(BB_re).
Example 11: What about PCF+timeout and K_2?
Although K_2 is logically fully abstract for PCF+timeout, and there
are applicative morphisms both ways, it seems that these do not quite
constitute an equivalence. (The reason is rather technical.)
However, we believe that by slightly modifying the definition of
PCF+timeout it should be possible to obtain an applicative equivalence,
but we have not done this yet.
Further thoughts and questions
------------------------------
We have seen that for any PCTS A we get a realizability category RC(A)
with pretty good structure. The above results also show that, even if
A isn't given as a PCA, it's quite often equivalent to one, and so
RC(A) quite often turns out to be a topos. The crucial property of A
that makes this happen appears to be the existence of some kind of
"universal" type t such that the whole of A can in some sense be
reduced to type t. This accords with the (vague) idea that the reason
we get a topos in the untyped case is because we have a small "universe"
which allows for impredicativity.
I used to suffer from a vague feeling that there was something slightly
escapist about concentrating on untyped structures (PCAs) just because
their realizability categories were mathematically so pleasant.
But the above results now seem to me to go quite a way towards vindicating
the study of realizability over untyped models of computation.
It doesn't seem too far-fetched to conjecture that RC(A) is a topos
*only if* A is equivalent to a PCA. Even if this isn't true,
it seems likely that we can somehow characterize abstractly those
realizability categories that arise from PCAs. Combining this with
Theorem 2, we would then have a categorical characterization of
standard realizability toposes - I believe this would be new??
(A related approach to this question was recently suggested
to me by Peter Lietz.)
It is also natural to look for other applicative equivalences between
typed and untyped structures. One can either ask whether there is a
PCA that is equivalent to some known typed language, or a typed language
that is equivalent to some known PCA. Even if there's no PCA equivalent
to a given language, one can still ask for a "semantic" characterization
of some equivalent PCTS. Something I'd particularly like to find (for
personal reasons) is a mathematically natural PCTS that's equivalent to
a fragment of SML with exceptions including WILDCARD exception handlers.
The research programme that's implicit here is to identify what seem to
be the "natural" notions of computability/realizability (as embodied by
PCTSs up to applicative equivalence). Of course, we also want to understand
what morphisms exist between these natural notions. It is immediate,
for example, that a translation between typed languages will induce
an applicative morphism between corresponding PCAs (if these exist).
The diagram appearing in the "Matching..." paper (Figure 1) can be seen
as a first stab at what this big picture might look like.