Documentation

Mathlib.Data.Seq.Parallel

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

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

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

Equations
theorem Computation.terminates_parallel.aux {α : Type u} {l : List (Computation α)} {S : Stream'.WSeq (Computation α)} {c : Computation α} :
c lc.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.parallel_empty {α : Type u} (S : Stream'.WSeq (Computation α)) (h : S.head.Promises none) :
def Computation.parallelRec {α : Type u} {S : Stream'.WSeq (Computation α)} (C : αSort v) (H : (s : Computation α) → s S(a : α) → a sC a) {a : α} (h : a Computation.parallel S) :
C a
theorem Computation.parallel_promises {α : Type u} {S : Stream'.WSeq (Computation α)} {a : α} (H : ∀ (s : Computation α), s Ss.Promises a) :
(Computation.parallel S).Promises a
theorem Computation.mem_parallel {α : Type u} {S : Stream'.WSeq (Computation α)} {a : α} (H : ∀ (s : Computation α), s Ss.Promises a) {c : Computation α} (cs : c S) (ac : a c) :
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 Ss.Promises a) ∀ (t : Computation α), t Tt.Promises a
theorem Computation.parallel_congr_left {α : Type u} {S : Stream'.WSeq (Computation α)} {T : Stream'.WSeq (Computation α)} {a : α} (h1 : ∀ (s : Computation α), s Ss.Promises a) (H : Stream'.WSeq.LiftRel Computation.Equiv S T) :
theorem Computation.parallel_congr_right {α : Type u} {S : Stream'.WSeq (Computation α)} {T : Stream'.WSeq (Computation α)} {a : α} (h2 : ∀ (t : Computation α), t Tt.Promises a) (H : Stream'.WSeq.LiftRel Computation.Equiv S T) :