def emptyConf (es : EventStructure) : Conf es

The empty configuration is a valid configuration.

Equations

• emptyConf es = ⟨∅, ⋯⟩

def 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

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

def Computations (es : EventStructure) : Type

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

Equations

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

def 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

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

theorem 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 ReachableConf (es : EventStructure) : Type

Configurations that are reachable by a computation.

Equations

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

def computation_to_reachable (es : EventStructure) : Computations es → ReachableConf es

Every computation targets a reachable configuration.

Equations

• computation_to_reachable es p = ⟨p.fst, ⋯⟩

theorem computation_to_reachable_surjective (es : EventStructure) : Function.Surjective (computation_to_reachable es)

The map from computations to reachable configurations is surjective.