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).)

source

def Computation.parallel.aux2 {α : Type u} :

List (Computation α) → α ⊕ List (Computation α)

Instances For

source

def Computation.parallel.aux1 {α : Type u} :

List (Computation α) × Stream'.WSeq (Computation α) → α ⊕ List (Computation α) × Stream'.WSeq (Computation α)

Instances For

source

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

Computation α

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

Instances For

source

theorem Computation.terminates_parallel.aux {α : Type u} {l : List (Computation α)} {S : Stream'.WSeq (Computation α)} {c : Computation α} :

c ∈ l → Computation.Terminates c → Computation.Terminates (Computation.corec Computation.parallel.aux1 (l, S))

source

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

Computation.Terminates (Computation.parallel S)

source

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

∃ c, c ∈ S ∧ a ∈ c

source

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)

source

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

Computation.parallel S = Computation.empty α

source

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

Instances For

source

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

Computation.Promises (Computation.parallel S) a

source

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

a ∈ Computation.parallel S

source

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 → Computation.Promises s a) ↔ ∀ (t : Computation α), t ∈ T → Computation.Promises t a

source

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

Computation.Equiv (Computation.parallel S) (Computation.parallel T)

source

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

Computation.Equiv (Computation.parallel S) (Computation.parallel T)