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.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

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

      Equations
      Instances For
        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
        Instances For
          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) :