Collecting runs in finite vectors

OracleComp.replicateFin collects successive runs as a function on Fin count. Listing its coordinates gives exactly the existing list-valued repetition program; the typed vector does not introduce a new sampling primitive or an efficiency assumption. Closed ProbComp runs draw independent values.

Main definitions

• Cslib.OracleComp.replicateFin: collect successive runs in a length-indexed vector.

Main results

• Cslib.OracleComp.map_ofFn_replicateFin: agreement with list-valued repetition.
• Cslib.ProbComp.mem_support_replicateFin_iff: support is coordinatewise, even for infinite types.
• Cslib.ProbComp.eval_replicateFin: independent finite coordinates have the product law.
• Cslib.ProbComp.eval_replicateFin_map: list-valued encodings preserve the joint law.
• Cslib.ProbComp.eval_replicateFin_of_uniformList: a flat fair-bit seed supplies every run.

References

This is the length-indexed interface to OracleComp.replicate and its product-distribution laws.

def Cslib.OracleComp.replicateFin {Query : Type u} {spec : OracleSpec Query} {α : Type v} (count : ℕ) : OracleComp spec α → OracleComp spec (Fin count → α)

Collect successive runs as a length-indexed vector, in execution order.

@[simp]

theorem Cslib.OracleComp.map_ofFn_replicateFin {Query : Type u} {spec : OracleSpec Query} {α : Type v} (count : ℕ) (program : OracleComp spec α) : List.ofFn <$> replicateFin count program = replicate count program

Listing the coordinates gives exactly the existing repeated-run program.

theorem Cslib.ProbComp.mem_support_replicateFin_iff {α : Type} (count : ℕ) (program : ProbComp α) (values : Fin count → α) : values ∈ (eval (OracleComp.replicateFin count program)).support ↔ ∀ (i : Fin count), values i ∈ program.eval.support

The vector support consists exactly of the tuples of individually supported values.

theorem Cslib.ProbComp.eval_replicateFin {α : Type} [Finite α] (count : ℕ) (program : ProbComp α) : eval (OracleComp.replicateFin count program) = Probability.PMF.pi fun (x : Fin count) => program.eval

Finite coordinate distributions give the independent product law.

theorem Cslib.ProbComp.eval_replicateFin_map {α β : Type} {source : ProbComp α} {encoded : ProbComp β} {encode : α → β} (h : encoded.eval = PMF.map encode source.eval) (count : ℕ) : eval (OracleComp.replicate count encoded) = PMF.map (fun (values : Fin count → α) => List.ofFn fun (i : Fin count) => encode (values i)) (eval (OracleComp.replicateFin count source))

Repeating a representation of each sampled value gives the represented vector law.

theorem Cslib.ProbComp.eval_replicateFin_map_coords {α β : Type} (count : ℕ) (program : ProbComp α) (f : α → β) : eval (OracleComp.replicateFin count (f <$> program)) = PMF.map (fun (values : Fin count → α) (i : Fin count) => f (values i)) (eval (OracleComp.replicateFin count program))

Mapping each coordinate after independent runs agrees with mapping each run's outcome. Neither outcome type needs to be finite.

theorem Cslib.ProbComp.eval_replicateFin_of_uniformList {α : Type} (count width : ℕ) (program : ProbComp α) (evaluate : List Bool → α) (hlaw : program.eval = PMF.map evaluate (BitString.uniformList width)) : eval (OracleComp.replicateFin count program) = PMF.map (fun (tape : List Bool) (i : Fin count) => evaluate (List.ofFn ((BitString.ofList (count * width) tape).block i))) (BitString.uniformList (count * width))

Disjoint blocks of one uniform tape realize a vector of independently sampled values. The output type may be infinite, and either the count or the block width may be zero.