Applications of Categories in Computer Science: Proceedings of the London Mathematical Society Symposium, Durham 1991 (London Mathematical Society Lecture Note Series, Series Number 177)

Applications of category theory and related topics of mathematics to computer science have been a growing area in recent years. This book contains selected papers on the subject from the London Mathematical Society Symposium held at the University of Durham in July 1991. Cover......Page 1 Title Page......Page 5 Contents......Page 7 Preface......Page 9 Computational Comonads and Intensional Semantics......Page 13 1 Introduction......Page 14 2.1 Comonads and the Kleisli category......Page 16 3 Notions of computation on domains......Page 18 3.1 Increasing paths......Page 19 3.2 Strictly increasing paths......Page 24 3.3 Timed data......Page 25 4.1 Computational comonads......Page 27 4.2 Examples......Page 32 5.1 Products......Page 35 5.2 Exponentiation......Page 37 5.3 Examples......Page 40 5.4 Pairing, currying and uncurrying on algorithms......Page 41 5.5 Examples......Page 45 6 Ordered categories......Page 46 7.2 Strict algorithms......Page 50 7.3 Computation on effectively given domains......Page 51 7.4 Computation on pre-domains......Page 52 8 Conclusions......Page 53 References......Page 55 0. Introduction......Page 57 1. Polycategories......Page 59 2.1. Definition......Page 64 2.2. Weakly distributive categories and polycategories......Page 66 3. Distributive categories......Page 67 4. Adding negation......Page 71 5. Some posetal examples......Page 75 References......Page 77 1 Introduction......Page 78 2 Syntactic sequentiality......Page 79 3 Full abstraction for PCF and related languages......Page 85 4 Sequential algorithms on concrete data structures......Page 95 5 One, two, hundred errors......Page 100 References......Page 104 Remarks on Algebraically Compact Categories......Page 107 1: On some examples......Page 108 2: On CPO-categories......Page 109 4: On the Product Theorems......Page 112 5: On Dinaturality......Page 115 6: On Multi-Coreflectivity......Page 116 7: On Relation Categories......Page 117 Dinaturality for free......Page 119 1. The problem......Page 120 2. Some properties of an internal functor......Page 121 3. When the hexagon commutes......Page 124 4. The algebraic case......Page 126 References......Page 129 1. Introduction......Page 131 2. Preliminaries......Page 133 3. Simply typed λ-calculus......Page 136 4. The untyped λ-calculus......Page 145 References......Page 153 1. Introduction......Page 155 2. Confluent Categories......Page 158 3. Confluent Adjunctions......Page 161 4.2. Contexts and Declarations......Page 164 5.1. The Reduction System......Page 168 5.2. A Substitution Model......Page 170 5.3. A Declaration Model......Page 171 6. Further Work......Page 172 References......Page 173 1. Introduction......Page 175 2. The original club idea......Page 176 3. The abstract notion of club......Page 182 4. The enriched case......Page 188 5. The original clubs are clubs in the abstract sense; other examples and counter-examples......Page 194 References......Page 200 1. A finite presentation......Page 203 2. A complete rewrite system......Page 205 3. Carrying on......Page 206 References......Page 207 Appendix: Confluence of the fifty-six critical pairs......Page 211 1. Introduction......Page 214 2. Strong dinaturality and fix......Page 215 3. Algebraically strong dinaturality and FIX......Page 220 References......Page 228 1 Introduction......Page 229 2 Possible Worlds......Page 230 3 Procedures......Page 235 4 States and Contravariance......Page 237 5 Generalized Variables......Page 239 6 Non-interference......Page 242 7 Discussion......Page 247 Acknowledgements......Page 248 References......Page 249 1.1. What this paper is about......Page 251 1.2. Fibrations and polymorphic λ-calculus......Page 254 2.1. Rules for subtypes and bounded quantification......Page 256 2.2. Characterising inclusions......Page 258 2.3. Incorporating bounded quantification......Page 260 2.4. Incorporating subkinds......Page 261 3.1. PER models......Page 263 3.2. Models arising from PER models......Page 265 3.3. Subtypes and constructions on types......Page 266 References......Page 267 2. Sequential PCF......Page 270 3. Logical Relations......Page 273 4. A Full Abstraction Result......Page 277 5. Conclusion......Page 280 References......Page 281 Introduction......Page 282 1. I-categories......Page 283 2.1. Colimit/limit coincidence. Dual I-categories.......Page 290 2.2. Initial/final algebras.......Page 291 2.3. Conservative extensions.......Page 292 3. Induction and Coinduction......Page 294 References......Page 297 Geometric Theories and Databases......Page 300 1. Introduction......Page 301 2. Geometric logic......Page 305 2.1 Flat functors and Diaconescu's Theorem......Page 309 2.2 Geometric logic as observational logic......Page 311 3. The lower bagdomain......Page 314 4. The mixed bagdomain......Page 319 5.2 Continuous domains......Page 323 5.5 Dynamic predicate geometric logic......Page 324 References......Page 325 1. Introduction......Page 327 2. Indexed Coproducts......Page 329 3. Partial Products......Page 332 4. Algebraic Bagdomains......Page 337 5. The Bagdomain Monad and its Algebras......Page 340 6. Bagdomains and Scones......Page 344 7. Bagdomains and Powerdomains......Page 347 8. Upper and Mixed Bagdomains......Page 348 References......Page 350 Computational comonads and intensional semantics / Stephen Brookes, Shai Geva Weakly distributive categories / J.R.B. Cockett, R.A.G. Seely Sequentiality and full abstraction / P.-L. Curien Remarks on algebraically compact categories / Peter Freyd Dinaturality for free / Peter J. Freyd, Edmund P. Robinson, Giuseppe Rosolini Simply typed and untyped lambda calculus revisited / Bart Jacobs Modelling reduction in confluent categories / C. Barry Jay On clubs and data-type constructors / G.M. Kelly Penrose diagrams and 2-dimensional rewriting / Yves Lafont Strong monads, algebras and fixed points / Philip S. Mulry Semantics of local variables / P.W. O'Hearn, R.D. Tennent Using fibrations to understand subtypes / Wesley Phoa Reasoning about sequential functions via logical relations / Kurt Sieber I-categories and duality / M.B. Smyth Geometric theories and databases / Steven Vickers Partial products, bagdomains and hyperlocal toposes / P.T. Johnstone. Category theory and related topics of mathematics have been increasingly applied to computer science in recent years. This book contains selected papers from the London Mathematical Society Symposium on the subject which was held at the University of Durham. Participants at the conference were leading computer scientists and mathematicians working in the area and this volume reflects the excitement and importance of the meeting. All the papers have been refereed and represent some of the most important and current ideas. Hence this book will be essential to mathematicians and computer scientists working in the applications of category theory. Category theory is being increasingly applied to computer science. Participants at the symposium on which this volume is based were leading computer scientists and mathematicians working in the area. The volume represents some of the most important and current ideas, hence will be essential to people applying category theory. We explore some foundational issues in the development of a theory of intensional semantics, in which program denotations may convey information about computation strategy in addition to the usual extensional information.