Deciders and normal form verifiers #

Blueprint def:decider, def:normal-verifier and def:lambda-bounded (paper games.tex, Definitions def:decider, def:normal-ver, def:normal-game, def:lambda; ledger node 1.1.3). A normal form verifier is the uniform way the pipeline presents an infinite family of games: a sampler (MIPRE.CL.Sampler), which produces the questions, and a decider, which checks the answers, both programs of the ambient cost model (MIPRE.Cost).

MIPRE.Decider: a program whose one input is encode (n, x, y, a, b); it accepts when it halts with output 1 (Decider.Accepts), and rejects otherwise. Decider.TimeBoundAt n T k is TIME_𝒟(n) ≤ T, read as halting within cost T · (|d| + 1)^k on every input (n, d), well formed or not: the paper's bound is uniform over all inputs, which the ambient model cannot achieve (see below), so the running time is bounded by a polynomial in the size of the input whose coefficient is T and whose degree is k.
MIPRE.Verifier ℓ: a sampler and a decider, with the paper's requirement that the decider accept only questions of the sampler's dimension s(n) (it "first checks |x| = |y| = s(n)", Verifier.accepts_length).
Verifier.game n T: the game 𝒱_n — questions 𝔽₂^{s(n)}, answers the bit strings of length at most T (Verifier.Answers T), the sampler's distribution, and acceptance by the decider. The paper's 𝒱_n is the case T = TIME_𝒟(n); the bound is a parameter here because every statement about 𝒱_n carries an explicit time bound anyway, and taking the exact supremum would only add a degenerate case (TIME_𝒟(n) = ∞, where the paper's game is undefined) to every definition. Verifier.syncGame is the same game as a SynchronousGame, under the condition on the decider that makes it one (Verifier.IsSynchronousAt).
Verifier.IsBounded λ: def:lambda-bounded, TIME_𝒮(n), TIME_𝒟(n) ≤ n^λ with degree λ in the input size, and s(n) ≤ n^λ, for n ≥ 2, and |𝒱| ≤ λ.

Timeouts are not modelled: in the ambient cost model a decider with TIME_𝒟(n) < ∞ halts on every input of index n, and the paper's convention that a timeout is a rejection is the convention that anything but halting with output 1 is.

Why the time bound is a polynomial in the input size #

The paper's TIME_𝒟(n) is the maximum of the running time over all inputs of index n, finite because a Turing machine can stop reading after a bounded prefix. The ambient model has no cursor into its input: a value is inspected in place by elim, one node per step, but a loop can carry the rest of a list from one iteration to the next only by copying it (Eval.var costs the size of the value), so walking j cells of a list of size s costs about j · s, and no program can check |x| = s(n) for unbounded s(n) within a cost independent of |x|. A bound uniform over all inputs is therefore satisfiable only by deciders that never look past a fixed depth of their input — none that satisfies Verifier.accepts_length with s(n) → ∞.

The degree k is needed as well as the coefficient T, and this is forced by the one thing every decider of the pipeline does: run another program through the universal machine. The overhead of MIPRE.Cost.UniversalMachine is a polynomial Q in |c| + |v| + t, of degree well above one (Cost.Universal.univPoly), so a simulated run costing T · (|d| + 1)^k becomes one costing about Q(T · (|d| + 1)^k), of degree k · deg Q in the input size. No fixed degree is closed under the composition the deciders perform; a bounded degree is, and k is that bound. Taking one parameter for both — T · (|d| + 1)^T — would be closed too, but then λ-boundedness would read as degree n^λ in the input size, which is not a polynomial-time condition at all and would make MIPRE.GapCompression assume compression of verifiers the paper's proof cannot compress.

So TimeBoundAt n T k is "cost at most T · (|d| + 1)^k", and λ-boundedness bounds both parameters by λ's: coefficient n^λ, degree λ. The consequence s(n) ≤ TIME_𝒮(n) of the paper, which depended on the uniform bound, is put into IsBounded as a clause.

Deciders and normal form verifiers #

Why the time bound is a polynomial in the input size #

Deciders #

Normal form verifiers #