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.