Observation algebras: Heyting algebra over coherence spaces
Paul Brunet
TL;DR
This work develops a framework of observation algebras built from down-closed subsets of coherence graphs to model partial observations in concurrent settings. It shows how these algebras form bounded distributive lattices and, with an added implication operator, Heyting algebras, with completeness results for tractable graph classes. Completeness is established for the bounded-distributive-lattice setting and, for Heyting structures, in particular under finite anti-neighborhoods and infinite-anticlique regimes via representation-theoretic approaches; a product construction then yields complete composite systems. The formalisation in Rocq underpins the rigorous development, and the product formalism enables scalable modeling of complex memory-like states, with insights into finite/infinite clique semantics and practical decidability considerations.
Abstract
In this report, we introduce observation algebras, constructed by considering the downclosed subsets of a coherence space ordered by reverse inclusion. These may be interpreted as specifications of sets of events via some predicates with some extra structure. We provide syntax for these algebras, as well as axiomatisations. We establish completeness of these axiomatisations in two cases: when the syntax is that of bounded distributive lattices (conjunction, disjunction, top, and bottom), and when the syntax also includes an implication operator (in the sense of Heyting algebra), but the underlying coherence space satisfies some tractability condition. We also provide a product construction to combine graphs and their axiomatisations, yielding a sound and complete composite system. This development has been fully formalised in Rocq.