Executable specialization of a typed sampler

Fixing a type yields an ordinary sampler, through an actual query adapter. The adapter recognizes the dimension query and otherwise adds the type tag. All malformed queries still halt because they become raw queries to the original typed sampler at the same index.

def MIPRE.CL.TypedSampler.tagQuery {T : Type u_1} [Cost.SizedEncoding T] (t : T) (q : Cost.Data) : Cost.Data

Equations

• MIPRE.CL.TypedSampler.tagQuery t q = if q = MIPRE.Cost.encode MIPRE.CL.Sampler.Query.dimension then MIPRE.Cost.Data.nil else (MIPRE.Cost.encode t).cons q

noncomputable def MIPRE.CL.TypedSampler.adapter {T : Type u_1} [Cost.SizedEncoding T] (t : T) : Cost.PolyTimeFun Cost.Data Cost.Data

The complete raw-data query adapter, including malformed input trees.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.CL.TypedSampler.adapter_cons {T : Type u_1} [Cost.SizedEncoding T] (t : T) (n q : Cost.Data) : (adapter t).toFun (n.cons q) = n.cons (tagQuery t q)

@[simp]

theorem MIPRE.CL.TypedSampler.tagQuery_dimension {T : Type u_1} [Cost.SizedEncoding T] (t : T) : tagQuery t (Cost.encode Sampler.Query.dimension) = Cost.encode Query.dimension

theorem MIPRE.CL.TypedSampler.tagQuery_atType {T : Type u_1} [Cost.SizedEncoding T] (t : T) (q : Sampler.Query) (hq : q ≠ Sampler.Query.dimension) : tagQuery t (Cost.encode q) = Cost.encode (Query.atType t q)

noncomputable def MIPRE.CL.TypedSampler.specializeProg {T : Type u_1} [Cost.SizedEncoding T] {ℓ : ℕ} (S : TypedSampler ℓ T) (t : T) : Cost.Prog

The ordinary program specializing one type of the typed sampler.

Equations

• S.specializeProg t = (MIPRE.CL.TypedSampler.adapter t).code.let_ S.prog

theorem MIPRE.CL.TypedSampler.specializeProg_closed {T : Type u_1} [Cost.SizedEncoding T] {ℓ : ℕ} (S : TypedSampler ℓ T) (t : T) : Cost.Prog.WellScoped 1 (S.specializeProg t)

theorem MIPRE.CL.TypedSampler.specializeProg_runs {T : Type u_1} [Cost.SizedEncoding T] {ℓ : ℕ} (S : TypedSampler ℓ T) (t : T) (n : ℕ) (q r : Cost.Data) (time : ℕ) (hr : S.prog.Runs ((Cost.encode n).cons (tagQuery t q)) r time) : ∃ (time' : ℕ), (S.specializeProg t).Runs ((Cost.encode n).cons q) r time'

noncomputable def MIPRE.CL.TypedSampler.specialize {T : Type u_1} [Cost.SizedEncoding T] {ℓ : ℕ} (S : TypedSampler ℓ T) (t : T) : Sampler ℓ

Fixing any type produces a genuine sampler with the same dimension and CL functions. In particular this is available to detyping's selected-type calls.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.CL.TypedSampler.specialize_dim {T : Type u_1} [Cost.SizedEncoding T] {ℓ : ℕ} (S : TypedSampler ℓ T) (t : T) (n : ℕ) : (S.specialize t).dim n = S.dim n

@[simp]

theorem MIPRE.CL.TypedSampler.specialize_cl {T : Type u_1} [Cost.SizedEncoding T] {ℓ : ℕ} (S : TypedSampler ℓ T) (t : T) (n : ℕ) (w : Player) : (S.specialize t).cl n w = S.cl n w t

noncomputable def MIPRE.CL.TypedSampler.specializeCost {T : Type u_1} [Cost.SizedEncoding T] (t : T) (n B k : ℕ) : Polynomial ℕ

An explicit polynomial for the wrapper's overhead at one index.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.CL.TypedSampler.tagQuery_size {T : Type u_1} [Cost.SizedEncoding T] (t : T) (q : Cost.Data) : (tagQuery t q).size + 1 ≤ q.size + (Cost.esize t + 2)

theorem MIPRE.CL.TypedSampler.specialize_haltsWithin {T : Type u_1} [Cost.SizedEncoding T] {ℓ : ℕ} (S : TypedSampler ℓ T) (t : T) (n B k : ℕ) (h : S.TimeBoundAt n B k) (q : Cost.Data) : Cost.HaltsWithin (S.specialize t).prog ((Cost.encode n).cons q) (Polynomial.eval q.size (specializeCost t n B k))

A typed running-time bound transfers through the actual adapter, including all malformed query trees, with the displayed polynomial overhead.

theorem MIPRE.CL.TypedSampler.specialize_timeBoundAt {T : Type u_1} [Cost.SizedEncoding T] {ℓ : ℕ} (S : TypedSampler ℓ T) (t : T) (n B k : ℕ) (h : S.TimeBoundAt n B k) : ∃ (B' : ℕ) (k' : ℕ), (S.specialize t).TimeBoundAt n B' k'

Specializing a type preserves polynomial boundedness at every index.