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

Instances For

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

    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, 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
      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