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.