Succinct descriptions and the bit-query program

IsSuccinctDesc c n x is [MNY, Definition 2.4] (blueprint def:succinct), with the time bound adapted to the ambient model (see the module docstring of MIPRE.Foundations.Compression). The bit-query program bitQueryProg univ of the recursive compression argument answers bit-queries about a string that is only given implicitly, as the output of a program c' on an input (e, n): on encode (((c', e), n), m) it simulates c' on encode (e, n) through the universal machine and indexes the result with bitAtProg. Its correctness is conditional on the run of c' (bitQueryProg_runs), and hardcoding ((c', e), n) into it gives a succinct description of that output whenever the run is fast enough for the budget (isSuccinctDesc_hardcode).

Succinct descriptions ([MNY, Definition 2.4]; blueprint def:succinct)

def MIPRE.Cost.IsSuccinctDesc (c : Prog) (n : ℕ) (x : BitStr) : Prop

(c, n) succinctly describes the bit string x: c is a closed program, x has length at most 2 ^ n, and c answers every bit-query m (presented in binary; the answer is bitQueryAnswer x m) within cost (n + 1) * (|m| + 1) ^ 2.

[MNY, Definition 2.4], with the time bound adapted as discussed in the module docstring of MIPRE.Foundations.Compression. The pair (c, n) is exponentially smaller than x itself; a compression procedure's guarantees are only required on genuine succinct descriptions, but it must run (in polynomial time) on all inputs.

Equations

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

def MIPRE.Cost.Prog.bitQueryProg (univ : Prog) : Prog

The bit-query program: on encode (((c', e), n), m), run univ on cons (encode c') (encode (e, n)) to obtain the string y, then answer the bit-query m about y with bitAtProg.

Equations

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

theorem MIPRE.Cost.Prog.bitQueryProg_wellScoped {univ : Prog} (hU : WellScoped 1 univ) : WellScoped 1 univ.bitQueryProg

noncomputable def MIPRE.Cost.bitQueryBound (U : UniversalMachine) : Polynomial ℕ

The cost of the bit-query program, as a polynomial in s = esize c' + esize e + esize n + t (with t the cost of the run of c'), per (|m| + 1) ^ 2.

Equations

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

theorem MIPRE.Cost.bitQueryBound_eval (U : UniversalMachine) (s : ℕ) : Polynomial.eval s (bitQueryBound U) = Polynomial.eval (s + 1) U.bound + (s + 1) * (s + 534) + 2 * s + 29

theorem MIPRE.Cost.Prog.bitQueryProg_runs (U : UniversalMachine) {α : Type u_1} [SizedEncoding α] (c' e : Prog) (n : α) (y : BitStr) (m : ℕ) {t : ℕ} (hrun : c'.Runs (encode (e, n)) (encode y) t) : ∃ T ≤ Polynomial.eval (esize c' + esize e + esize n + t) (bitQueryBound U) * (m.size + 1) ^ 2, U.univ.bitQueryProg.Runs (encode (((c', e), n), m)) (bitQueryAnswer y m) T

Conditional correctness of the bit-query program: if c' runs on encode (e, n) to encode y at cost t, then bitQueryProg U.univ answers the bit-query m about y within bitQueryBound U (esize c' + esize e + esize n + t) · (|m| + 1) ^ 2.

theorem MIPRE.Cost.isSuccinctDesc_hardcode (U : UniversalMachine) {α : Type u_1} [SizedEncoding α] (c' e : Prog) (n' : α) (n : ℕ) (y : BitStr) {t : ℕ} (hrun : c'.Runs (encode (e, n')) (encode y) t) (hlen : t ≤ 2 ^ n) (hbudget : Polynomial.eval (esize c' + esize e + esize n' + t) (bitQueryBound U) + (esize c' + esize e + 1 + esize n' + 1) + 4 ≤ n + 1) : IsSuccinctDesc (hardcode U.univ.bitQueryProg (encode ((c', e), n'))) n y

Hardcoding ((c', e), n') into the bit-query program gives a succinct description of the output y of c' on encode (e, n'), with parameter n, as soon as the run of c' fits the budget (n' may be any encodable value, e.g. a level or a pair of levels): its cost t is at most 2 ^ n, and the bit-query overhead is at most n + 1.