Collecting runs in finite tuples and vectors

OracleComp.pi collects successive runs of a dependent family of oracle computations indexed by Fin m, in index order, and OracleComp.piRestrict runs only the coordinates belonging to a subset I : Finset (Fin m). OracleComp.replicateFin is the homogeneous specialization of OracleComp.pi to a single repeated program. Listing its coordinates gives the existing list-valued repetition program OracleComp.replicate; closed ProbComp runs draw independent values with the product distribution PMF.pi.

Main definitions

• Cslib.OracleComp.pi: collect successive runs of a dependent family over Fin m.
• Cslib.OracleComp.piRestrict: run only the coordinates in a subset I : Finset (Fin m).
• Cslib.OracleComp.replicateFin: collect successive runs of one program in a length-indexed vector (pi (fun _ => program)).

Main results

• Cslib.OracleComp.replicateFin_eq_pi: replicateFin is the constant-family specialization of pi.
• Cslib.OracleComp.map_ofFn_replicateFin: agreement with list-valued repetition.
• Cslib.ProbComp.mem_support_pi_iff, Cslib.ProbComp.mem_support_replicateFin_iff: support is coordinatewise, even for infinite types.
• Cslib.ProbComp.eval_pi, Cslib.ProbComp.eval_replicateFin: independent finite coordinates have the product law PMF.pi.
• Cslib.ProbComp.eval_pi_map, Cslib.ProbComp.eval_replicateFin_map_coords: coordinatewise maps commute with pi and replicateFin.
• Cslib.ProbComp.eval_bind_restrict_pi, Cslib.ProbComp.eval_map_restrict_pi: restricting eval (pi programs) to I : Finset (Fin m) runs only the programs in I.
• 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 finite-tuple interface to OracleComp.replicate and its product-distribution laws.

def Cslib.OracleComp.pi {Query : Type u} {spec : OracleSpec Query} {m : ℕ} {α : Fin m → Type v} : ((i : Fin m) → OracleComp spec (α i)) → OracleComp spec ((i : Fin m) → α i)

Collect successive runs of a dependent family of oracle computations over Fin m, in execution order (0, 1, …, m - 1).

@[simp]

theorem Cslib.OracleComp.pi_zero {Query : Type u} {spec : OracleSpec Query} {α : Fin 0 → Type v} (programs : (i : Fin 0) → OracleComp spec (α i)) : pi programs = pure fun (i : Fin 0) => i.elim0

theorem Cslib.OracleComp.pi_succ {Query : Type u} {spec : OracleSpec Query} {m : ℕ} {α : Fin (m + 1) → Type v} (programs : (i : Fin (m + 1)) → OracleComp spec (α i)) : pi programs = do let first ← programs 0 Fin.cons first <$> pi fun (i : Fin m) => programs i.succ

def Cslib.OracleComp.piRestrict {Query : Type u} {spec : OracleSpec Query} {m : ℕ} {α : Fin m → Type v} (I : Finset (Fin m)) : ((i : ↥I) → OracleComp spec (α ↑i)) → OracleComp spec ((i : ↥I) → α ↑i)

Run the programs in a subset I : Finset (Fin m) in index order, returning a dependent tuple on I without running programs outside I.

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

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

theorem Cslib.OracleComp.replicateFin_eq_pi {Query : Type u} {spec : OracleSpec Query} {α : Type v} (count : ℕ) (program : OracleComp spec α) : replicateFin count program = pi fun (x : Fin count) => program

replicateFin is the constant-family specialization of pi.

@[simp]

theorem Cslib.OracleComp.replicateFin_zero {Query : Type u} {spec : OracleSpec Query} {α : Type v} (program : OracleComp spec α) : replicateFin 0 program = pure Fin.elim0

theorem Cslib.OracleComp.replicateFin_succ {Query : Type u} {spec : OracleSpec Query} {α : Type v} (count : ℕ) (program : OracleComp spec α) : replicateFin (count + 1) program = do let first ← program Fin.cons first <$> replicateFin count program

@[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_pi_iff {m : ℕ} {α : Fin m → Type} (programs : (i : Fin m) → ProbComp (α i)) (r : (i : Fin m) → α i) : r ∈ (eval (OracleComp.pi programs)).support ↔ ∀ (i : Fin m), r i ∈ (programs i).eval.support

A tuple is in the support of pi programs if and only if each coordinate is in the support of its coordinate program.

theorem Cslib.ProbComp.eval_pi_congr {m : ℕ} {α : Fin m → Type} {p q : (i : Fin m) → ProbComp (α i)} (h : ∀ (i : Fin m), (p i).eval = (q i).eval) : eval (OracleComp.pi p) = eval (OracleComp.pi q)

Evaluating pi programs depends only on the distributions of the individual programs.

theorem Cslib.ProbComp.eval_pi_map {m : ℕ} {α β : Fin m → Type} (programs : (i : Fin m) → ProbComp (α i)) (f : (i : Fin m) → α i → β i) : eval (OracleComp.pi fun (i : Fin m) => f i <$> programs i) = PMF.map (fun (r : (i : Fin m) → α i) (i : Fin m) => f i (r i)) (eval (OracleComp.pi programs))

Mapping each coordinate program commutes with pi.

@[simp]

theorem Cslib.ProbComp.eval_pi_pure {m : ℕ} {α : Fin m → Type} (x : (i : Fin m) → α i) : eval (OracleComp.pi fun (i : Fin m) => pure (x i)) = PMF.pure x

Evaluating pi on pure coordinate programs yields PMF.pure.

theorem Cslib.ProbComp.eval_pi_bind {m : ℕ} {α β : Fin m → Type} (p : (i : Fin m) → ProbComp (α i)) (q : (i : Fin m) → α i → ProbComp (β i)) : eval (OracleComp.pi fun (i : Fin m) => p i >>= q i) = (eval (OracleComp.pi p)).bind fun (a : (i : Fin m) → α i) => eval (OracleComp.pi fun (i : Fin m) => q i (a i))

Coordinatewise monadic bind distributes over eval (OracleComp.pi ...).

theorem Cslib.ProbComp.eval_pi_pair {m : ℕ} {α β : Fin m → Type} (p : (i : Fin m) → ProbComp (α i)) (q : (i : Fin m) → ProbComp (β i)) : eval (OracleComp.pi fun (i : Fin m) => do let a ← p i let b ← q i pure (a, b)) = (eval (OracleComp.pi p)).bind fun (a : (i : Fin m) → α i) => PMF.map (fun (b : (i : Fin m) → β i) (i : Fin m) => (a i, b i)) (eval (OracleComp.pi q))

Pairing independent coordinate programs in OracleComp.pi is equivalent to binding two independent OracleComp.pi runs.

theorem Cslib.ProbComp.eval_pi_comm {m k : ℕ} {α : Fin m → Fin k → Type} (p : (i : Fin m) → (s : Fin k) → ProbComp (α i s)) : eval (OracleComp.pi fun (i : Fin m) => OracleComp.pi fun (s : Fin k) => p i s) = PMF.map (fun (f : (i : Fin k) → (i_1 : Fin m) → α i_1 i) (i : Fin m) (s : Fin k) => f s i) (eval (OracleComp.pi fun (s : Fin k) => OracleComp.pi fun (i : Fin m) => p i s))

Swapping Fin m and Fin k in a nested OracleComp.pi preserves the evaluated PMF.

theorem Cslib.ProbComp.eval_pi {m : ℕ} {α : Fin m → Type} [∀ (i : Fin m), Finite (α i)] (programs : (i : Fin m) → ProbComp (α i)) : eval (OracleComp.pi programs) = Probability.PMF.pi fun (i : Fin m) => (programs i).eval

When each coordinate type is finite, eval (pi programs) is the independent product distribution PMF.pi.

theorem Cslib.ProbComp.eval_bind_restrict_pi {m : ℕ} {α : Fin m → Type} {β : Type} (I : Finset (Fin m)) (programs : (i : Fin m) → ProbComp (α i)) (k : ((i : ↥I) → α ↑i) → PMF β) : ((eval (OracleComp.pi programs)).bind fun (r : (i : Fin m) → α i) => k (I.restrict r)) = (eval (OracleComp.piRestrict I (I.restrict programs))).bind k

Binding eval (pi programs) to a continuation that depends only on I.restrict r is equivalent to running only the programs in I via piRestrict. No finiteness assumption on α is needed.

theorem Cslib.ProbComp.eval_map_restrict_pi {m : ℕ} {α : Fin m → Type} (I : Finset (Fin m)) (programs : (i : Fin m) → ProbComp (α i)) : PMF.map I.restrict (eval (OracleComp.pi programs)) = eval (OracleComp.piRestrict I (I.restrict programs))

Restricting eval (pi programs) to a subset I : Finset (Fin m) has the same law as piRestrict I (I.restrict programs).

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.block (BitString.ofList (count * width) tape) 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.