Computations

A computation to a configuration is an asynchronous path from the empty configuration to it. This module defines computations, the type of reachable configurations, and linearisations, and relates computations to the configurations they reach.

def EventStructures.emptyConf (es : EventStructure) : Conf es

The empty configuration is a valid configuration.

Equations

• EventStructures.emptyConf es = ⟨∅, ⋯⟩

def EventStructures.Computation (es : EventStructure) (c : Conf es) : Type

A computation to a configuration c is an asynchronous path starting at the empty configuration and ending at c. Equivalently, a computation records a causal execution up to trace equivalence of the underlying path.

Equations

• EventStructures.Computation es c = EventStructures.Path.Async es (EventStructures.emptyConf es) c

def EventStructures.Computations (es : EventStructure) : Type

The type of all computations, paired with their target configuration.

Equations

• EventStructures.Computations es = ((c : EventStructures.Conf es) × EventStructures.Computation es c)

def EventStructures.isLinearisation (es : EventStructure) (c : Conf es) (t : List es.Event) : Prop

A list of events t is a linearisation of configuration c if it is trace-equivalent to the trace of some path from the empty configuration to c. Equivalently, t enumerates the events of c in some order compatible with causality.

Equations

• EventStructures.isLinearisation es c t = ∃ (p : EventStructures.Path es (EventStructures.emptyConf es) c), EventStructures.TraceEquiv es (EventStructures.Path.trace es p) t

theorem EventStructures.computation_is_linearisation (es : EventStructure) {c : Conf es} (comp : Computation es c) : ∃ (t : List es.Event), isLinearisation es c t

Every computation determines a linearisation of its target configuration.

def EventStructures.ReachableConf (es : EventStructure) : Type

Configurations that are reachable by a computation.

Equations

• EventStructures.ReachableConf es = { c : EventStructures.Conf es // Nonempty (EventStructures.Computation es c) }

def EventStructures.computationToReachable (es : EventStructure) : Computations es → ReachableConf es

Every computation targets a reachable configuration.

Equations

• EventStructures.computationToReachable es p = ⟨p.fst, ⋯⟩

theorem EventStructures.computation_to_reachable_surjective (es : EventStructure) : Function.Surjective (computationToReachable es)

The map from computations to reachable configurations is surjective.