Computations

Asynchronous paths from the empty configuration.

def Computation {L : Type u_1} (F : ConfFamily L) (c : F.Conf) : Type u_2

A computation to c is an asynchronous path from the empty configuration.

Equations

• Computation F c = Path.Async F F.empty c

def Computations {L : Type u_1} (F : ConfFamily L) : Type u_2

All computations, paired with their target configuration.

Equations

• Computations F = ((c : F.Conf) × Computation F c)

def isLinearisation {L : Type u_1} (F : ConfFamily L) (c : F.Conf) (t : List F.Event) : Prop

t linearises c when some path to c has a trace equivalent to t.

Equations

• isLinearisation F c t = ∃ (p : Path F F.empty c), F.TraceEquivFrom (↑F.empty) (Path.trace F p) t

theorem computation_is_linearisation {L : Type u_1} (F : ConfFamily L) {c : F.Conf} (comp : Computation F c) : ∃ (t : List F.Event), isLinearisation F c t

Every computation determines a linearisation of its target configuration.

def ReachableConf {L : Type u_1} (F : ConfFamily L) : Type u_2

Configurations reachable by a computation.

Equations

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

def computation_to_reachable {L : Type u_1} (F : ConfFamily L) : Computations F → ReachableConf F

Every computation targets a reachable configuration.

Equations

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

theorem computation_to_reachable_surjective {L : Type u_1} (F : ConfFamily L) : Function.Surjective (computation_to_reachable F)

The map from computations to reachable configurations is surjective.