Typed samplers with an ambient program

The typed version of the sampler interface in types.tex. There is a single program and a common ambient dimension. A dimension query carries no type; every other query carries the selected type together with the usual query.

inductive MIPRE.CL.TypedSampler.Query (T : Type u_1) : Type u_1

• dimension {T : Type u_1} : Query T
• atType {T : Type u_1} (type : T) (query : Sampler.Query) : Query T

def MIPRE.CL.TypedSampler.Query.toData {T : Type u_1} [Cost.SizedEncoding T] : Query T → Cost.Data

Equations

• MIPRE.CL.TypedSampler.Query.dimension.toData = MIPRE.Cost.Data.nil
• (MIPRE.CL.TypedSampler.Query.atType t q).toData = (MIPRE.Cost.encode t).cons (MIPRE.Cost.encode q)

def MIPRE.CL.TypedSampler.Query.ofData {T : Type u_1} [Cost.SizedEncoding T] : Cost.Data → Option (Query T)

Equations

• MIPRE.CL.TypedSampler.Query.ofData MIPRE.Cost.Data.nil = some MIPRE.CL.TypedSampler.Query.dimension
• MIPRE.CL.TypedSampler.Query.ofData (t.cons q) = (MIPRE.Cost.decode t).bind fun (t' : T) => Option.map (MIPRE.CL.TypedSampler.Query.atType t') (MIPRE.Cost.decode q)

@[simp]

theorem MIPRE.CL.TypedSampler.Query.ofData_toData {T : Type u_1} [Cost.SizedEncoding T] (q : Query T) : ofData q.toData = some q

@[instance_reducible]

instance MIPRE.CL.TypedSampler.Query.instSizedEncoding {T : Type u_1} [Cost.SizedEncoding T] : Cost.SizedEncoding (Query T)

Equations

• MIPRE.CL.TypedSampler.Query.instSizedEncoding = { encode := MIPRE.CL.TypedSampler.Query.toData, decode := MIPRE.CL.TypedSampler.Query.ofData, decode_encode := ⋯ }

structure MIPRE.CL.TypedSampler (ℓ : ℕ) (T : Type u_1) [Cost.SizedEncoding T] : Type u_1

A typed sampler has one executable query interface for all types, rather than a nonuniform collection of independently chosen programs.

• prog : Cost.Prog
• closed : Cost.Prog.WellScoped 1 self.prog
• dim : ℕ → ℕ
• cl (n : ℕ) : Player → T → CLFun 𝔽₂ (Fin (self.dim n)) ℓ
• cl_exactlyOn (n : ℕ) (w : Player) (t : T) : (self.cl n w t).ExactlyOn Finset.univ
• runs_dimension (n : ℕ) : ∃ (time : ℕ), self.prog.Runs (Cost.encode (n, Query.dimension)) (Cost.encode (self.dim n)) time
• runs_marginal (n : ℕ) (w : Player) (t : T) (j : ℕ) (z : Cost.BitStr) : 1 ≤ j → j ≤ ℓ → List.length z = self.dim n → ∃ (time : ℕ), self.prog.Runs (Cost.encode (n, Query.atType t (Sampler.Query.marginal w j z))) (Cost.encode (toBits ((CLFun.truncate j (self.cl n w t)).eval (ofBits (self.dim n) z)))) time
• runs_linear (n : ℕ) (w : Player) (t : T) (j : ℕ) (u y : Cost.BitStr) : 1 ≤ j → j ≤ ℓ → (∃ (x : Fin (self.dim n) → 𝔽₂), u = toBits ((CLFun.truncate (j - 1) (self.cl n w t)).eval x)) → List.length y = self.dim n → ∃ (time : ℕ), self.prog.Runs (Cost.encode (n, Query.atType t (Sampler.Query.linear w j u y))) (Cost.encode (toBits (((self.cl n w t).mapOfPrefix (j - 1) (ofBits (self.dim n) u)) (ofBits (self.dim n) y)))) time
• runs_factor (n : ℕ) (w : Player) (t : T) (j : ℕ) (u : Cost.BitStr) : 1 ≤ j → j ≤ ℓ → (∃ (x : Fin (self.dim n) → 𝔽₂), u = toBits ((CLFun.truncate (j - 1) (self.cl n w t)).eval x)) → ∃ (time : ℕ), self.prog.Runs (Cost.encode (n, Query.atType t (Sampler.Query.factor w j u))) (Cost.encode (indicatorBits ((self.cl n w t).factorOfPrefix (j - 1) (ofBits (self.dim n) u)))) time
• halts (n : ℕ) (d : Cost.Data) : Cost.Halts self.prog ((Cost.encode n).cons d)

def MIPRE.CL.TypedSampler.TimeBoundAt {ℓ : ℕ} {T : Type u_1} [Cost.SizedEncoding T] (S : TypedSampler ℓ T) (n B k : ℕ) : Prop

Equations

• S.TimeBoundAt n B k = ∀ (d : MIPRE.Cost.Data), MIPRE.Cost.HaltsWithin S.prog ((MIPRE.Cost.encode n).cons d) (B * (d.size + 1) ^ k)

theorem MIPRE.CL.TypedSampler.TimeBoundAt.mono {ℓ : ℕ} {T : Type u_1} [Cost.SizedEncoding T] {S : TypedSampler ℓ T} {n B k B' k' : ℕ} (h : S.TimeBoundAt n B k) (hB : B ≤ B') (hk : k ≤ k') : S.TimeBoundAt n B' k'