The halting verifier along the paper's route: the decider

Blueprint lem:halt-construction in the paper's form (recursive.tex, fig:halt_f), for the polynomial-time halting reduction of planning/polytime-halting.md. For a machine M and a parameter λ, the verifier is

Vhalt M λ = Verifier.ofSamplerDecider U (G.sampler λ) (dec M λ),

the compressed sampler at λ together with the decider dec M λ, wrapped in the question-length check of def:normal-verifier. The decider is an efficient Kleene fixed point (Cost.kleeneFix) of the map d' ↦ hardcode body (encode (M, (λ, d'))), so that on (n, x, y, a, b) it runs body on the pair of its own description (M, (λ, dec M λ)) and the input, where body:

1. runs M on the empty input for the budget Nat.size n (the clocked universal machine); if it halts, accepts;
2. otherwise runs the semidecider S' of the search branch — "val* at level C₀ of the verifier this string describes exceeds 1/2" (exists_semL) — on the description descOf λ (dec M λ), for the budget Nat.size n; if it halts, rejects;
3. otherwise computes the compressed decider Compress ((S^compr_λ, wrap (dec M λ)), λ) of its own verifier and runs it on the input through the universal machine.

Branch 2 is Lin's search branch, which the criterion route (Compression.lean, decFunV) has too: the value form of compression has no base case for soundness, and the search supplies it. Branches 1 and 3 are the paper's F. The reading of M's and the search's budgets as Nat.size n rather than n is the criterion's, and costs nothing: the levels of the recursion are n, 2 ^ n, …, along which Nat.size grows without bound.

body is the program of a polynomial-time function prep returning the pair "program to run, its input" — branch 1 returns the constant-true program, branch 2 the constant-false one, branch 3 the compressed decider on the input — followed by one call of the universal machine. That is what makes the acceptance characterization (accepts_iff, blueprint lem:dhalt-values) a matter of running prep and reading its output, and what keeps the accounting (Paper/Cost.lean) to prep's time bound plus the universal machine's overhead on the compressed decider.

Three polynomial-time pieces

noncomputable def MIPRE.Halting.descPoly : Cost.PolyTimeFun (ℕ × Cost.Prog) Cost.BitStr

The description string descOf λ d of a pair, as a polynomial-time function: serProg.

Equations

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

@[simp]

theorem MIPRE.Halting.descPoly_apply (lam : ℕ) (d : Cost.Prog) : descPoly.toFun (lam, d) = descOf lam d

noncomputable def MIPRE.Halting.wrapBuild (U : Cost.UniversalMachine) : Cost.PolyTimeFun (Cost.Prog × Cost.Prog) Cost.Prog

The wrapper's description, as a polynomial-time function of the sampler program and the inner decider: wrapBuildProg.

Equations

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

noncomputable def MIPRE.Halting.wrapPoly (G : GapCompression) (U : Cost.UniversalMachine) : Cost.PolyTimeFun (ℕ × Cost.Prog) Cost.Prog

(λ, d) ↦ wrapCore U.univ (G.samplerProg λ) (encode d), the program of the wrapped decider of the verifier (S^compr_λ, d).

Equations

• MIPRE.Halting.wrapPoly G U = (MIPRE.Halting.wrapBuild U).comp ((G.samplerProg.comp MIPRE.Cost.PolyTimeFun.fst).pair MIPRE.Cost.PolyTimeFun.snd)

theorem MIPRE.Halting.wrapPoly_apply (G : GapCompression) (U : Cost.UniversalMachine) (lam : ℕ) (d : Cost.Prog) : (wrapPoly G U).toFun (lam, d) = U.univ.wrapCore (G.sampler lam).prog (Cost.encode d)

noncomputable def MIPRE.Halting.reencode : Cost.PolyTimeFun (ℕ × Cost.Data) Cost.Data

The pair (n, rest) as the datum encode (n, rest): the identity program.

Equations

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

def MIPRE.Halting.trueProg : Cost.Prog

The program halting with output true on every input.

Equations

• MIPRE.Halting.trueProg = MIPRE.Cost.Prog.const (MIPRE.Cost.encode true)

def MIPRE.Halting.falseProg : Cost.Prog

The program halting with output false on every input.

Equations

• MIPRE.Halting.falseProg = MIPRE.Cost.Prog.const (MIPRE.Cost.encode false)

def MIPRE.Halting.searchP (S' : Cost.Prog) (lam : ℕ) (d : Cost.Prog) : Cost.Prog

The search program of the pair (λ, d): the semidecider S' hard-coded to the description descOf λ d, to be run on the empty input.

Equations

• MIPRE.Halting.searchP S' lam d = MIPRE.Cost.hardcode S'.onLeft (MIPRE.Cost.encode (MIPRE.Halting.descOf lam d))

theorem MIPRE.Halting.halts_searchP_iff {S' : Cost.Prog} (hS' : Cost.Prog.WellScoped 1 S') (lam : ℕ) (d : Cost.Prog) : Cost.Halts (searchP S' lam d) Cost.Data.nil ↔ Cost.Halts S' (Cost.encode (descOf lam d))

The preparation, and the decider

noncomputable def MIPRE.Halting.prep (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyTimeFun ((Cost.Prog × ℕ × Cost.Prog) × ℕ × Cost.Data) (Cost.Prog × Cost.Data)

The three branches, as a polynomial-time function of the description (M, (λ, d')) and the input (n, rest): the program to run and its input.

Equations

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

noncomputable def MIPRE.Halting.comprDec (G : GapCompression) (U : Cost.UniversalMachine) (lam : ℕ) (d : Cost.Prog) : Cost.Prog

The compressed decider of the verifier (S^compr_λ, wrap d).

Equations

• MIPRE.Halting.comprDec G U lam d = G.compress.toFun ((G.samplerProg.toFun lam, U.univ.wrapCore (G.samplerProg.toFun lam) (MIPRE.Cost.encode d)), lam)

theorem MIPRE.Halting.prep_apply (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) (d : Cost.Prog) (n : ℕ) (rest : Cost.Data) : (prep G U UT S').toFun ((M, lam, d), n, rest) = if (Cost.evalWithin M Cost.Data.nil n.size).isSome = true then (trueProg, Cost.Data.nil) else if (Cost.evalWithin (searchP S' lam d) Cost.Data.nil n.size).isSome = true then (falseProg, Cost.Data.nil) else (comprDec G U lam d, Cost.encode (n, rest))

noncomputable def MIPRE.Halting.body (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.Prog

The body of the decider: run prep, then the universal machine on its output.

Equations

• MIPRE.Halting.body G U UT S' = (MIPRE.Halting.prep G U UT S').code.let_ (MIPRE.Cost.Prog.callVar 0 U.univ)

theorem MIPRE.Halting.body_wellScoped (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.Prog.WellScoped 1 (body G U UT S')

noncomputable def MIPRE.Halting.F (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Cost.PolyTimeFun Cost.Prog Cost.Prog

The map whose fixed point is the decider: d' ↦ hardcode body (encode (M, (λ, d'))).

Equations

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

theorem MIPRE.Halting.F_apply (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) (d : Cost.Prog) : (F G U UT S' M lam).toFun d = Cost.hardcode (body G U UT S') (Cost.encode (M, lam, d))

noncomputable def MIPRE.Halting.dec (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Cost.Prog

The decider 𝒟^halt of the machine M at the parameter λ: the efficient Kleene fixed point of F.

Equations

• MIPRE.Halting.dec G U UT S' M lam = MIPRE.Cost.kleeneFix U (MIPRE.Halting.F G U UT S' M lam)

noncomputable def MIPRE.Halting.Vhalt (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Verifier 7

The verifier 𝒱^halt of the machine M at the parameter λ.

Equations

• MIPRE.Halting.Vhalt G U UT S' M lam = MIPRE.Verifier.ofSamplerDecider U (G.sampler lam) (MIPRE.Halting.dec G U UT S' M lam)

theorem MIPRE.Halting.Vhalt_eq_Vof (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Vhalt G U UT S' M lam = Vof G U (descOf lam (dec G U UT S' M lam))

@[simp]

theorem MIPRE.Halting.Vhalt_sampler (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : (Vhalt G U UT S' M lam).sampler = G.sampler lam

theorem MIPRE.Halting.Vhalt_decider_prog (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : (Vhalt G U UT S' M lam).decider.prog = U.univ.wrapCore (G.sampler lam).prog (Cost.encode (dec G U UT S' M lam))

Running the decider

theorem MIPRE.Halting.body_runs_iff (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (P : Cost.Prog × ℕ × Cost.Prog) (n : ℕ) (rest r : Cost.Data) : (∃ (t : ℕ), (body G U UT S').Runs (Cost.encode (P, n, rest)) r t) ↔ ∃ (t : ℕ), ((prep G U UT S').toFun (P, n, rest)).1.Runs ((prep G U UT S').toFun (P, n, rest)).2 r t

A run of body on (P, (n, rest)) is a run of the program prep returns on the input it returns.

theorem MIPRE.Halting.dec_runs_iff (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) (v r : Cost.Data) : (∃ (t : ℕ), (dec G U UT S' M lam).Runs v r t) ↔ ∃ (t : ℕ), (body G U UT S').Runs ((Cost.encode (M, lam, dec G U UT S' M lam)).cons v) r t

A run of the decider on v is a run of body on its own description and v.

theorem MIPRE.Halting.accepts_iff (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam n : ℕ) (x y a b : Cost.BitStr) : (Vhalt G U UT S' M lam).decider.Accepts n x y a b ↔ List.length x = (G.sampler lam).dim n ∧ List.length y = (G.sampler lam).dim n ∧ if (Cost.evalWithin M Cost.Data.nil n.size).isSome = true then True else if (Cost.evalWithin (searchP S' lam (dec G U UT S' M lam)) Cost.Data.nil n.size).isSome = true then False else (G.output ((Vhalt G U UT S' M lam).sampler.prog, (Vhalt G U UT S' M lam).decider.prog) lam).decider.Accepts n x y a b

Acceptance of 𝒱^halt (blueprint lem:dhalt-values): the two questions have the sampler's dimension, and then: everything is accepted if M halts within Nat.size n; nothing is if the search halts within Nat.size n; otherwise exactly what the compressed decider of 𝒱^halt itself accepts.