The halting problem reduces to tailored games

Paper II, II:1505 (thm:tailored_MIP*=RE), from a tailored gap compression: the statement TailoredGameValue.TailoredHaltingReduction of MIPRE/TailoredGameValue.lean, which mentions Mathlib alone.

The reduction sends a machine M to the tabulation, at the level C, of the tailored halting verifier V^{M,λ} with the search program of Tailored/Halting/Search.lean and λ = Λ₀ + 4|M| (gameOf). That verifier is λ-bounded (Lam0_spec), so its tabulation presents the doubled game at C (presents_tabT), which has no weight on its loops:

• if M halts, V^{M,λ} has a perfect ZPC strategy at C (halting_tailored_search), which, padded with identities, is one of the tabulation (Presents.hasPerfectZPC);
• if not, V^{M,λ} has value at most 1/2 at C, which is the quantum value of the tabulation (Presents.quantumValue_eq), and the synchronous value is at most that (TailoredGameData.gameValue_le_quantumValue).

The map is computable because the processor's description is a fixed tree around the encodings of M and λ (lpBuild, built from the three shapes of Halting/Paper/Build.lean, which are generic in the body), and the tabulation is computable (computable_tabT). Machines are Nat.Partrec.Code, carried to programs by exists_compile; the universal machines are those of Cost/Universal.lean.

tailored_halting_reduction_quantum_of is the stronger form the library proves, with the soundness clause in the quantum value; tailored_halting_reduction_of is the statement.

The processor's description, in polynomial time

theorem MIPRE.Tailored.Halting.toData_F_code {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : (F TG U UT S' M lam).code.toData = Halting.fcodeData (body TG U UT S').toData M.toData (Cost.encode lam)

noncomputable def MIPRE.Tailored.Halting.lpBuild {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyTimeFun (Cost.Prog × ℕ) Cost.Prog

The processor's description from (M, λ), in polynomial time: the description of LP^{M,λ} is that of the existing decider dec M λ with the tailored body.

Equations

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

@[simp]

theorem MIPRE.Tailored.Halting.lpBuild_apply {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (p : Cost.Prog × ℕ) : (lpBuild TG U UT S').toFun p = lpProg TG U UT S' p.1 p.2

The reduction

noncomputable def MIPRE.Tailored.Halting.lamOf {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (M : Cost.Prog) : ℕ

The parameter at the machine M: Λ₀ + 4|M|.

Equations

• MIPRE.Tailored.Halting.lamOf TG U UT M = MIPRE.Tailored.Halting.lamThreshold TG U UT + 4 * MIPRE.Cost.esize M

noncomputable def MIPRE.Tailored.Halting.descM {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (M : Cost.Prog) : Cost.BitStr

The description string of V^{M,λ} at λ = Λ₀ + 4|M|.

Equations

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

noncomputable def MIPRE.Tailored.Halting.gameOf {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (M : Cost.Prog) : TailoredGameValue.TailoredGameData

The reduction's output at M: the tabulation of V^{M,λ} at the level C, for λ = Λ₀ + 4|M|.

Equations

• MIPRE.Tailored.Halting.gameOf TG U UT M = MIPRE.Tailored.tabT TG (MIPRE.Tailored.Halting.descM TG U UT M) (MIPRE.Tailored.Halting.C TG)

theorem MIPRE.Tailored.Halting.presents_gameOf {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (M : Cost.Prog) : ∃ (e : Fin ((gameOf TG U UT M).nV + 1) ≃ Bool × (VT TG U UT M (lamOf TG U UT M)).Questions (C TG)), Presents (gameOf TG U UT M) ((VT TG U UT M (lamOf TG U UT M)).tgame (C TG)).doubled e

The output presents the doubled game of V^{M,λ} at the level C.

theorem MIPRE.Tailored.Halting.hasPerfectZPC_gameOf {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (M : Cost.Prog) (hM : Cost.Halts M Cost.Data.nil) : (gameOf TG U UT M).HasPerfectZPC

Completeness: if M halts on the empty input, the output has a perfect ZPC strategy.

theorem MIPRE.Tailored.Halting.quantumValue_gameOf {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (M : Cost.Prog) : quantumValue (gameOf TG U UT M).game = (VT TG U UT M (lamOf TG U UT M)).valStar (C TG)

The quantum value of the output is the value of V^{M,λ} at the level C.

theorem MIPRE.Tailored.Halting.quantumValue_gameOf_le {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (M : Cost.Prog) (hM : ¬Cost.Halts M Cost.Data.nil) : quantumValue (gameOf TG U UT M).game ≤ 1 / 2

Soundness: if M does not halt on the empty input, the output has quantum value at most 1/2.

theorem MIPRE.Tailored.Halting.computable_gameOf {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {α : Type u_1} [Primcodable α] (f : α → Cost.Prog) (hf : Computable fun (a : α) => Cost.encode (f a)) : Computable fun (a : α) => gameOf TG U UT (f a)

The reduction is computable, along any computable family of encoded machines.

theorem MIPRE.Tailored.tailored_halting_reduction_quantum_of {ℓ : ℕ} (TG : TailoredGapCompression ℓ) : ∃ (g : Nat.Partrec.Code → TailoredGameValue.TailoredGameData), Computable g ∧ ∀ (c : Nat.Partrec.Code), (HaltingGameValue.HaltsOnEmptyInput c → (g c).HasPerfectZPC) ∧ (¬HaltingGameValue.HaltsOnEmptyInput c → quantumValue (g c).game ≤ 1 / 2)

The halting problem reduces to tailored games, in the quantum value, from a tailored gap compression: a computable map from Nat.Partrec.Code to tailored game descriptions with a perfect ZPC strategy on the machines that halt on the empty input and quantum value at most 1/2 on the others.

theorem MIPRE.Tailored.tailored_halting_reduction_of {ℓ : ℕ} (TG : TailoredGapCompression ℓ) : TailoredGameValue.TailoredHaltingReduction

thm:tailored_MIP*=RE from tailored compression (II:1505): a tailored gap compression gives TailoredGameValue.TailoredHaltingReduction, the synchronous value being at most the quantum value.