April 1991 - Categories - categories.org.au

Re: Categorical view of loop invariants (& diagrams)
by Paul Taylor 29 Apr '91

29 Apr '91

By "diagrams3", Barry Jay means the same version as was quite widely distributed last year; it hasn't changed significantly since then. It would be better to ask me for it than him, though. (It was temporarily called diagrams3 whilst version 2 was still in service and I wasn't confident about version 3)

1 0

Event spaces paper
by Vaughan Pratt 26 Apr '91

26 Apr '91

"Event Spaces and Their Linear Logic," which I promised way back in February, is now a more or less complete 19-page paper, see abstract below. It is available as pub/es.tex from Boole.Stanford.EDU by anonymous ftp, and will appear in the AMAST'91 proceedings (AMAST is in Iowa City late next month, May 22-25). It supersedes "Concurrent Automata and Their Logic". See pub/README on Boole for abstracts of related papers. The intended application of event spaces is to modelling concurrency. In January I claimed that they were incidentally "the best model of linear logic to date". The guardians of posterity were understandably shocked. Let me try to attenuate my obvious proprietor's bias a bit by listing the criteria for "best" that I have in mind. Only criterion 2 has the force of a theorem, but the other two are surely clear enough that one could reasonably hope for some sort of consensus. Event spaces are 1. simple: the category is just posets with all nonempty joins and a top, and their homomorphisms. 2. nondegenerate: the sums and products are four distinct operations; 3. useful: their primary raison d'etre is not as a model of linear logic but as a model of concurrency that in comparison to event structures is more general and has a cleaner algebraic structure, namely that of full linear logic. If you have a model of full linear logic that meets all three criteria as well or better I am likely to be among your first and most enthusiastic customers (unless it turns out to require inaccessible cardinals). The closest competitor seems to be Girard's original model, coherent spaces and their linear morphisms. However the objects are a very special case of state spaces (dual to event spaces), while the morphisms require the conditions of monotonicity, continuity, stability, and linearity, whereas event space morphisms are merely homomorphisms. Those models of full linear logic that purport to model concurrency all seem very complicated to me, though I'd be very happy to be set straight if I've overestimated the complexity of someone's model. Other features of the paper: What linear logic is about (answer: it combines elementary and categorical logic in the one system). Applications of event spaces to family planning (no connection with risque computers). Herewith the abstract. ABSTRACT Boolean logic treats disjunction and conjunction symmetrically and algebraically. The corresponding operations for computation are respectively nondeterminism (choice) and concurrency. Petri nets treat these symmetrically but not algebraically, while event structures treat them algebraically but not symmetrically. Here we achieve both via the notion of an event space as a poset with all nonempty joins representing concurrence and a top representing the unreachable event. The symmetry is with the dual notion of state space, a poset with all nonempty meets representing choice and a bottom representing the start state. The algebra is that of a parallel programming language expanded to the language of full linear logic, Girard's axiomatization of which is satisfied by the event space interpretation of this language. Event spaces resemble vector spaces in distinguishing tensor product from direct product and in being isomorphic to their double dual, but differ from them in distinguishing direct product from direct sum and tensor product from tensor sum.

1 0

Tex 3.0
by Vaughan Pratt 25 Apr '91

25 Apr '91

Don't worry too much about Tex 3.1, all the systems I'm aware of are only up to 3.0 (Paul's included, he confesses!). If you want to upgrade to 3.0, here are some places to look. Except for the first I found these by sending mail to archie(a)quiche.cs.mcgill.ca (a program) with subject "prog tex" and picking out those that referred to tex3.0. (I should have said "prog tex3.0"). Many more don't so identify themselves with the 3.0 suffix but may well carry tex3.0. For those not used to using anonymous ftp to fetch things with I include a copy of the README from Boole.Stanford.EDU, whose "Instructions" section explains the procedure. Vaughan Pratt Host labrea.stanford.edu (36.8.0.47) Location: /pub/tex Host ccadfa.cc.adfa.oz.au (131.236.1.2) Location: /tex/tex-3.0 Host emx.utexas.edu (128.83.1.33) Location: /pub/mnt/source/tex/tex-3.0 Host freja.diku.dk (129.142.96.1) Location: /TeX/TeX-3.0 Host psuvax1.cs.psu.edu (130.203.1.6) Location: /pub/src/TeX3.0/TeX3.0 Host ugle.unit.no (129.241.1.97) Location: /pub/tex/tex-3.0 Host uxc.cso.uiuc.edu (128.174.5.50) Location: /text/TeX3.0/TeX3.0 Host walhalla.informatik.uni-dortmund.de (129.217.64.63) Location: /pub/comp/msdos/emtex3.0 The Sun Garage Cache Prepublication Medium Papers on Parallel Software Theory Available by Anonymous FTP from Boole.Stanford.EDU This file is README in the /pub directory of Boole.Stanford.EDU, 36.8.0.65, accessible by anonymous ftp. The /pub directory is for FTP distribution of prepublications in the area of parallel software theory. It is run by the Boole group, a subgroup of the Mathematical Theory of Computation group, Computer Science Department, Stanford University. The group consists of the following people. Ross Casley casley(a)cs.stanford.edu (SYS) Roger Crew crew(a)cs.stanford.edu (SYS) Rob van Glabbeek rvg(a)cs.stanford.edu Vineet Gupta vgupta(a)cs.stanford.edu Vaughan Pratt (group leader) pratt(a)cs.stanford.edu (SYS) Pat Simmons (secretary) simmons(a)cs.stanford.edu Orli Waarts orli(a)cs.stanford.edu ==========================Instructions================================= FTP LOGIN. Give the following commands. ftp boole.stanford.edu Login: anonymous (if you don't have an account on boole) Paswd: yoursurname (though any string will work) bin (if you are retrieving a .dvi file) prompt off (if you want no ? prompts from mget) cd pub (change directory to ^ftp/pub ls -lt (see what's there, most recent first) mget filename-1 ... filename-n (e.g. mget cg.tex logic.bib) quit (exit from FTP) SOURCE. To retrieve the source to paper foo, get foo.tex and logic.bib. The source should be compiled using latex foo; bibtex foo; latex foo; latex foo DVI. If you wish to print paper foo without having to compile with latex, retrieve just foo.dvi. You must first give the bin command to ftp since .dvi files are not text files. Print foo.dvi on your host using lpr -d foo.dvi. PROBLEMS. If you have problems in either retrieving or compiling papers, please contact a systems person (flagged SYS on the list above). ===========================Available papers================================= TITLES casthes.tex On the Specification of Concurrent Systems es.tex Event Spaces and their Linear Logic (in preparation) catl.tex Concurrent Automata and Their Logic (old es.tex, temporary) cg.tex Modeling Concurrency with Geometry jelia.tex Action Logic and Pure Induction man.tex Temporal Structures pp2.tex Teams Can See Pomsets am4.tex Enriched Categories and the Floyd-Warshall Connection iowatr.tex Dynamic Algebras as a well-behaved fragment of Relation Algebras ijpp.tex Modelling Concurrency with Partial Orders ----------------------------------------------------------------------- ABSTRACTS casthes.tex On the Specification of Concurrent Systems Ross Casley Ph.D. Thesis, January, 1991 In models of concurrent processes constraints on the order of events are often represented by partial orders, and schedules of events are then defined using an algebra of standard operations such as sequential and parallel composition. In this dissertation the notion of partial order is replaced by that of a set with a metric which takes values in a given ordered monoid. Partial orders are the simple case of a monoid whose two elements represent the presence or absence of a constraint. An ordered monoid can be seen as a monoidal category, and schedules based on it are categories enriched in the monoid. Algebraic operations on schedules can then be defined as constructions in the category of schedules. These definitions rely on certain properties of a category of schedules, such as closure and completeness. To simplify proofs of these properties, two constructions are defined. The first creates a category of unlabeled schedules from a system of constraints. The second adds labels to unlabeled schedules. Many categories of interest can be constructed from simple categories using these two methods. The main results of the dissertation derive the required properties of categories so constructed from similar, more easily verified properties of the base categories. Several notions of timing constraint can be viewed in a uniform way in this framework. An example is the Gaifman-Pratt system, essentially the partial order model with additional specification as to whether two events may occur simultaneously. It corresponds to a monoid whose three elements represent strict precedence, lax precedence (simultaneity is permitted), and absence of constraint. Real-valued timing constraints correspond to the additive monoid of the real numbers. es.tex Event Spaces and their Linear Logic V. Pratt Boolean logic treats disjunction and conjunction symmetrically and algebraically. The corresponding operations for computation are respectively nondeterminism (choice) and concurrency. Petri nets treat these symmetrically but not algebraically, while event structures treat them algebraically but not symmetrically. Here we achieve both via the notion of an event space as a poset with all nonempty joins representing concurrences and a top representing the unreachable event. The symmetry is with the dual notion of state space, a poset with all nonempty meets representing choices and a bottom representing the start state. The algebra is that of a parallel programming language expanded to the language of linear logic, Girard's axiomatization of which is satisfied by the event space interpretation of this language. Event spaces resemble vector spaces in distinguishing tensor product from direct product and in being isomorphic to their double dual, but differ from them in distinguishing direct product from direct sum and tensor product from tensor sum. catl.tex Concurrent Automata and Their Logic V. Pratt Superseded by es.tex A concurrent automaton is a poset with a top (the global initial state) and all nonempty sups (the local initial states). A schedule is defined identically. These form dually isomorphic categories Aut and Sched admitting universally definable operations constituting a concurrent programming language, and additional operations constituting a linear logic of concurrency in which $!a$ and $?a$ are respectively a free choice automaton and a free concert schedule. The linear theory Th(CSLat) of complete semilattices strictly extends Th(Aut) with $\query a=\bang a$, an unwanted isomorphism of free and cofree semilattices (both being Boolean algebras) found only in CSLat. Both theories contain such howlers as 0=1. Intersection with classical logic (multiplication by 2) removes the howlers, but not usefully so for CSLat, and moreover $\query a=\bang a$ remains. The self-duality of these categories permits a non-categorical account requiring only elementary lattice theory. cg.tex Modeling Concurrency with Geometry V. Pratt To appear in POPL-91. Branching time and causality find their respective homes in the Birkhoff-dual models of automata and schedules. This creates a puzzle: if the duality is supposed to make the models completely equivalent then why does each phenomenon have a preferred side? We identify dimension as the culprit: 1-dimensional automata are skeletons permitting only interleaving concurrency, true n-fold concurrency resides in transitions of dimension n. The Birkhoff dual of a poset then becomes a simply-connected space. We distinguish Birkhoff duality from Stone duality and treat the former in detail from a concurrency perspective. We introduce true nondeterminism and define it as monoidal homotopy; from this perspective nondeterminism in ordinary automata arises from forking and joining creating nontrivial homotopy. We propose a formal definition of higher dimensional automaton as an n-complex or n-category, whose two essential axioms are associativity of concatenation within dimension and an interchange principle between dimensions. jelia.tex Action Logic and Pure Induction V. Pratt To appear in Proceedings of JELIA-90, European Workshop on Logics in AI (ed. J. van Benthem and Jan Eijck), held Amsterdam, Sept. 1990 In Floyd-Hoare logic programs are dynamic while assertions are static (hold at states). In action logic the two notions become one, with programs viewed as on-the-fly assertions whose truth is evaluated along intervals instead of at states. Action logic is an equational theory ACT conservatively extending the equational theory REG of regular expressions with operations preimplication a -> b (HAD a THEN b) and postimplication b <- a (b IF-EVER a). Unlike REG, ACT is finitely based, makes a* reflexive transitive closure, and has an equivalent Hilbert system. The crucial axiom is that of pure induction, (a -> a)* = a -> a. man.tex Temporal Structures R. Casley, R. Crew, J. Meseguer, V. Pratt To appear in Mathematical Structures in Computer Science, inaugural issue, 1990. Revision of proceedings version in Category Theory and Computer Science, LNCS 389, Manchester, 1989. Formerly called "Dynamic Types." We combine the principles of the Floyd-Warshall-Kleene algorithm, enriched categories, and Birkhoff arithmetic, to yield a useful class of algebras of transitive vertex-labeled spaces. The motivating application is a uniform theory of abstract or parametrized time in which to any given notion of time there corresponds an algebra of concurrent behaviors and their operations, always the same operations but interpreted automatically and appropriately for that notion of time. An interesting side application is a language for succinctly naming a wide range of datatypes. pp2.tex Teams Can See Pomsets G. Plotkin and V. Pratt Draft in preparation Strings may serve as both specifications and observations of behavior. However partial strings or pomsets, superior to strings in certain respects for the representation of concurrent behavior, are provably unobservable and hence apparently suitable only for specifying behavior. The proof however tacitly assumes that observers are isolated individuals. We show that observations by a cooperating team of sequential observers agreeing on *what* happened but not *when* can distinguish all pomsets. The resolving power of a finite team increases strictly with its size k, permitting it to distinguish all pomsets of dimension (not width) k but not all of k+1. These results extend to observation of augment closed processes. As expected we depend on the now standard technique of refinement of atomic events to complex events; what is not expected is that their complexity need be only that of nondeterminism, in that we refine one atomic event to a set of alternative atomic events, not to a set of sequences. am4.tex Enriched Categories and the Floyd-Warshall Connection V. Pratt Proceedings, AMAST-88 We give a correspondence between enriched categories and the Gauss-Kleene-Floyd-Warshall connection familiar to computer scientists. This correspondence shows this generalization of categories to be a close cousin to the generalization of transitive closure algorithms. Via this connection we may bring categorical and 2-categorical constructions into an active but algebraically impoverished arena presently served only by semiring constructions. We illustrate these techniques by applying them to Birkoff's poset arithmetic, interpretable as an algebra of ``true concurrency.'' iowatr.tex Dynamic Algebras as a well-behaved fragment of Relation Algebras V. Pratt Algebraic Logic and Universal Algebra in Computer Science, LNCS 425, ed. C.H. Bergman, R.D. Maddux, D.L. Pigozzi, Springer-Verlag, 1990. The varieties RA of relation algebras and DA of dynamic algebras are similar with regard to definitional capacity, admitting essentially the same equational definitions of converse and star. They differ with regard to completeness and decidability. The RA definitions that are incomplete with respect to representable relation algebras, when expressed in their DA form are complete with respect to representable dynamic algebras. Moreover, whereas the theory of RA is undecidable, that of DA is decidable in exponential time. These results follow from representability of the free intensional dynamic algebras. ijpp.tex Modelling Concurrency with Partial Orders V. Pratt International Journal of Parallel Programming, 15:1, 33-71, Feb. 1986. Concurrency has been expressed variously in terms of formal languages (typically via the shuffle operator), partial orders, and temporal logic, inter alia. In this paper we extract from these three approaches a single hybrid approach having a rich language that mixes algebra and logic and having a natural class of models of concurrent processes. The heart of the approach is a notion of partial string derived from the view of a string as a linearly ordered multiset by relaxing the linearity constraint, thereby permitting partially ordered multisets or pomsets. Just as sets of strings form languages, so do sets of pomsets form processes. We introduce a number of operations useful for specifying concurrent processes and demonstrate their utility on some basic examples. Although none of the operations is particularly oriented to nets it is nevertheless possible to use them to express processes constructed as a net of subprocesses, and more generally as a system consisting of components. The general benefits of the approach are that it is conceptually straightforward, involves fewer artificial constructs than many competing models of concurrency, yet is applicable to a considerably wider range of types of systems, including systems with buses and ethernets, analog systems, and real-time systems.

1 0

Program of MWPL
by mwpl＠Concour.cs.Concordia.CA 25 Apr '91

25 Apr '91

Program of the Montreal Workshop on Programming Languages -Algebraic and Logical Approaches in Programming Languages- April 29-30, 1991 Montreal Organized by the Montreal Programming Languages Group. In cooperation with the Montreal Interuniversity Category Theory-Logic Seminar, the Queen's Workshop on Programming Languages, and the McMaster International Workshops on Programming Languages. Supported by the Center for Pattern Recognition and Machine Intelligence of Montreal and the Ministere d'enseignement superieure et recherche de Quebec under the Quebec-Ontario Cooperation Program. There is no registration charge. Tuesday lunch will be served in the Workshop with a reasonable charge, as well as a Monday night cash-bar reception. WORKSHOP LOCATION: Faculty Club 7th Floor Hall Building Concordia University 1455 boul. de Maisonneuve Ouest Montreal, Quebec WORKSHOP TIME: 1:00PM Monday, April 29 to 5:10PM Tuesday, April 30. PROGRAM: All events, including lectures, reception (Monday), coffee, breakfast (Tuesday) and lunch (Tuesday), will take place in the Faculty Club. Monday (April 29) Pre-Workshop Departmental Open Seminar: 11:00 AM Dominique Sotteau (U. Paris-Sud & CNRS) "Embeddings of Interconnection Networks - The Graph Embedding Problem" Formal Program of MWPL ---------------------- 1:00 PM Opening Address Keynote Lecture Maurice Nivat (U. Paris VII) "Tree Languages" 2:00 PM D. Therien (McGill U.) "Regular Languages and Parallel Computation" 2:40 PM coffee 3:00 PM A. Podelski (DEC - Paris Lab) "The Logic, Inheritance, Functional and Equational Language - LIFE" 3:40 PM M. Okada (Concordia U.) "Executable Higher Order Algebraic Specification Languages" 4:10 PM break 4:20 PM D. Craigen and M. Saaltink (Odyssey Research, Ottawa) "Simple Type Theory in EVES" 4:50 PM P. J. Scott (U. Ottawa) "Uniqueness Conditions for Typed Functional Languages" 5:30 PM break 5:40 PM G. Butler (U. Sydney) "Cayley: A Language for Computation with Algebraic Structures" 6:10 PM G. Pottinger (Odyssey Research, Ithaca, NY) "Defining Unification for Descriptions of Lambda-terms" 6:40 PM Workshop Reception (light meal and cash bar) 8:30 PM Committee Meeting Tuesday (April 30) 8:30 AM coffee and doughnuts 9:10 AM Keynote lecture J. Lambek (McGill U.) "Least Fixpoints in Cartesian Closed Categories" 10:10 AM J. Zucker (McMaster U.) "Application of Intensional Logic to Program Semantics" 10:50 AM break 11:00 AM P. Panangaden (McGill U.) "Semantic Foundations of Concurrent Constraint Programming" 11:40 AM H. Mili (U. Quebec - Montreal) "Constraints in Object-Oriented Programming" 12:10 PM Workshop Lunch 2:00 PM Keynote Lecture R. D. Tennent (Queen's U.) "Possible World Semantics for Algol-like Programming Languages" 3:00 PM M. Barr (McGill U.) "Terminal Coalgebras in Well-Founded Set Theory" 3:40 PM J. Seldin (Concordia U.) "Excluded Middle Without Definite Descriptions in the Theory of Constructions" End of Formal Program of MWPL Post-Workshop Departmental Open Seminar: 4:10 PM Maurice Nivat (U. Paris VII) "Mathematics of Tiling Games" ORGANIZING COMMITTEE: M. Barr (McGill U.) P. Grogono (Concordia U.) B. Hodgson (U. Laval) P. Lauer (McMaster U.) H. Mili (UQAM) M. Nivat (U. Paris VII, visiting Concordia U.) M. Okada (Concordia U.)(chair) P. Panangaden (McGill U.) P. J. Scott (U. Ottawa) R. Seely (McGill U.) J. Seldin (Concordia U.) R. D. Tennent (Queen's U.) For further information, send e-mail to mwpl(a)concour.cs.concordia.ca or write to MWPL, c/o Dr. M. Okada Department of Computer Science Concordia University 1455 boul. de Maisonnneuve Ouest Montreal, Quebec H3G 1M8

1 0

Categorical view of loop invariants
by C Barry Jay 24 Apr '91

24 Apr '91

Program loops have a very simple categorical interpretation, as loop diagrams, i.e. as diagrams with one object C and one morphism f, necessarily an endomorphism of C. -- / \ | | | \/ | f | C | | | \ / -- Of course, the limit of the loop is its fixpoints. The colimit, however, is even more interesting. A cocone for the diagram is a morphism g:C-->Q such that f;g = g. That is, an *invariant* for the loop. Thus the colimit is the universal invariant of the loop. Definition A loop *converges* if it has an object of invariants Inv(f) which is also an object of fixpoints such that the canonical composite Inv(f) --> C --> Inv(f) is the identity. This property captures the desirable property of a loop that its iteration approaches a fixpoint. The simplest way to achieve this is if the loop always terminates after a finite number of steps. While such *termination* is equivalent to convergence in the category of Sets, the topological nature of domain theory allows convergence without termination. There are two technical reports available which exploit such loops. Fixpoint and loop constructions as colimits and Tail recursion via universal invariants The first shows how to interpret while-loops in domains, and give termination conditions. The second gives a categorical account of tail recursion, and establishes conditions under which a tail recursive characterisation of finite lists is equivalent to the usual intial algera construction. Copies of the latex code for either paper can be obtained by e-mail request (sorry - no ftp here yet!). Please specify if you need a copy of Paul Taylor's diagrams package: diagrams3. Barry Jay

1 0

Categories of separated presheaves
by dbenson＠yoda.eecs.wsu.edu 23 Apr '91

23 Apr '91

Let E be the category of presheaves on space X and S the category of sheaves on the same space, clearly the category of separated presheaves on X, call it P, is between E and F. ?In more detail, P is the full subcategory of E determined by the separated presheaves on X.? I suppose that P is not a topos in general, but I am wondering if anyone knows of a nice characterization of it, or indeed whether there are any papers on this topic. Neither Barr and Wells' TTT nor Peter Johnstone's book says enough about separated presheaves for my current explorations of the connections between sheaf-theoretic ideas and some questions in software systems theory that I am working on with Rakesh Dubey. Any suggestions will be most appreciated. Thanks, David

2 1

separated presheaves
by koslowj＠math.ksu.edu 23 Apr '91

23 Apr '91

David B. Benson asked for a characterization of the category P of presheaves on a space X, which is sandwiched between the categories S of sheaves and E of presheaves. P is just the epi-reflective hull of S in E. (All epis in E are regular.) J"urgen Koslowski Department of Mathematics Kansas State University Manhattan, KS 66502 koslowj(a)math.ksu.edu

1 0

set theory question
by barr＠triples.Math.McGill.CA 23 Apr '91

23 Apr '91

Dear Bob: Here is a distillation of the answers I got from several people on my question on set theory. What I was asking for (eventually) is called a weakly inaccessible cardinal. What Dan Leivant constructed was actually not regular either (Les Nelson). If it was it was inaccessible. There are models of set theory with no cardinals that satisfy the GCH and probably (Blass wasn't certain) had no weakly inaccessibles either. Oddly enough those models were constructed using some large cardinals. No stranger, actually, than Freyd's construction of models lacking choice that start from ZFC and build an elementary topos lacking choice and then a model of set theory also lacking choice. So the upshot is that what I wanted is indeed weaker than the existence of inaccessibles, but still fairly strong. Fortunately, it is only a peripheral to what I was doing. It clarified a side issue that had no effect on the main result, which is that you certainly don't have to delve into the mysteries of non-well-founded sets in order to show that the coalgebras for an inaccessibly accessible functor have a terminal model no larger than the inaccessible provided the functor takes smaller cardinals to smaller cardinals. Michael

1 0

question on set theory
by barr＠triples.Math.McGill.CA 20 Apr '91

20 Apr '91

This question is not category theory, but I am sure there are people on the net who know much more set theory than me. If you assume the generalized continuum hypothesis, it is evident that any power cardinal $\kappa$ has the property that $\lambda < \kappa$ implies $2^\lambda <= \kappa$. Otherwise, that property is obvious to me only for inaccessible cardinals. My question is whether there are a large class of cardinals for which that is true even without the GCH? Michael

3 5

beth in TeX
by Paul Taylor 17 Apr '91

17 Apr '91

You can do \beth in TeX, but you need the AMS symbol fonts (msym10 or msbm10) and associated macros (mssymb.tex or some similar name). As a general comment (since I frequently get complaints about mssymb.tex and a4.sty in relation to my diagram macros) if your local TeX system doesn't have these things then you should COMPLAIN LOUDLY to your system manager as they are part of the standard TeX distribution. The same applies if you're still running TeX version 2.993 (I've even seen systems with 2.0 still!): 3.1 is current. TeX is public domain and available from several fileservers; there is really no excuse for having defective systems, especially if you're a unix user.

1 0