Parallel computation

Parallel computation of a computable sequence of computations by a diagonal enumeration. The important theorems of this operation are proven as terminates_parallel and exists_of_mem_parallel. (This operation is nondeterministic in the sense that it does not honor sequence equivalence (irrelevance of computation time).)

def Computation.parallel.aux2 {α : Type u} : List (Computation α) → α ⊕ List (Computation α)

Equations

• One or more equations did not get rendered due to their size.

def Computation.parallel.aux1 {α : Type u} : List (Computation α) × Stream'.WSeq (Computation α) → α ⊕ List (Computation α) × Stream'.WSeq (Computation α)

Equations

• One or more equations did not get rendered due to their size.

def Computation.parallel {α : Type u} (S : Stream'.WSeq (Computation α)) : Computation α

Parallel computation of an infinite stream of computations, taking the first result

Equations

• Computation.parallel S = Computation.corec Computation.parallel.aux1 ([], S)

theorem Computation.terminates_parallel.aux {α : Type u} {l : List (Computation α)} {S : Stream'.WSeq (Computation α)} {c : Computation α} : c ∈ l → c.Terminates → (Computation.corec Computation.parallel.aux1 (l, S)).Terminates

theorem Computation.terminates_parallel {α : Type u} {S : Stream'.WSeq (Computation α)} {c : Computation α} (h : c ∈ S) [T : c.Terminates] : (Computation.parallel S).Terminates

theorem Computation.exists_of_mem_parallel {α : Type u} {S : Stream'.WSeq (Computation α)} {a : α} (h : a ∈ Computation.parallel S) : ∃ (c : Computation α), c ∈ S ∧ a ∈ c

theorem Computation.map_parallel {α : Type u} {β : Type v} (f : α → β) (S : Stream'.WSeq (Computation α)) : Computation.map f (Computation.parallel S) = Computation.parallel (Stream'.WSeq.map (Computation.map f) S)

theorem Computation.parallel_empty {α : Type u} (S : Stream'.WSeq (Computation α)) (h : S.head.Promises none) : Computation.parallel S = Computation.empty α

def Computation.parallelRec {α : Type u} {S : Stream'.WSeq (Computation α)} (C : α → Sort v) (H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a) {a : α} (h : a ∈ Computation.parallel S) : C a

theorem Computation.parallel_promises {α : Type u} {S : Stream'.WSeq (Computation α)} {a : α} (H : ∀ (s : Computation α), s ∈ S → s.Promises a) : (Computation.parallel S).Promises a

theorem Computation.mem_parallel {α : Type u} {S : Stream'.WSeq (Computation α)} {a : α} (H : ∀ (s : Computation α), s ∈ S → s.Promises a) {c : Computation α} (cs : c ∈ S) (ac : a ∈ c) : a ∈ Computation.parallel S

theorem Computation.parallel_congr_lem {α : Type u} {S : Stream'.WSeq (Computation α)} {T : Stream'.WSeq (Computation α)} {a : α} (H : Stream'.WSeq.LiftRel Computation.Equiv S T) : (∀ (s : Computation α), s ∈ S → s.Promises a) ↔ ∀ (t : Computation α), t ∈ T → t.Promises a

theorem Computation.parallel_congr_left {α : Type u} {S : Stream'.WSeq (Computation α)} {T : Stream'.WSeq (Computation α)} {a : α} (h1 : ∀ (s : Computation α), s ∈ S → s.Promises a) (H : Stream'.WSeq.LiftRel Computation.Equiv S T) : (Computation.parallel S).Equiv (Computation.parallel T)

theorem Computation.parallel_congr_right {α : Type u} {S : Stream'.WSeq (Computation α)} {T : Stream'.WSeq (Computation α)} {a : α} (h2 : ∀ (t : Computation α), t ∈ T → t.Promises a) (H : Stream'.WSeq.LiftRel Computation.Equiv S T) : (Computation.parallel S).Equiv (Computation.parallel T)