The actual detyping sampler #
A fixed finite graph and an arbitrary typed sampler compile to an ordinary sampler with two additional levels. The construction includes a closed ambient program, all query correctness clauses and halting on every malformed query.
noncomputable def
MIPRE.CL.Detyping.samplerProg
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(S : TypedSampler ℓ T)
:
Equations
Instances For
theorem
MIPRE.CL.Detyping.samplerProg_closed
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(S : TypedSampler ℓ T)
:
Cost.Prog.WellScoped 1 (samplerProg E S)
theorem
MIPRE.CL.Detyping.samplerProg_halts
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(S : TypedSampler ℓ T)
(n : ℕ)
(q : Cost.Data)
:
Cost.Halts (samplerProg E S) ((Cost.encode n).cons q)
theorem
MIPRE.CL.Detyping.run_direct
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(S : TypedSampler ℓ T)
(n : ℕ)
(q : Sampler.Query)
(out : Cost.BitStr)
(h : (Program.route E).toFun (Cost.encode (n, q)) = Program.directResult out)
:
∃ (time : ℕ), (samplerProg E S).Runs (Cost.encode (n, q)) (Cost.encode out) time
theorem
MIPRE.CL.Detyping.run_call
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(S : TypedSampler ℓ T)
(n : ℕ)
(q : Sampler.Query)
(sub : TypedSampler.Query T)
(preBits out : Cost.BitStr)
(time : ℕ)
(h :
(Program.route E).toFun (Cost.encode (n, q)) = Program.callResult (Cost.encode (n, sub)) (Program.withPrefix preBits))
(hr : S.prog.Runs (Cost.encode (n, sub)) (Cost.encode out) time)
:
∃ (t : ℕ), (samplerProg E S).Runs (Cost.encode (n, q)) (Cost.encode (preBits ++ out)) t
theorem
MIPRE.CL.Detyping.samplerProg_dimension
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(S : TypedSampler ℓ T)
(n : ℕ)
:
∃ (time : ℕ),
(samplerProg E S).Runs (Cost.encode (n, Sampler.Query.dimension)) (Cost.encode (graphDim T + S.dim n)) time
theorem
MIPRE.CL.Detyping.samplerProg_marginal
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(S : TypedSampler ℓ T)
(hℓ : 0 < ℓ)
(n : ℕ)
(w : Player)
(j : ℕ)
(z : Cost.BitStr)
(hj : 1 ≤ j)
(hj' : j ≤ ℓ + 2)
(hz : List.length z = graphDim T + S.dim n)
:
∃ (time : ℕ),
(samplerProg E S).Runs (Cost.encode (n, Sampler.Query.marginal w j z))
(Cost.encode (toBits ((CLFun.truncate j (numbered E w (S.cl n w))).eval (ofBits (graphDim T + S.dim n) z)))) time
theorem
MIPRE.CL.Detyping.samplerProg_linear
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(S : TypedSampler ℓ T)
(hℓ : 0 < ℓ)
(n : ℕ)
(w : Player)
(j : ℕ)
(u y : Cost.BitStr)
(hj : 1 ≤ j)
(hj' : j ≤ ℓ + 2)
(hu : ∃ (x : Fin (graphDim T + S.dim n) → 𝔽₂), u = toBits ((CLFun.truncate (j - 1) (numbered E w (S.cl n w))).eval x))
(hy : List.length y = graphDim T + S.dim n)
:
∃ (time : ℕ),
(samplerProg E S).Runs (Cost.encode (n, Sampler.Query.linear w j u y))
(Cost.encode
(toBits
(((numbered E w (S.cl n w)).mapOfPrefix (j - 1) (ofBits (graphDim T + S.dim n) u))
(ofBits (graphDim T + S.dim n) y))))
time
theorem
MIPRE.CL.Detyping.samplerProg_factor
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(S : TypedSampler ℓ T)
(hℓ : 0 < ℓ)
(n : ℕ)
(w : Player)
(j : ℕ)
(u : Cost.BitStr)
(hj : 1 ≤ j)
(hj' : j ≤ ℓ + 2)
(hu : ∃ (x : Fin (graphDim T + S.dim n) → 𝔽₂), u = toBits ((CLFun.truncate (j - 1) (numbered E w (S.cl n w))).eval x))
:
∃ (time : ℕ),
(samplerProg E S).Runs (Cost.encode (n, Sampler.Query.factor w j u))
(Cost.encode (indicatorBits ((numbered E w (S.cl n w)).factorOfPrefix (j - 1) (ofBits (graphDim T + S.dim n) u))))
time
noncomputable def
MIPRE.CL.Detyping.sampler
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(S : TypedSampler ℓ T)
(hℓ : 0 < ℓ)
:
Detyping as a genuine ambient sampler, with two additional CL levels.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPRE.CL.Detyping.sampler_dim
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(S : TypedSampler ℓ T)
(hℓ : 0 < ℓ)
(n : ℕ)
: