Subject: a paper Date: Wed, 31 Mar 93 16:26:57 EST From: pavlovic@triples.Math.McGill.CA (Dusko Pavlovic) A paper on logic and factorisations MAPS I: RELATIVE TO A FACTORISATIONS SYSTEM by Dusko Pavlovic is available by anonymous ftp from triples.math.mcgill.ca. The file is called mapsI-A4.dvi.Z (or mapsI-US.dvi.Z). It is in the directory pub/pavlovic. Please let me know if you have problems fetching or printing this file. Regards, Dusko Pavlovic Abstract Originally, the categorical calculus of relations was developed using the canonical factorisation in regular categories. More recently, relations restricted to a proper factorisation system have been studied by several authors. In the present paper, we consider the general situation, in which relations are induced by an arbitrary stable factorisation. This extension of the calculus of relations is necessary for a categorical development of strongly constructive (and computational) logic, where non-monic relations come about naturally. In this setting, we analyze the correspondence of the maps, i.e. the total, single-valued relations, and the functions, as given by the arrows in the underlying category. ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Subject: mapsI Date: Mon, 5 Apr 93 12:13:30 EDT From: pavlovic@triples.Math.McGill.CA (Dusko Pavlovic) There was a gap in section 3 of my paper "Maps I", announced here on Friday. I noticed and fixed it on Sunday, but some people had already downloaded it. Sorry about this. - Dusko Pavlovic ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Subject: Piaget Date: 10 Apr 93 10:08:40 EST From: ------------- Has anyone here seen Piaget's book _Morphismes et Categories_? I haven't yet, but will, and I wondered if anyone had an opinion on it. (It is not clear to me from the listing how much of it is by Piaget.) Best, Colin McLarty ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Subject: Workshop on Foundational Methods in Computer Science Date: Sat, 10 Apr 93 10:21 PDT From: hook@hood.cse.ogi.edu (Jim Hook) Preliminary Announcement: Second Annual Workshop on Foundational Methods in Computer Science A workshop on applications of categories in computer science Dates: June 4-6, 1993 Location: Reed College, Portland, Oregon Overview: This will be the second year of the workshop on foundational methods in computer science. It is an "informal, even casual," workshop bringing together mathematicians and computer scientists with an interest in category theory and its applications to computer science. The workshop will have approximately the same format as last year, with a one day tutorial on June 4 and short research presentations on June 5 and 6. There will not be a formal proceedings. Guests: I am still in the process of contacting distinguished visitors and guests. Tutorials will be presented by Ernie Manes, Robin Cockett and David Benson (there may be others as well). Participation: People wishing to participate should send me email. We hope to encourage the participation of researchers at all levels in this workshop. Fees: I have made arrangements for dormitory accommodations and classroom space. I haven't negotiated the meal plan yet and I haven't completed a budget, so I don't yet have a registration fee calculated. I hope to keep the fees to an absolute minimum. ---------------------------------------------------------------------------- James Hook | Department of Computer Science and Engineering hook@cse.ogi.edu | Oregon Graduate Institute of Science & Technology Phone: (503) 690-1169 | 19600 N.W. von Neumann Drive Fax: (503) 690-1029 | Beaverton, OR 97006-1999 ---------------------------------------------------------------------------- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Subject: LICS93 Date: Sat, 10 Apr 93 18:33:57 ADT From: "daniel leivant" May I request you to post the following announcement on any appropriate email distribution list, news board, newsletter, or journal, which is in your responsibility. I apologize for the rather impersonal nature of this memo, and I hope this will not affect your willingness to assist with LICS93 publicity. Thanks very much in advance Daniel Leivant LICS Publicity Chair LOGIC IN COMPUTER SCIENCE (LICS) ******************************** Eighth Annual IEEE Symposium June 19-23, 1993, Montreal, Canada ADVANCE REGISTRATION AND PROGRAM INFORMATION ============================================ (The conference flyer is accessible via anonymous ftp from cs.indiana.edu, directory /pub/logic, files lics93.tex, lics93.dvi, lics93.ps etc.) CONFERENCE OFFICE. ================= Please address forms, payments and inquiries to: LICS93 Secretariat, Conference Office McGill University 550 Sherbrooke Str. West, West Tower, Suite 490 Montreal, Canada H3A 1B9 Phone: (514) 398-3770 Fax: (514) 398-4854 Email: lics93@cs.mcgill.ca REGISTRATION DESK. ================= A registration and information desk will be located at the Stephen Leacock Building, and the Welcome Reception will take place at Redpath Hall, both on McGill University's main campus. Entering campus through the McTavish Street entrance (below the corner of Dr. Penfield) Leacock will be the second building on your left, and Redpath the first on your right. The registration desk will operate on: The desk will operate on: * Saturday, June 19: 2-6pm * Sunday, June 20: 7:30am-6pm * Monday, June 21: 8am-6pm * Tuesday, June 22: 8am-6pm * Wednesday, June 23: 8-11am REGISTRATION FEES. ================= A table of registration fees can be found on the registration form. The member rate applies to members of a sponsoring organization (IEEE Computer Society, ACM, EATCS, ASL), members of the organizing and program committees, and authors of accepted papers. The student rate applies to full time students. All registration privileges are extended to the reduced rates. In the event of cancellation fees will be refunded, except for a $50 cancelation fee, provided a written request is received by the conference office by April 30. Payment of fees must accompany the registration form. Registrants may use a charge card (Visa, MasterCard, or American Express) by filling out the details and signing the appropriate portion of the registration form. Canadian and US residents may also send a personal check or money order, which must be in their national currency. Other registrants may also send an international money order, which must be in Canadian dollars. Checks and money orders should be payable to "LICS'93-McGill University". Fees include a 7% federal (GST) tax and a 4% provincial (PST) tax, which are refundable (except for residents of Canada for GST and residents of Quebec for PST). Refund forms will be included in the registration package. LODGING. ======= Blocks of rooms have been reserved at the Shangrila Hotel, for a pre-tax rate of $96 per night (single or double), and at the McGill University Royal Victoria College, for a pre-tax rate of $33 per night (single only). Both are a few minute walk from the conference site. To guarantee your reservation a deposit must be made by May 14, either by using a charge card (filling out the appropriate form in the registration form), or by contacting the hotel directly. All accommodation fees should be paid directly to the hotel at check-out time. For further information, please contact: Le Shangrila Hotel 3407 Peel Str. Montreal, Canada H3A 1W7 Phone: 514-288.4141, 800-361.7791 Fax: 514-288.3021 McGill Residences Royal Victoria College 3425 University Street Montreal, Canada, H3A 1X6 Phone: 514-398.6378 Fax: 514-398.4455 Montreal Convention & Tourism Bureau 1555 Peel Street, Room 600 Montreal, Canada H3A 1X6 Phone: 514-844.5400 Fax: 514-844.5757 Additionally, a block of suites has been reserved at Le Monfort at a special eight night rate (June 15th to June 23), ranging from a studio (bed & sofa-bed) at the rate of C$400 to a two bedroom apartment at C$725, all including small kitchen and dining area. This is of particular interest to people attending both RTA (June 16-18) and LICS (for RTA'93 information: rta93@cs.concordia.ca). Le Monfort is a few minute walk from the RTA site, and a short subway ride (or about 20 minute walk) from the LICS site. Reservations must be made directly with the hotel by May 7: Le Monfort (attn. Gisele Gariepy) 1975, de Maisonneuve Ouest Montreal H3H 1K4 Phone: 514-934.0916 Fax 514-939.2552 AIRPORT INFORMATION. =================== Domestic and US flights arrive at Dorval Airport. Buses depart every 20 minutes to the Berri Metro in downtown Montreal, a 20 minute ride, for a fare of $8.50. The taxi fare is about $25. Intercontinental flights arrive at Mirabel Airport, 56 km (35 miles) from downtown. There is a frequent bus service to the Berri Metro, for a fare of $13. Cab fare may reach $50. REGISTRATION AND ACCOMMODATION FORM *********************************** First Name __________________ Last Name ___________________ Affiliation ________________________________________________ Mailing Address _____________________________________________ _______________________________________________________ _______________________________________________________ Phone(s) _______________________ Fax: ______________________ E-mail: ___________________________________________________ RATES. Fees indicated below are in [Canadian dollars/US dollars]. Please indicate the applicable rate (and currency) by circling it on the table, and also writing it in. through 05.14 from 05.15 on site Regular 425/340 500/400 600/480 Member 375/300 450/360 550/440 Student 200/160 250/200 300/240 * Fee: ____________ * Justification: ______________________ HOTEL RESERVATION. Please mark the desired accommodation: * Shangrila single / double * McGill Residences (only single) * Arrival: _____________ * Departure: _________________ * No reservation requested MODE OF PAYMENT (Note: Accomodations must be guaranteed by May 14. See REGISTRATION section above.) Please circle one: Check Money Order VISA MC AmExp Credit Card Information (if applicable): Name on card ________________________________ Card Number _________________________________ Expiration date _____________________________ Signature ___________________________________ Charge card to be used for (please mark the appropriate): registration fees / accommodation guarantee / both CONFERENCE PROGRAM ****************** (All talks at Stephen Leacock Building) SATURDAY, June 19 ================= REGISTRATION (at Stephen Leacock Bldng) (2:00-6:00 pm) WELCOME RECEPTION (at Redpath Hall) (5:00-7:00 pm) SUNDAY, June 20 =============== TUTORIAL (8:30-10:00am) Chair: R. Constable (Cornell) Andrew M. Pitts (Cambridge): Bisimulation and co-induction SESSION 1: TYPES Chair: M. Abadi (DEC-SRC) (10:30-12:30) 10:30 The genericity theorem and the notion of parametricity in the polymorphic lambda-calculus Giuseppe Longo (ENS), Kathleen Milsted (DEC-PRL) & Sergei Soloviev (Russian Academy of Science) 11:00 Standard ML weak polymorphism and imperative constructs, My Hoang (Stanford), John Mitchell (Stanford) & Ramesh Viswanathan (Stanford) 11:30 A lambda calculus of objects and method specialization, John Mitchell (Stanford), Furio Honsell (Udine) & Kathleen Fisher (Stanford) 12:00 Strong normalization for second order classical natural deduction, Michel Parigot (Paris VII) HOSTED LUNCH (at the University Center Cafeteria) (12:30-2:00) SESSION 2: DEDUCTION Chair: N. Shankar (SRI) (2:00-4:00) 2:00 Automated production of traditional proofs for constructive geometry theorems, Shang-Ching Chou (Wichita State), Xiao-Shan Gao (Edinburgh) & Jing-Zhong Zhang (Wichita State) 2:30 On the unification problem for cartesian closed categories, Paliath Narendran (SUNY-Albany), Frank Pfenning (CMU) & Richard Statman (CMU) 3:00 Functional unification of higher-order patterns, Tobias Nipkow (TU Muenchen) 3:30 Set constraints are the monadic class, Leo Bachmair (SUNY-Stony Brook), Harald Ganzinger (Max Planck Inst) & Uwe Waldmann (Max Planck Inst) SESSION 3: SEMANTICS Chair: P.J. Freyd (U. Penn) (4:30-6:00) 4:30 Relational properties of recursively defined domains, Andrew M. Pitts (Cambridge) 5:00 Full abstraction for a shared variable parallel language, Stephen Brookes (CMU) 5:30 A coinduction principle for recursive data types based on bisimulation, Marcelo P. Fiore (Edinburgh) BUSINESS MEETING (at Leacock Building) (8:00-10:00) MONDAY, June 21 =============== TUTORIAL Chair: Y. Moschovakis (UCLA) (8:30-10:00) Phokion G. Kolaitis (UC Santa Cruz): Finite-model theory SESSION 4: MODAL & TEMPORAL LOGICS (10:30-12:30) Chair: M.Y. Vardi (IBM-Almaden) 10:30 In and out of temporal logic, Amir Pnueli (Weizmann Inst) & Lenore Zuck (Yale) 11:00 On completeness of mu-calculus, Igor Walukiewicz (Warsaw) 11:30 On model checking for real-time properties with durations, A. Bouajjani (LGI-IMAG), R. Echahed (LGI-IMAG) & J.Sifakis (LGI-IMAG) 12:00 Verifying programs with unreliable channels, Parosh Abdulla (Uppsala) & Bengt Jonsson (Uppsala) LUNCH BREAK (12:30-2:00) SESSION 5: FINITE-MODEL THEORY (2:00-4:00) Chair: P.G. Kolaitis (UC Santa Cruz) 2:00 y = 2x vs. y = 3x Alexei Stolboushkin (UCLA) & Damian Niwinski (Warsaw) 2:30 Monadic second-order logic and hypergraph orientation, Bruno Courcelle (Bordeaux I) 3:00 Infinitary logics and very sparse random graphs, James F. Lynch (Clarkson) 3:30 Asymptotic probabilities of languages with generalized quantifiers, Guy Fayolle (INRIA), Stephane Grumbach (INRIA) & Christophe Tollu (Paris-Nord) SESSION 6: LOGIC PROGRAMMING (4:30-6:00) Chair: D. Miller (U. Penn) 4:30 Compositional analysis for concurrent constraint programming, Moreno Falaschi (Padova), Maurizio Gabbrielli (Pisa), Kim Marriott (Monash) & Catuscia Palamidessi (Genova) 5:00 Rules of definitional reflection, Peter Schroeder-Heister (Tubingen) 5:30 Encoding the calculus of constructions in a higher-order logic, Amy Felty (Bell Labs) CONFERENCE RECEPTION (at Redpath Hall) (6:00-7:30) EVENING LECTURE (at Leacock Bldg) (8:00-9:00) Chair: M. Okada (Concordia) Jim Lambek (McGill): Programs, grammars and arguments -- a personal view of some connections between computation, language and logic TUESDAY, June 22 ================ INVITED TALK Chair: P. Panangaden (McGill) (9:00-10:00) Jon Barwise (Indiana): Information flow in imperfect channels SESSION 7: LAMBDA CALCULUS (10:30-12:30) Chair: S. Abramsky (Imperial Coll) 10:30 A typed pattern calculus, Val Breazu-Tannen (U.Penn), Delia Kesner (INRIA/Paris-Sud) & Laurence Puel (Paris-Sud) 11:00 Non-determinism in a functional setting, C.-H. Luke Ong (Cambridge/Singapore) 11:30 Adequacy for untyped translations of typed lambda-calculi, Wesley Phoa (U. of New South Wales) 12:00 Local and asynchronous beta-reduction, Vincent Danos (CNRS) & Laurent Regnier (CNRS) LUNCH BREAK (12:30-2:00) SESSION 8: COMPLEXITY & DATABASES (2:00-4:00) Chair: P. Clote (Boston Coll) 2:00 An exponential separation between the matching principle and the pigeonhole principle, Paul Beame (U Washington) & Toniann Pitassi (UC San Diego) 2:30 Some desirable conditions for feasible functionals of type 2, Anil Seth (Tata Institute) 3:00 Database query languages embedded in the typed lambda calculus, Gerd G. Hillebrand (Brown), Paris C. Kanellakis (Brown) & Harry G.Mairson (Brandeis) 3:30 Homomorphic tree embeddings and their applications to recursive program optimization, V.S. Lakshmanan (Concordia), Karima Ashraf (Concordia) & Jiawei Han (Simon Fraser) SESSION 9: REWRITING Chair: P. Lescanne (CRIN) (4:30-6:00) 4:30 The order types of termination orderings on terms, strings and multisets, Ursula Martin (St.Andrews) & Elizabeth Scott (St.Andrews) 5:00 The unifiability problem in ground AC theories, Paliath Narendran (SUNY-Albany) & Michael Rusinowitch (INRIA/CRIN) 5:30 Lambek grammars are context free, Mati Pentus (Moscow U) FREE EVENING WEDNESDAY, June 23 ================== INVITED TALK Chair: M.Abadi (DEC-SRC) (8:45-9:45) Gordon D.Plotkin (Edinburgh): Type theory and recursion SESSION 10: CONCURRENCY Chair: B.Bloom (Cornell) (10:05-12:35) 10:05 Typing and subtyping for mobile processes, Benjamin Pierce (Edinburgh) & Davide Sangiorgi (Edinburgh) 10:35 Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes, Soren Christensen (Edinburgh), Yoram Hirshfeld (Edinburgh) & Faron Moller (Edinburgh) 11:05 A fully abstract denotational model for higher-order processes, M.Hennessy (Sussex) 11:35 Self-synchronization of concurrent processes, Lalita Jategaonkar (MIT) & Albert R. Meyer (MIT) 12:05 Bisimulation and open maps, Andre Joyal (UQAM Montreal), Mogens Nielsen (Aarhus) & Glynn Winskel (Aarhus) END OF CONFERENCE CONFERENCE ORGANIZATION *********************** LICS General Chair: Robert L. Constable 1993 Conference Co-chairs: Mitsuhiro Okada & Prakash Panangaden 1993 Program Chair: Moshe Y. Vardi Publicity Chair: Daniel Leivant PROGRAM COMMITTEE: ================= M. Abadi, S. Abramsky, B. Bloom, P. Clote, P.J. Freyd, D. Harel, K.G. Larsen, P. Lescanne, D. McAllester, J. Meseguer, D. Miller, Y. Moschovakis, N. Shankar, C. Talcott, M.Y. Vardi, and P. Wolper. ORGANIZING COMMITTEE: ==================== M. Abadi, S. Abramsky, S. Artemov, J. Barwise, M. Blum, A. Borodin, A. Bundy, S. Buss, E. Clarke, R. Constable (Chair), E. Engeler, J. Gallier, U. Goltz, Y. Gurevich, S. Hayashi, G. Huet, G. Kahn, D. Kapur, C. Kirchner, R. Kosaraju, J.W. Klop, P. Kolaitis, D. Leivant, A.R. Meyer, G. Mints, J. Mitchell, Y. Moschovakis, M. Okada, P. Panangaden, A. Pitts, G. Plotkin, S. Ronchi della Rocca, G. Rozenberg, A. Scedrov, D. Scott, J. Tiuryn, M.Y. Vardi, R. de Vrijer. ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Subject: Re: Piaget Date: Mon, 12 Apr 93 13:58:42 EDT From: barr@triples.Math.McGill.CA (Michael Barr) Bizarre! No, I haven't seen nor heard of it. I spoke with Aczel, who gave a talk at the recent meeting in New Orleans I was at. He has toned down his claims for NWF sets quite a bit and now only claims that they are useful for intuition. He does prefer to talk of sets and classes, where I might prefer an inaccessible, but that is perfectly harmless as far as I am concerned. Michael ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Subject: ftp access: Adjoint Char'n of Cat of Sets Date: April 12,1992 From: Bob Rosebrugh The paper whose abstract follows is available by anonymous ftp in the directory pub/papers/rosebrugh at sun1.mta.ca (138.73.1.12) as the files accs.{dvi,tex} If you download the latter you need to know that it is in LaTeX and uses the bibliography file accs.bib and Mike Barr's diagram macros, diagram.tex, both found in the same directory. Don't hesitate to contact me if you experience any difficulties or need ftp instructions. I will gladly forward a paper copy. If you request one be sure to include a full postal address. Bob Rosebrugh +++++++++++++++++++++++++++++++++++ An adjoint characterization of the category of sets Robert Rosebrugh and R. J. Wood Abstract If a category B with Yoneda embedding Y : B ---> CAT(B^op,set) has an adjoint string, U -| V -| W -| X -| Y, then B is equivalent to set.  ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Subject: Upgrade to CTCS Date: Tue, 13 Apr 93 11:58:07 EDT From: barr@triples.Math.McGill.CA (Michael Barr) \item[p. 236] (Frank Piessens). The statement, ``It would be incorrect to assume in general (although it is true in familiar examples) that every node of $\Tsc$ is a limit of a diagram in the graph of $\Ssc$'' is wrong. The reason is that $\Tsc\op$ is a full subcategory of the category $\Fun(\Ssc,\Set)$ (to be precise, that should be the free category generated by the graph underlying $\Ssc$) and every functor is a colimit of representables and, hence, in $\Tsc$, every functor is a limit of them. Thus every object of the theory is a limit of a diagram built from the objects and arrows of $\Ssc$. \item[p. 387] (Nico Verwer). The solution to Exercise 4 of 8.3 contains several errors. The right hand label of the diagram should be $$, the lower left corner of the diagram should be $B$ and the $f\x g$ in the displayed line that begins $G(X)=\ldots$ should also be $$. ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Subject: *** Modulated Bicategories *** Date: Thu, 15 Apr 93 14:59:15 +1000 From: domv@macadam.mpce.mq.edu.au Paper Preprint Available ======================== The following paper preprint is available for anonymous FTP from ftp.mpce.mq.edu.au (137.111.216.12) in /pub/maths/Categories/mod.bicats.ps.Z The abstract is available as /pub/maths/Categories/mod.bicats.abs MODULATED BICATEGORIES. Aurelio Carboni, Scott Johnson, Ross Street, and Dominic Verity ABSTRACT: The concept of regular category has several 2-dimensional analogues depending upon which special arrows are chosen to mimic monics. Here, the choice of the conservative arrows, leads to our notion of faithfully conservative bicategory K in which two-sided discrete fibrations become the arrows of a bicategory F=DFib(K). While the homcategories F(B,A) have finite limits, it is important to have conditions under which these finite ``local'' limits are preserved by composition (on either side) with arrows of F. In other words, when are all fibrations in K flat? Novel axioms on K are provided for this, and we call a bicategory H modulated when H^op is such a K. Thus, we have {\bf constructed} a proarrow equipment ()_*:H-->M (in the sense of Wood) with M=F^coop. Moreover, M is locally finitely cocomplete and certain collages exist. In the converse direction, if M is any locally countably cocomplete bicategory which admits finite collages, then the bicategory M^* of maps in M is modulated. {Recall that a 1-cell in a bicategory is called a {\it map\/} when it has a right adjoint.} --------------------------------------------------------------------------- To fetch and print a copy of the file, use the following procedure: % ftp ftp.mpce.mq.edu.au Name: anonymous Password: @ ftp> cd /pub/maths/Categories ftp> binary ftp> get mod.bicats.ps.Z ftp> quit % uncompress mod.bicats.ps.Z % lpr -P mod.bicats.ps If your site does not support the Unix uncompress program, or you have trouble fetching compressed files, our server can uncompress the file for you. Simply fetch mod.bicats.ps instead of mod.bicats.ps.Z. --------------------------------------------------------------------------- Dominic Verity, Macquarie University, NSW 2109, Australia. email: domv@macadam.mpce.mq.edu.au ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Subject: Monograph announcement Date: Thu, 15 Apr 93 15:55:29 +0200 From: curien@dmi.ens.fr The second, thoroughly revised, edition of my monograph Categorical combinators, Sequential algorithms and Functional programming, by P.-L. Curien just appeared in the series Progress in Theoretical Computer Science, Birkhauser. I enclose the contents of the back cover, the table of contents, and the preface to the second edition, to give an idea of the contents and of the improvements with respect to the first edition. Order and price info are given at the end. ------------------------------------------------------ BACK COVER This book is a thoroughly revised edition of a monograph that appeared under the same title in 1986 in the Series Research Notes in Theoretical Computer Science, Pitman. It presents an approach to the design and implementation of sequential programming languages based on the relationship between lambda-calculus and category theory. The foundations of a new "categorical" combinatory logic are laid down. Compilation and evaluation techniques are investigated. A simple abstract machine, called the Categorical Abstract Machine, is presented: it has served as the core of the implementation of the language CAML, of the ML family, developped at INRIA-Roquencourt and Ecole Normale Supe'rieure, and first released in 1987. The main characteristics of this approach are conceptual simplicity and compacity, with bearings on portability, efficiency, and correctness proofs. A mathematical semantics of sequentiality is proposed, in which "sequential algorithms" rather than functions are used to interpret procedures. The theoretical investigation has led to the development of a programming language, {bold CDS0}, in which basic and functional types are not differentiated. The evaluation framework is a demand-driven data flow network. The model of sequential algorithms is fully abstract with respect to this language: two procedures have the same denotation if and only if they have the same behaviour. Background on full abstraction is given. The new edition covers new results, and introduces new connections, as suggested by the following non exhaustive list of keywords: confluence properties of categorical combinators, explicit substitutions, control operations, linear logic, geometry of interaction, strong stability. ------------------------------------------------- TABLE OF CONTENTS PREFACE TO THE SECOND EDITION PREFACE TABLE OF DEPENDENCIES INTRODUCTION 1. CATEGORICAL COMBINATORS 1.1 Introducing categorical combinators 1.2 lambda-calculus and untyped categorical combinatory logic 1.3 Types and cartesian closed categories 1.4 From untyped calculus to typed calculus: axiomatizing a universal type 1.5 Models of the %lbd%-calculus 1.6 Equivalences of presentations 1.7 Evaluation of categorical terms 1.8 Discussion 2. SEQUENTIAL ALGORITHMS 2.1 Concrete data structures 2.2 Representation theorems 2.3 Domain equations 2.4 Sequential functions 2.5 Sequential algorithms 2.6 The category of concrete data structures and sequential algorithms 2.7 Discussion 3. CDS0: THE KERNEL OF A FUNCTIONAL LANGUAGE 3.1 Declaring concrete data structures 3.2 The language of constants: states and sequential algorithms 3.3 The language of expressions 3.4 Operational semantics: presentation 3.5 Operational semantics: the rules of CDS01 3.6 Full abstraction for CDS01 3.7 Discussion 4. THE FULL ABSTRACTION PROBLEM 4.1 The languages PCF, PCFP and PCFC 4.2 Sequential algorithms and extensionality: the bicds's 4.3 Complete bicds's 4.4 Extensional algorithms and definability 4.5 Discussion 5. CONCLUSION 6. MATHEMATICAL PREREQUISITES REFERENCES INDEX OF DEFINITIONS INDEX OF SYMBOLS ------------------------------------------------- PREFACE TO THE SECOND EDITION This book is a revised edition of the monograph which appeared under the same title in the series Research Notes in Theoretical Computer Science, Pitman, in 1986. In addition to a general effort to improve typography, English, and presentation, the main novelty of this second edition is the integration of some new material. Part of it is mine (mostly jointly with coauthors). Here is brief guide to these additions. - I have augmented the account of categorical combinatory logic with a description of the confluence properties of rewriting systems of categorical combinators (Hardin, Yokouchi), and of the newly developed calculi of explicit substitutions (Abadi, Cardelli, Curien, Hardin, Le'vy, and Rios), which are similar in spirit to the categorical combinatory logic, but are closer to the syntax of %lbd%-calculus (Section 1.2). - The study of the full abstraction problem for PCF and extensions of it has been enriched with a new full abstraction result: the model of sequential algorithms is fully abstract with respect to an extension of PCF with a control operator (Cartwright, Felleisen, Curien). An order-extensional model of error-sensitive sequential algorithms is also fully abstract for a corresponding extension of PCF with a control operator and errors (Sections 2.6 and 4.1). - I suggest that sequential algorithms lend themselves to a decomposition of the function spaces that leads to models of linear logic (Lamarche, Curien), and that connects sequentiality with games (Joyal, Blass, Abramsky) (Sections 2.1 and 2.6). - There is even more to the connection with linear logic: the operational semantics of sequential algorithms, formalized in Chapter 3, bears striking similarities with the geometry of interaction, developed for linear logic by Girard in 1988. In Section 3.4, I have included a prologue and a picture to help conveying this conceptual similarity. - I include a short description of some results of Bucciarelli and Ehrhard, who have proposed a more abstract theory of sequential algorithms (Section 2.4), an extensional (but not order-extensional) notion of strong stability, that is closed under exponentiation and coincides with sequentiality at first order (Section 2.6), and a method of order-extensional embedding (Section 4.4). - These results are reported mostly in the form of exercises. I have decorated some exercises with a star to stress that their solution represents a significant work. The reader can use them as a quick reference to the source papers. Here are a few other new works that I account for: - adaptations of abstract environment machines to carry out full normalization of %lbd%-terms (Cre'gut, Asperti, Curien) (Section 1.2); - a hierarchical coherence theorem whose proof by Lafont gives as a side-effect a proof of termination of the execution of simply typed terms by the categorical abstract machine (Section 1.3); - the inability of graph reduction of categorical combinators to implement optimal sharing of reductions (Curien, Field, Le'vy) (Section 1.7); - further results on representation theorems for event domains, and solutions of domain equations (Droste) (Sections 2.2 and 2.3); - the striking connection between (extensional) sequential algorithms and the oracle semantics of higher-order recursion theory developed by Kleene in the last years of his scientific career (Section 2.7); - the works of Brookes and Geva on various approaches to intensional continuous semantics (Section 2.7); - the use of logical relations to obtain a full abstraction result for order up to 3 (Sieber) (Sections 4.1 and 4.2). ... -------------------------------------------------------- To order: in North America call (201) 348-4033, or write Birkhaeuser, 44 Hartz Way, Secaucus, NJ 07096-2491. outside North America, please contact Birkhaeuser Verlag AG, Klosterberg 23, CH-4010, Basel, Switzerland. FAX 061 271 7666. Price: $64.50 (US dollars) (hardcover only) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Subject: Categories of relational structures Date: Fri, 30 Apr 93 20:31:14 ADT From: Vaughan Pratt Define a relational structure (A,R) to consist of a set A and a n-ary relation on A for some ordinal n. A homomorphism f:(A,R)->(B,S) is a function f:A->B between the underlying sets of two relational structures of the same arity, such that f(R) c S. Write Str_n for the category of all n-ary relational structures and homomorphisms between them, and Str for the sum in CAT of Str_n over all ordinals n. 1. What is the term for the notion of full subcategory of either Str_n or Str? Failing that, what would be a suitable term? Relational categories? Categories of relational structures? Familiar examples of such categories and an upper bound on their arities include those of groups (3), rings (4), fields (4), lattices (3), vector spaces over the field K (1+max(|K|,2)), directed graphs (2), posets (2), and categories (3). I would expect complete lattices, complete Boolean algebras, topological spaces, and hypergraphs not to embed in Str_n for any n, because their structural elements (subsets, e.g. open sets) have no fixed cardinality bound, unlike n-tuples. A pointer to a proof of such nonembedding, or a demonstration of how to embed them, would be greatly appreciated. Since the concept is such a natural one, this question must surely have been looked at before. 2. What generalizations of Str or Str_n have been considered? One can make Str a bit more "communicative" by permitting homomorphisms between dissimilar structures (A,R), (B,S) of respective arities m