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 lComputation.Terminates cComputation.Terminates (Computation.corec Computation.parallel.aux1 (l, S))
        theorem Computation.exists_of_mem_parallel {α : Type u} {S : Stream'.WSeq (Computation α)} {a : α} (h : a Computation.parallel S) :
        ∃ (c : Computation α), c S a c
        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
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem Computation.mem_parallel {α : Type u} {S : Stream'.WSeq (Computation α)} {a : α} (H : ∀ (s : Computation α), s SComputation.Promises s 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 SComputation.Promises s a) ∀ (t : Computation α), t TComputation.Promises t a