The abstracts below have simply been copied from the papers as they were written at the time.
|
PDF (227 kb) DVI (61 kb) PostScript (compressed) (78 kb) A5 PS booklet (compressed) (71 kb) What are these? [12 Feb 2009] | Appendix A of Proofs and Types, partly based on a chapter of the original notes; written April 1988. The semantics is in terms of coherence spaces, and has a "uniformity" property over all types. We attempt to calculate ΠX.X, ΠX. X- > X, ΠX. X- > X- > X and ΠX. X- > (X- > X) - > X. |
|
PDF (311 kb) DVI (104 kb) PostScript (compressed) (114 kb) A5 PS booklet (compressed) (105 kb) What are these? [12 Feb 2009] | Written January-March 1988. Published in the Journal of Pure and Applied Algebra, 64 (1990) 171-203. Day [75] showed that the category of continuous lattices and maps which preserve directed joins and arbitrary meets is the category of algebras for a monad over Set, Sp or Pos, the free functor being the set of filters of open sets. Separately, Berry [78] constructed a cartesian closed category whose morphisms preserve directed joins and connected meets, whilst Diers [79] considered similar functors independently in a study of categories of models of disjunctive theories. Girard [85] built on Berry's work to build a new and very lean model of polymorphism. In this paper we bring these strands together, defining a monad based on filters of connected open sets and showing that its category of algebras has Berry's (stable) morphisms and is cartesian closed. The objects have multijoins as in Diers' work, and the slices are continuous lattices. The monad can only be defined for locally connected spaces, so via [Barr-Paré 80] there is a further (unexplained) connection with cartesian closure. Jung [87] has shown that the same objects (L-domains) also form a cartesian closed category with maps preserving only directed joins. Berry's proof of cartesian closure (using the trace factorisation, which also occurs in Diers' work and is discussed in [Taylor 88]) and more direct proofs by Coquand [88] and Lamarche [88] use two additional hypotheses, strong finiteness and distributivity (of finite meets over finite joins). Our proof is the first to use neither of these, but it does use distributivity of codirected meets over directed joins, which [Taylor 88] shows not to be needed either. Lamarche has shown that evaluation does not preserve equalisers, so in the categorical context connected limits must be replaced by wide pullbacks. He has also found a generalised notion of neighbourhood system which unifies stable and continuous functions and generalises our ad hoc notion of Berry order between continuous functions. |
|
PDF (360 kb) DVI (140 kb) PostScript (compressed) (142 kb) A5 PS booklet (compressed) (131 kb) What are these? [12 Feb 2009] | Written January-June 1989. Presented at Category Theory and Computer Science 3 (Manchester) ed. David Pitt, Springer Lecture Notes in Computer Science 389 (1989) 155-181. We introduce the notion of a candidate for "multiple valued universal constructions" and define stable functors (which generalise functors with left adjoints) in terms of factorisation through candidates. There are many mathematical examples, including the Zariski spectrum of a ring (as shown by Diers [81]) and the Galois group of a polynomial, but we are mainly interested in Berry's [78] minimum data property. In fact we begin with a completely non-mathematical example. The aim is to find domain models in which terms of the typed or polymorphic λ-calculus are interpreted as stable functors. We study Girard's quantitative domains [85], in which information is represented by a collection of tokens from a universe of tokens for a particular type, and there is no restriction on the ability of different tokens to co-exist or on the number of occurrences of a particular token. This idea may be used to code parallelism (with no suppression of duplicated output) or accounted resources. Unfortunately Girard did not fully describe the function-spaces, which should be equipped with the Berry order; this turns out to mean that function-tokens must have "internal symmetries". It is our purpose to describe the smallest cartesian closed category with these function-spaces which contains Set (the simplest non-trivial quantitative domain, with one token which may appear arbitrarily often) as an object. The natural way of presenting this is as a new interpretation of Linear Logic given by group (and more generally groupoid) actions. These stand in the same relation to quantitative domains as coherence spaces do to qualitative domains, and there is a kind of coherence between group(oid) elements. By a similar analysis of stable functors we obtain an of course operation. Finally, our (generalised) quantitative domains themselves form a domain of this kind with rigid comparisons as morphisms, and hence we have a type of types. |
|
PDF (363 kb) DVI (182 kb) PostScript (compressed) (153 kb) A5 PS booklet (compressed) (142 kb) What are these? [12 Feb 2009] | Written July-November 1988. A functor is stable if it has a left adjoint on each slice. Such functors arise as forgetful functors from categories of models of disjunctive theories. A stable functor factorises as a functor with a (global) left adjoint followed by a fibration of groupoids; Diers [D79] showed that in many cases the corresponding indexation is a well-known spectrum. Independently, Berry [B78,B79] constructed a cartesian closed category of posets and stable functors, which Girard [G85] developed into a model of polymorphism; the proof of cartesian closure implicitly makes use of this factorisation. Girard [G81] had earlier developed a technique in proof theory involving dilators (stable endofunctors of the category of ordinals), also using the factorisation. Although Diers [D81] knew of the existence of this factorisation system, his work used an additional assumption of preserving equalisers. However Lamarche [L88] observed that examples such as algebraically closed fields can be incorporated if this assumption is dropped, and also that (in the the search for cartesian closed categories) evaluation does not preserve equalisers. We find that Diers' definitions can be modified in a simple and elegant way which also throws light on the General Adjoint Functor Theorem and on factorisation systems. In this paper the factorisation system is constructed in detail and related back to Girard's examples; following him we call the intermediate category the trace. We also consider natural and cartesian transformations between stable functors. We find that the latter (which must be the morphisms of the "stable functor category") have a simple connection with the factorisation, and induce a rigid adjunction (whose unit and counit are cartesian) between traces. |
|
PDF (277 kb) DVI (146 kb) PostScript (compressed) (123 kb) A5 PS booklet (compressed) (116 kb) What are these? [12 Feb 2009] | Written July-November 1988 |
|
PDF (295 kb) DVI (115 kb) PostScript (compressed) (110 kb) A5 PS booklet (compressed) (102 kb) What are these? [12 Feb 2009] | Written October-December 1989 Gabriel-Ulmer duality relates locally finitely presentable and left exact categories. Diers generalised this by making the colimits in LFP categories "mutilple-valued", but retained functors with left adjoints as the 1-cells and natural transformations as the 2-cells in the duality. But Berry showed (in a very special case) that using functors which have left adjoints only on each slice and cartesian transformations we obtain a cartesian-closed 2-category. Our goal is to prove duality [and cartesian closure] in the most general case. However Lamarche has shown that, for the latter, multiple colimits must be generalised further to allow them to have automorphisms; the category of algebraically closed fields is now an example. We use the results of a previous paper, where it was shown that functors with adjoints on each slice admit a factorisation, known to Berry as the trace and to Diers as a spectrum. |
This is www.PaulTaylor.EU/stable/index.php and it was derived from stable/index.tex which was last modified on 2 June 2007.