Guide to Papers on Chu Spaces

This page contains the abstracts of papers about or leading up to couples (Chu spaces) written by current or former members of the Stanford Concurrency Group, namely Ross Casley, Roger Crew, Rob van Glabbeek, Vineet Gupta, Dominic Hughes, Jose Meseguer, Gordon Plotkin, and Vaughan Pratt. For papers by this group on other topics, see the file abstracts.html which contains their abstracts in reverse chronological order.

Starting from the following list of titles, clicking on the title takes you to the abstract and citation information. From there, clicking again on the title delivers the full paper as a PDF file.

Where to begin? This depends on whether your preferred point of view is recent perspective, mathematical, computational, philosophical, or hands-on.

INTRODUCTORY: Visit http://chu.stanford.edu/ (unless you just arrived here from there). There you have the choice of using the Chu calculator to experiment with actual couples, or of staying there and reading an elementary introduction to the subject without having to click on anything. Or both: you can move between the two using your browser's Back and Forward buttons.

For a comprehensive perspective on applications of Chu spaces to concurrency, see
Transition and Cancellation in Concurrency and Branching Time. This relatively long (40 pages) paper extends
Orthocurrence as Both Interaction and Observation (IJCAI'01 Workshop on Spatial and Temporal Reasoning) and
Higher Dimensional Automata Revisited (MSCS Aug. 2000, 525-548) while tying many process algebra ideas into one coherent framework.
Another recent paper is from CONCUR 2002,
Event-State Duality: The Enriched Case which ties up one more loose end originating with categorical enrichment and
Temporal Structures (1989).

MATH: For a more mathematical perspective, start with
Chu spaces: Course notes for the School in Category Theory and Applications.

CS: For the computational perspective, we recommend again
Transition and Cancellation in Concurrency and Branching Time. Earlier versions of some of these ideas but with a considerably narrower view are Chu Spaces and their Interpretation as Concurrent Objects or the longer
Chu Spaces: A Model of Concurrency, Vineet Gupta's thesis.

PHILOSOPHY: Philosophers may find
Rational Mechanics and Natural Mathematics of interest.

INTERACTIVE: For hands-on experience with Chu spaces, try
Chu Spaces Live, a web-based tutorial-cum-calculator for Chu spaces.

The papers are organized into four categories: Introductory, Technical, Applications, and Prehistory.

1. Introductory.

(In recommended order of reading)
Chu spaces: Course notes for the School in Category Theory and Applications
Notes for seven lectures at the categories summer school in Coimbra in 1999.
Chu spaces as a semantic bridge between linear logic and mathematics
The linear logic connection, presented at Linear Logic '96 (Tokyo)
Chu Spaces: Complementarity and Uncertainty in Rational Mechanics"
Notes for five lectures at the TEMPUS summer school in Budapest in 1994.
Chu Spaces and their Interpretation as Concurrent Objects
Overview of concurrency aspects of Chu spaces. In LNCS 1000.
Chu Spaces Live
A web-based tutorial-cum-calculator for Chu spaces.
Chu spaces from the representational viewpoint
Parikhfest paper, 1997.
Types as Processes, via Chu spaces
EXPRESS'97 paper.

2. Applications.

Concurrency
Event-State Duality: The Enriched Case
Transition and Cancellation in Concurrency and Branching Time
Orthocurrence as Both Interaction and Observation
Higher Dimensional Automata Revisited
Chu Spaces and their Interpretation as Concurrent Objects
Configuration Structures
Gates Accept Concurrent Behavior
Chu Spaces: A Model of Concurrency
Concurrent Kripke Structures
Time and Information in Sequential and Concurrent Computation
Mathematics
The Stone Gamut: A Coordinatization of Mathematics
Linear logic
Chu spaces as a semantic bridge between linear logic and mathematics
Broadening the Denotational Semantics of Linear Logic(Early conference version of the preceding "semantic bridge" paper)
Linear Logic complements Classical Logic
Physics
Linear Logic for Generalized Quantum Mechanics
Chu Spaces: Automata with Quantum Aspects
Philosophy
Rational Mechanics and Natural Mathematics

3. Technical.


"Full completeness of multiplicative linear logic for Chu spaces
Establishes a bijection between syntactic and semantic proofs for multiplicative linear logic.
"Towards full completeness for the linear logic of Chu spaces
Establishes a bijection between syntactic and semantic proofs for multiplicative linear logic restricted to two occurrences per variable.
On the Representation of Finite Abelian Groups as Chu Spaces
Represents finite abelian groups in terms of their characters.
Notes on the Chu construction and Recursion
Shows that although recursive equations cannot be solved when the language includes linear logic's par connective, they can be solved when the operations are circuit-definable.
"Notes on Event Structures and Chu"
A preliminary study for Plotkin's LICS'95 paper with van Glabbeek.
"Shorter proof of universality of Chu spaces"
Another proof that the category of k-ary relational structures, for any ordinal k, embeds fully and concretely in the category of Chu spaces over 2^k.
"Chu realizes all small concrete categories"
"The Second Calculus of Binary Relations"
Chu spaces as a form of relation algebra.

4. Prehistory.

Modeling Concurrency with Partial Orders"
Develops an algebra of partially ordered multisets as a concurrent programming language.
"Temporal Structures"
Defines time as an ordered monoid, more generally a monoidal category, and defines processes whose schedules use that notion of time as categories enriched in that monoidal structure.
"Modeling Concurrency with Geometry"
Defines a concurrent process to be a complex of cells whose dimension corresponds to the number of concurrently executing processes making up that cell.
"Event Spaces and Their Linear Logic"
Defines a self-dual category of schedules, dual to a category of automata, as a precursor to Chu spaces.
"The Duality of Time and Information"
An introduction to event spaces starting from nonconcurrent nonbranching programs defined as linear orders, which by themselves form a self-dual category.


1. Introductory

Chu spaces: Course notes for the School in Category Theory and Applications

@Misc( Pr99a, Author="Pratt, V.R.", Title="Chu Spaces", Comment="Course notes for the School in Category Theory and Applications", Address="Coimbra, Portugal", Month=July, Year=1999) These are the notes for the course on Chu Spaces for the School in Category Theory and Applications, Coimbra, Portugal, July 13-17, 1999. Chapter 1 introduces the basic notions, gives examples of use of Chu spaces, points out some interference properties, and proves that functions between Chu spaces are continuous if and only if they are homomorphisms. Chapter 2 realizes a variety of mathematical objects as Chu spaces, including posets, topological spaces, semilattices, distributive lattices, and vector spaces. Chapter 3 gives several senses in which Chu spaces are universal objects of mathematics. Chapter 4 interprets operations of linear logic and process algebra over Chu spaces. Chapter 5 studies linear logic from an axiomatic viewpoint, with emphasis on the multiplicative fragment. Chapter 6 develops several notions of naturality as a semantic criterion for canonical transformations. Chapter 7 proves full completeness of the multiplicative linear logic of Chu spaces

Chu Spaces Live ....
A web-based (Java) tutorial-cum-calculator for operating on Chu spaces with the operations of both process algebra and linear logic (which overlap, notably at plus and times). Caveat: your browser must support the current version of Java (1.1), which Javasoft and Internet Explorer do but Netscape unfortunately has fallen behind and currently only beta prereleases of Netscape (4.05) can run Chu Spaces Live.

Chu spaces from the representational viewpoint PDF version.... HTML version

@InCollection( Pr97b, Author="Pratt, V.R.", Title="Chu spaces from the representational viewpoint", Booktitle="Parikh Festschrift", Year=1997) We give an elementary introduction to Chu spaces. The perspective taken views their elements as represented by words of a fixed length over some alphabet. This perspective dualizes the alternative view of Chu spaces as generalized topological spaces, and has the advantage of substituting the intuitions of formal language theory for those of topology.

Types as Processes, via Chu spaces

@Article( Pr94, Author="Pratt, V.R.", Title="Types as Processes, via Chu spaces", Booktitle="EXRESS'97 Proceedings", Year=1997) We match up types and processes by putting values in correspondence with events, coproduct with (noninteracting) parallel composition, and tensor product with orthocurrence. We then bring types and processes into closer correspondence by broadening and unifying the semantics of both using Chu spaces and their transformational logic. Beyond this point the connection appears to break down; we pose the question of whether the failures of the correspondence are intrinsic or cultural.

Chu Spaces: Complementarity and Uncertainty in Rational Mechanics

@TechReport( Pr94, Author="Pratt, V.R.", Title="Chu Spaces: Complementarity and Uncertainty in Rational Mechanics", Note="Course notes, TEMPUS summer school, 35pp", Address="Budapest", Year=1994) Notes for five lectures given at the Tempus summer school, Budapest, July 1994. Topics covered: Introduction to Chu spaces. Behavior: from event structures to rational mechanics. Algebra: from linear logic to process algebra. Relational structures. Heisenberg uncertainty in Chu spaces.

Chu Spaces and their Interpretation as Concurrent Objects

@InCollection( Pr95d, Author= "Pratt, V.R.", Title= "Chu Spaces and their Interpretation as Concurrent Objects", Booktitle="Computer Science Today: Recent Trends and Developments", Series=LNCS, Volume=1000, Pages="392-405", Editor="van Leeuwen, J.", Publisher="Springer-Verlag", Year="1995") A Chu space is a binary relation =| from a set A to an antiset X defined as a set which transforms via converse functions. Chu spaces admit a great many interpretations by virtue of realizing all small concrete categories and most large ones arising in mathematical and computational practice. Of particular interest for computer science is their interpretation as computational processes, which takes A to be a schedule of events distributed in time, X to be an automaton of states forming an information system in the sense of Scott, and the pairs (a,x) in the =| relation to be the individual transcriptions of the making of history. The traditional homogeneous binary relations of transition on X and precedence on A are recovered as respectively the right and left residuals of the heterogeneous binary relation =| with itself. The natural algebra of Chu spaces is that of linear logic, made a process algebra by the process interpretation.


2. Applications

Concurrency

Event-State Duality: The Enriched Case

@InProceedings( Pr02c, Author="Pratt, V.R.", Title="Event-State Duality: the Enriched Case", Booktitle="Proc. CONCUR'02", Address="Brno", Month=Aug, Year=2002) Enriched categories have been applied in the past to both event-oriented true concurrency models and state-oriented information systems, with no evident relationship between the two. Ordinary Chu spaces expose a natural duality between partially ordered temporal spaces (pomsets, event structures), and partially ordered information systems. Barr and Chu's original definition of Chu spaces however was for the general V-enriched case, with ordinary Chu spaces arising for V = Set (equivalently V = Pos at least for biextensional Chu spaces). We extend time-information duality to the general enriched case, and apply it to put on a common footing event structures, higher-dimensional automata (HDAs), a cancellation-based approach to branching time, and other models treatable by enriching either event (temporal) space or state (information) space.

Transition and Cancellation in Concurrency and Branching Time

@Article( Pr02a, Author="Pratt, V.R.", Title="Transition and Cancellation in Concurrency and Branching Time", Journal="Math. Structures in Comp. Sci.", Volume=13, Number=4, Pages="485-529", Month=Aug, Year=2003) We review the conceptual development of (true) concurrency and branching time starting from Petri nets and proceeding via Mazurkiewicz traces, pomsets, bisimulation, and event structures up to higher dimensional automata (HDAs), whose acyclic case may be identified with triadic event structures and triadic Chu spaces. Acyclic HDAs may be understood as the extension of Boolean logic with a third truth value _- expressing transition. We prove the necessity of such a third value under mild assumptions about the nature of observable events, and show that the expansion of any complete Boolean basis L to L_T with a third literal hat(a) expressing a = _- forms an expressively complete basis for the representation of acyclic HDAs. The main contribution is a new event state X of cancellation, sibling to _-, serving to distinguish a(b+c) from ab+ac while simplifying the extensional definitions of termination v' A and sequence AB. We show that every HDAX (acyclic HDA with X) is representable in the expansion of L_T to L_{TX} with a fourth literal /a expressing a=X.

Orthocurrence as both Interaction and Observation

@Misc( Pr01b, Author="Pratt, V.R.", Title="Orthocurrence as both Interaction and Observation", Howpublished="Proc. Workshop on Spatial and Temporal Reasoning (ed. R.~Rodriguez and F.~Anger), IJCAI'01 (Invited paper)", Address=Seattle, Month=Aug, Year=2001) Orthocurrence or tensor product A*B of systems A and B can be understood symmetrically as an interaction operator expressing a form of conjunction of state predicates, or asymmetrically as one of two information channels: either A -o B' as a system consisting of A observing states of B (equivalently, conveying information about the states of B to A), or B -o A' for the same thing in the other direction. We show how the notion of Chu space or couple arises as a natural corollary of this point of view. We conclude with a history of orthocurrence.

Higher Dimensional Automata Revisited

@Article( Pr00a, Author="Pratt, V.R.", Title="Higher dimensional automata revisited", Journal="Math. Structures in Comp. Sci., Special Issue on Geometry and Concurrency (Invited paper)", Volume=10, Pages="525--548", Year=2000) The dual of a true concurrency schedule appears to be a false concurrency automaton, a paradox we resolved in a previous paper by extending the latter to higher dimensions. This extension may be formalized via such discrete geometries as n-categories, simplicial complexes, cubical complexes, and Chu spaces. We advocate the last as having a clear notion of event, a well-defined process algebra uniformly extending that for event structures, and ease of extension beyond the basic before-during-after analysis.

Configuration Structures

@InProceedings( vGP, Author="Van Glabbeek, R. and Plotkin, G.", Title="Configuration Structures", Booktitle="Logic in Computer Science", Pages="199-209", Month="Jun", Publisher="IEEE Computer Society", Year="1995") Configuration structures provide a model of concurrency generalising the families of configurations of event structures. They can be considered logically, as classes of propositional models; then sub-classes can be axiomatised by formulae of simple prescribed forms. Several equivalence relations for event structures are generalised to configuration structures, and also to general Petri nets. Every configuration structure is shown to be ST-bisimulation equivalent to a prime event structure with binary conflict; this fails for the tighter history preserving bisimulation. Finally, Petri nets without self-loops under the collective token interpretation are shown behaviourally equivalent to configuration structures, in the sense that there are translations in both directions respecting history preserving bisimulation. This fails for nets with self-loops.

Gates Accept Concurrent Behavior

@InProceedings( GP93, Author="Gupta, V. and Pratt, V.R.", Title="Gates Accept Concurrent Behavior", Booktitle="Proc. 34th Ann. IEEE Symp. on Foundations of Comp. Sci.", Pages="62-71", Month=Nov, Year=1993) We represent concurrent processes as Boolean propositions or gates, cast in the role of acceptors of concurrent behavior. This properly extends other mainstream representations of concurrent behavior such as event structures, yet is defined more simply. It admits an intrinsic notion of duality that permits processes to be viewed as either schedules or automata. Its algebraic structure is essentially that of linear logic, with its morphisms being consequence-preserving renamings of propositions, and with its operations forming the core of a natural concurrent programming language.

Chu Spaces: A Model of Concurrency

@PhDThesis( Gup94, Author="Vineet Gupta", Title="Chu Spaces: A Model of Concurrency", School="Stanford University", Month=Sep, Year=1994) A Chu space is a binary relation between two sets. In this thesis we show that Chu spaces form a non-interleaving model of concurrency which extends event structures while endowing them with an algebraic structure whose natural logic is linear logic.

We provide several equivalent definitions of Chu spaces, including two pictorial representations. Chu spaces represent processes as automata or schedules, and Chu duality gives a simple way of converting between schedules and automata. We show that Chu spaces can represent various concurrency concepts like conflict, temporal precedence and internal and external choice, and they distinguish between causing and enabling events.

We present a process algebra for Chu spaces including the standard combinators like parallel composition, sequential composition, choice, interaction, restriction, and show that the various operational identities between these hold for Chu spaces. The solution of recursive domain equations is possible for most of these operations, giving us an expressive specification and programming language. We define a history preserving equivalence between Chu spaces, and show that it preserves the causal structure of a process.

Concurrent Kripke Structures

@InProceedings( Gup93, Author="Gupta, V.", Title="Concurrent Kripke Structures", Booktitle="Proceedings of the North American Process Algebra Workshop, Cornell CS-TR-93-1369", Month=Aug, Year=1993) We consider a class of Kripke Structures in which the atomic propositions are events. This enables us to represent worlds as sets of events and the transition and satisfaction relations of Kripke structures as the subset and membership relations on sets. We use this class, called event Kripke structures, to model concurrency. The obvious semantics for these structures is a true concurrency semantics. We show how several aspects of concurrency can be easily defined, and in addition get distinctions between causality and enabling, and choice and nondeterminism. We define a duality for event Kripke structures, and show how this duality enables us to convert between imperative and declarative views of programs, by treating states and events on the same footing. We provide pictorial representations of both these views, each encoding all the information to convert to the other.

We define a process algebra of event Kripke structures, showing how to combine them in the usual ways---parallel composition, sequential composition, choice, interaction and iteration. Various properties of these connectives like associativity and distributivity are proved. We then show that Winskel's event structures can be embedded in the class of event Kripke structures, and define partial synchronous composition, the primary connective for event structures, for event Kripke structures, and show its equivalence to Winskel's definition.

Time and Information in Sequential and Concurrent Computation

@InProceedings( Pr94c, Author="Pratt, V.R.", Title="Time and Information in Sequential and Concurrent Computation", Booktitle="Proc. Theory and Practice of Parallel Programming (TPPP'94)", Address="Sendai, Japan", Month=Nov, Pages="1-24". Year=1994) Time can be understood as dual to information in extant models of both sequential and concurrent computation. The basis for this duality is phase space, coordinatized by time and information, whose axes are oriented respectively horizontally and vertically. We fit various basic phenomena of computation, and of behavior in general, to the phase space perspective. The extant two-dimensional logics of sequential behavior, the van Glabbeek map of branching time and true concurrency, event-state duality and schedule-automaton duality, and Chu spaces, all fit the phase space perspective well, in every case confirming our choice of orientation.

Mathematics

The Stone Gamut: A Coordinatization of Mathematics

@InProceedings( Pr95c, Author="Pratt, V.R.", Title="The {S}tone Gamut: A Coordinatization of Mathematics", Booktitle="Logic in Computer Science", Pages="444-454", Month="June", Publisher="IEEE Computer Society", Year="1995") We give a uniform representation of the objects of mathematical practice as Chu spaces, forming a concrete self-dual bicomplete closed category and hence a constructive model of linear logic. This representation distributes mathematics over a two-dimensional space we call the Stone gamut. The Stone gamut is coordinatized horizontally by coherence, ranging from -1 for sets to 1 for complete atomic Boolean algebras (CABA's), and vertically by complexity of language. Complexity 0 contains only sets, CABA's, and the inconsistent empty set. Complexity 1 admits noninteracting set-CABA pairs. The entire Stone duality menagerie of partial distributive lattices enters at complexity 2. Groups, rings, fields, graphs, and categories have all entered by level 16, and every category of relational structures and their homomorphisms eventually appears. The key is the identification of continuous functions and homomorphisms, which puts Stone-Pontrjagin duality on a uniform basis by merging algebra and topology into a simple common framework.

Linear Logic

Note: The following three papers are listed in reverse chronological order, with each being a complete rewrite of and hence superseding the next.

Chu spaces as a semantic bridge between linear logic and mathematics

@Article( Pr98b, Author=Pratt, V.R.", Title="Chu spaces as a semantic bridge between linear logic and mathematics", Journal="TCS", Volume=294", Number=3, Pages="439-471", Month=Feb, Year=2003) The motivating role of linear logic is as a ``logic behind logic.'' We propose a sibling role for it as a logic of transformational mathematics via the self-dual category of Chu spaces, a generalization of topological spaces. These create a bridge between linear logic and mathematics by soundly interpreting linear logic while fully and concretely embedding a comprehensive range of concrete categories of mathematics. Our main goal is to treat each end of this bridge in expository detail. In addition we introduce the dialectic lambda-calculus, and show that dinaturality semantics is not fully complete for the Chu interpretation of linear logic.

Broadening the Denotational Semantics of Linear Logic

Broadening the denotational semantics of linear logic V.R. Pratt ENTCS proceedings of Linear Logic '96, Tokyo The proof-theoretic origins and specialized models of linear logic make it primarily operational in orientation. In contrast first-order logic treats the operational and denotational aspects of general mathematics quite evenhandedly. Here we show that linear logic has models of even broader denotational scope than those of first order logic, namely Chu spaces, the category of which Barr has observed to form a model of linear logic. We have previously argued that every category of n-ary relational structures embeds fully and concretely in the category of Chu spaces over 2^n. The main contributions of this paper are improvements to that argument, and an embedding of every small category in the category of Chu spaces via a symmetric variant of the Yoneda embedding.

Linear Logic complements Classical Logic

Linear Logic complements Classical Logic V.R. Pratt Preliminary proceedings, Linear Logic '96, Tokyo Classical logic enforces the separation of individuals and predicates, linear logic draws them together via interaction; these are not right-or-wrong alternatives but dual or complementary logics. Linear logic is an incomplete realization of this duality. While its completion is not essential for the development and maintenance of logic, it is crucial for its application. We outline the ``four-square'' program for completing the connection, whose corners are set, function, number, and arithmetic, and define ordinal Set, a bicomplete *equational* topos, meaning its canonical isomorphisms are identities, including associativity of product.

Physics

Linear Logic for Generalized Quantum Mechanics

This paper is really prehistory, in that it hints at Chu spaces only at the end, where it calls them partial distributive lattices.

@InProceedings( Pr93a, Author="Pratt, V.R.", Title="Linear Logic for Generalized Quantum Mechanics", Booktitle="Proc. Workshop on Physics and Computation (PhysComp'92)", Address="Dallas", Publisher="{IEEE}", Pages="166-180", Year=1993) Quantum logic is static, describing automata having uncertain states but no state transitions and no Heisenberg uncertainty tradeoff. We cast Girard's linear logic in the role of a dynamic quantum logic, regarded as an extension of quantum logic with time nonstandardly interpreted over a domain of linear automata and their dual linear schedules. In this extension the uncertainty tradeoff emerges via the ``structure veil.'' When VLSI shrinks to where quantum effects are felt, their computer-aided design systems may benefit from such logics of computational behavior having a strong connection to quantum mechanics.

Chu Spaces: Automata with Quantum Aspects

@InProceedings( Pr94b, Author="Pratt, V.R.", Title="Chu Spaces: Automata with Quantum Aspects", Booktitle="Proc. Workshop on Physics and Computation (PhysComp'94)", Pages="186-195", Address="Dallas", Publisher="{IEEE}", Year=1994) Chu spaces are a recently developed model of concurrent computation extending automata theory to express branching time and true concurrency. They exhibit in a primitive form the quantum mechanical phenomena of complementarity and uncertainty. The complementarity arises as the duality of information and time, automata and schedules, and states and events. Uncertainty arises when we define a measurement to be a morphism and notice that increasing structure in the observed object reduces clarity of observation. For Chu spaces this uncertainty can be calculated in an attractively simple way directly from its dimensions.

Philosophy

Rational Mechanics and Natural Mathematics

@InProceedings( Pr95a, Author="Pratt, V.R.", Title="Rational Mechanics and Natural Mathematics", Booktitle="TAPSOFT'95", Series=LNCS, Volume=915, Address="Aarhus, Denmark", Pages="108-122", Publisher="Springer-Verlag", Year=1995) Chu spaces have found applications in computer science, mathematics, and physics. They enjoy a useful categorical duality analogous to that of lattice theory and projective geometry. As natural mathematics Chu spaces borrow ideas from the natural sciences, particularly physics, while as rational mechanics they cast Hamiltonian mechanics in terms of the interaction of body and mind.

This paper addresses the chief stumbling block for Descartes' 17th-century philosophy of mind-body dualism, how can the fundamentally dissimilar mental and physical planes causally interact with each other? We apply Cartesian logic to reject not only divine intervention, preordained synchronization, and the eventual mass retreat to monism, but also an assumption Descartes himself somehow neglected to reject, that causal interaction within these planes is an easier problem than between. We use Chu spaces and residuation to derive all causal interaction, both between and within the two planes, from a uniform and algebraically rich theory of between-plane interaction alone. Lifting the two-valued Boolean logic of binary relations to the complex-valued fuzzy logic of quantum mechanics transforms residuation into a natural generalization of the inner product operation of a Hilbert space and demonstrates that this account of causal interaction is of essentially the same form as the Heisenberg-Schr"odinger quantum-mechanical solution to analogous problems of causal interaction in physics.


3. Technical Notes

On the Representation of Finite Abelian Groups as Chu Spaces

@Unpublished( Pr97d, Author="Pratt, V.R.", Title="On the Representation of Finite Abelian Groups as Chu Spaces", Comment="Draft Report", Month=Oct, Year=1997) We compare two representations of finite abelian groups as Chu spaces. The first represents the elements of any ternary relational structure as words on an 8-letter alphabet. The second is based on the group characters of abelian groups as the elements of the dual group.

Notes on the Chu construction and Recursion

@Unpublished( Plo93a, Author="Plotkin, G.D.", Title="Notes on the Chu construction and Recursion", Comment="Draft Report", Month=Aug, Year=1993) We consider two kinds of recursive equations in categories of the form Chu(K,x): type equations and value equations. Throughout it is assumed that K is monoidal closed, complete and co-complete.

Notes on Event Structures and Chu

@Unpublished( Plo93a, Author="Plotkin, G.D.", Title="Notes on Event Structures and Chu", Comment="Draft Report", Month=Aug, Year=1993) We consider the relation between event structures and Chu(Set,2), particularly the full subcategory Sys of set systems.

Shorter proof of universality of Chu spaces

@Note( Pr94b, Author="Vaughan Pratt", Title="Shorter proof of universality of Chu spaces", School="Stanford University", Month=Aug, Year=1994) We give a shorter proof of the result in section 5 of our MFPS'93 paper (scbr), that every k-ary relational structure is realizable as a Chu space.

Chu realizes all small concrete categories

V.R. Pratt Draft in preparation The category Chu is concretely universal for much of concrete mathematics; in particular it concretely represents or realizes all categories of relational structures and their homomorphisms, as well as all topological such. This note extends these results to all small concrete categories, equivalently all small subcategories of Set. The category C is realized in Chu(Set,K) where K is the disjoint union of the underlying sets of objects of C. Each object is realized as the normal Chu space (A,X) where X consists of all functions from A in C astricted to K.

The Second Calculus of Binary Relations

@InProceedings( Pr93b, Author="Pratt, V.R.", Title="The Second Calculus of Binary Relations", Booktitle="MFCS'93, Gda{\'n}sk", Pages="142-155", Address="Poland", Year=1993) We view the Chu space interpretation of linear logic as an alternative interpretation of the language of the Peirce calculus of binary relations. Chu spaces amount to K-valued binary relations, which for K=2^n we show generalize n-ary relational structures. We also exhibit a four-stage unique factorization system for Chu transforms that illuminates their operation.

Towards Full Completeness for the Linear Logic of Chu spaces (or)

@InProceedings( Pr97a, Author="Pratt, V.R.", Title="Towards Full Completeness of the Linear Logic of Chu Spaces", Booktitle="Electronic Notes in Theoretical Computer Science", Volume=6, Year=1997, Address="Pittsburgh", Year=1997, Note="URL: http://www.elsevier.nl/locate/entcs/volume6.html, 18 pages") We investigate the linear logic of Chu spaces as defined by its dinaturality semantics. For those formulas of multiplicative linear logic limited to at most two occurrences of each variable we prove full completeness of Girard's MIX-free axiomatization, namely that the cut-free proof-nets of such formulas are in a natural bijection with the dinatural elements of the corresponding functors.

Full Completeness of the Linear Logic of Chu Spaces

@InProceedings( DHPP, Author="Devarajan, H. and Hughes, D. and Plotkin, G. and Pratt, V.", Title="Full completeness of the multiplicative linear logic of Chu spaces", Booktitle="{\rm Proceedings $14^{th}$ Annual IEEE Symposium on} Logic in Computer Science, {\rm LICS'99, Trento, Italy, July 1999}", Editor="G. Longo", Month="July", Publisher="IEEE Computer Society Press", Year="1999", Note="Available at {\tt http://boole.stanford.edu/pub/fullchu.pdf}") We prove full completeness of multiplicative linear logic (MLL) without MIX under the Chu interpretation. In particular we show that the cut-free proofs of MLL theorems are in a natural bijection with the binary logical transformations of the corresponding operations on the category of Chu spaces on a two-letter alphabet.}


4. Prehistory

Modeling Concurrency with Partial Orders

@Article( Pr86, Author="Pratt, V.R.", Title="Modeling Concurrency with Partial Orders", Journal="Int. J. of Parallel Programming", Volume=15, Number=1, Pages="33-71", Month=Feb, Year=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.

Temporal Structures

@Article( CCMP, Author="Casley, R.T and Crew, R.F. and Meseguer, J. and Pratt, V.R.", Title="Temporal Structures", Journal="Math. Structures in Comp. Sci.", Volume=1, Number=2, Pages="179-213", Month=Jul, Year=1991) 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.

Modeling Concurrency with Geometry

@InProceedings( Pr91a, Author="Pratt, V.R.", Title="Modeling Concurrency with Geometry", Booktitle="Proc. 18th Ann. ACM Symposium on Principles of Programming Languages", Pages="311-322", Month=Jan, Year=1991) 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.

Event Spaces and Their Linear Logic

@InProceedings( Pr91b, Author="Pratt, V.R.", Title="Event Spaces and Their Linear Logic", Booktitle="AMAST'91: Algebraic Methodology and Software Technology", Publisher="Springer-Verlag", Series="Workshops in Computing", Pages="1-23", Address="Iowa City", Year=1992) 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 finite-dimensional 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.

The Duality of Time and Information

@InProceedings( Pr92e, Author="Pratt, V.R.", Title="The Duality of Time and Information", Booktitle="Proc. of CONCUR'92", Pages="237-253", Publisher="Springer-Verlag", Address="Stonybrook, New York", Month=Aug, Year=1992) The states of a computing system bear information and change time, while its events bear time and change information. We develop a primitive algebraic model of this duality of time and information for rigid local computation, or straightline code, in the absence of choice and concurrency, where time and information are linearly ordered. This shows the duality of computation to be more fundamental than the logic of computation for which choice is disjunction and concurrency conjunction.

To accommodate flexible distributed computing systems we then bring in choice and concurrency and pass to partially ordered time and information, the formal basis for this extension being Birkhoff-Stone dualtiy. A degree of freedom in how this is done permits a perfectly symmetric logic of computation amounting to Girard's full linear logic, which we view as the natural logic of computation when equal importance is attached to choice and concurrency.

We conclude with an assessment of the prospects for extending the duality to other organizations of time and information besides partial orders in order to accommodate real time, nonmonotonic logic, and automata that can forget, and speculate on the philosophical significance of the duality.