Geometric logic, causality and event structures

Abstract

The conventional approach to causality is based on partial orders. Without additional structure, partial orders are only capable of expressing AND causality. In this paper we investigate a syntactic, or logical, approach to causality which allows other causal relationships, such as OR causality, to be expressed with equal facility. In earlier work, [3], we showed the benefits of this approach by giving a causal characterisation, in the finite case, of Milner's notion of confluence in CCS. This provides the justification for the more systematic study of causality, without finiteness restrictions, which appears here. We identify three general principles which a logic of causality should satisfy. These principles summarise some basic intuitions about events and causality. They lead us to geometric logic — the “logic of finite observations” — as a candidate for a logic of causality. We introduce the formalism of geometric automata based on this choice; a geometric automation is a set E together with a pair of endomorphisms of the free frame (locale) generated by E. Our main result is to show that Winskel's general event structures are a special case of geometric automata. This is analogous to the transition from topological data (sets of points) to algebraic structures (lattices of open subsets) in “pointless topology”, [6]. This result links our ideas on causality with Winskel's theory of events in computation; it provides a syntax for describing event structures and it opens the way to giving a causal interpretation of event structure phenomena. We show further that geometric automata give rise to domains of configurations which generalise the event domains of Winskel and Droste.