A language in P has a polynomial-time verdict function

⚠️ Unreviewed by Bolton

Complexity.mem_P_of_decisionFn puts a language in P given a verdict function in FP. This file is the converse: a language in P has such a function. That is what a development needs whenever a polynomial-time predicate has to be consulted from inside another polynomial-time computation — the predicate arrives as a machine, and only a function can be composed.

The function is the machine's own run, carried out inside the algebra: Cobham.initFn encodes the initial configuration, Cobham.stepFn advances it, and after the machine's time bound many steps Complexity.acceptFlag reads the verdict cell off the resulting code. Halted configurations are fixed points of the encoded step, so running for exactly the time bound is safe however early the machine stops.

Main definitions

• Complexity.TM.stepOrStay, Complexity.TM.runTo — the run as a total iteration
• Complexity.codeStep — the encoded step with its ruler carried alongside
• Complexity.pVerdict — the verdict function

Main results

• Complexity.runCode_eq — the encoded run is the code of the real one
• Complexity.pVerdict_eq_true_iff — the verdict function decides the language
• Complexity.pVerdict_mem_FP — and it is polynomial-time
• Complexity.exists_decisionFn_of_mem_P — hence every language in P has one

The run as a total iteration

def Complexity.TM.stepOrStay {k : ℕ} (tm : TM k) (c : Cfg k tm.Q) : Cfg k tm.Q

One step of a deterministic machine, staying put once it has halted.

Equations

• tm.stepOrStay c = (tm.step c).getD c

theorem Complexity.TM.stepOrStay_of_halted {k : ℕ} (tm : TM k) {c : Cfg k tm.Q} (h : c.state = tm.qhalt) : tm.stepOrStay c = c

theorem Complexity.TM.stepOrStay_of_step {k : ℕ} (tm : TM k) {c c' : Cfg k tm.Q} (h : tm.step c = some c') : tm.stepOrStay c = c'

def Complexity.TM.runTo {k : ℕ} (tm : TM k) (x : List Bool) (n : ℕ) : Cfg k tm.Q

The configuration after n steps, halted ones counting as no-ops.

Equations

• tm.runTo x n = tm.stepOrStay^[n] (tm.initCfg x)

@[simp]

theorem Complexity.TM.runTo_zero {k : ℕ} (tm : TM k) (x : List Bool) : tm.runTo x 0 = tm.initCfg x

theorem Complexity.TM.runTo_succ {k : ℕ} (tm : TM k) (x : List Bool) (n : ℕ) : tm.runTo x (n + 1) = tm.stepOrStay (tm.runTo x n)

theorem Complexity.TM.iterate_stepOrStay_of_reachesIn {k : ℕ} (tm : TM k) {t : ℕ} {c c' : Cfg k tm.Q} : tm.reachesIn t c c' → tm.stepOrStay^[t] c = c'

A bounded walk is exactly that many total steps.

theorem Complexity.TM.iterate_stepOrStay_halted {k : ℕ} (tm : TM k) {c : Cfg k tm.Q} (h : c.state = tm.qhalt) (n : ℕ) : tm.stepOrStay^[n] c = c

A halted configuration is a fixed point of the total step.

theorem Complexity.TM.runTo_of_halted {k : ℕ} (tm : TM k) (x : List Bool) {t : ℕ} {c : Cfg k tm.Q} (h : tm.reachesIn t (tm.initCfg x) c) (hh : c.state = tm.qhalt) {n : ℕ} (hn : t ≤ n) : tm.runTo x n = c

Once the machine has halted, the run stays where it stopped.

theorem Complexity.TM.exists_reachesIn_runTo {k : ℕ} (tm : TM k) (x : List Bool) (n : ℕ) : ∃ t ≤ n, tm.reachesIn t (tm.initCfg x) (tm.runTo x n)

Every point of the run is reached by a walk no longer than the index.

theorem Complexity.TM.startInvariant_of_reachesIn {k : ℕ} (tm : TM k) {t : ℕ} {c c' : Cfg k tm.Q} : tm.reachesIn t c c' → c.input.StartInvariant → (∀ (i : Fin k), (c.work i).StartInvariant) → c.output.StartInvariant → c'.input.StartInvariant ∧ (∀ (i : Fin k), (c'.work i).StartInvariant) ∧ c'.output.StartInvariant

The left-end markers survive any walk.

theorem Complexity.TM.codeInv_runTo {k : ℕ} (tm : TM k) (x : List Bool) {W n : ℕ} (hn : n ≤ W) : CodeInv W (tm.runTo x n)

Every point of the run is inside the window a time bound gives.

The encoded run

noncomputable def Complexity.codeStep {k : ℕ} (tm : TM k) (w : List Bool) : List Bool

The encoded step, carrying its ruler alongside the code.

Equations

• Complexity.codeStep tm w = Complexity.pair (Complexity.pairFst w) (Complexity.Cobham.stepFn tm (Complexity.pairFst w) (Complexity.pairSnd w))

theorem Complexity.codeStep_pair {k : ℕ} (tm : TM k) (R z : List Bool) : codeStep tm (pair R z) = pair R (Cobham.stepFn tm R z)

theorem Complexity.codeStep_iterate {k : ℕ} (tm : TM k) (R z : List Bool) (n : ℕ) : (codeStep tm)^[n] (pair R z) = pair R ((Cobham.stepFn tm R)^[n] z)

theorem Complexity.codeStep_mem_FP {k : ℕ} (tm : TM k) : codeStep tm ∈ FP

theorem Complexity.runCode_eq {k : ℕ} (tm : TM k) (W : ℕ) (hq : Fintype.card tm.Q ≤ Cobham.blockWidth W) (x : List Bool) (hx : x.length ≤ W) (n : ℕ) : n ≤ W → (Cobham.stepFn tm (Cobham.blockRuler W))^[n] (Cobham.initFn tm (Cobham.blockRuler W) x) = Cobham.cfgCode W (tm.runTo x n)

The encoded run is the code of the real one.

Reading the verdict off a code

theorem Complexity.acceptFlag_cfgCode_tm {k : ℕ} (tm : TM k) (W : ℕ) (c : Cfg k tm.Q) (hq : Fintype.card tm.Q ≤ Cobham.blockWidth W) (hinv : CodeInv W c) (hW : 1 ≤ W) (ruler : List Bool) (hruler : W ≤ ruler.length) : acceptFlag (Cobham.stateCode tm.qhalt) (Cobham.blockRuler W) ruler (Cobham.cfgCode W c) = [true] ↔ c.state = tm.qhalt ∧ c.output.cells 1 = Γ.one

The test decides acceptance, for a deterministic machine.

The verdict function

noncomputable def Complexity.pVerdict {k : ℕ} (tm : TM k) (wp tp : Polynomial ℕ) (x : List Bool) : List Bool

The verdict a deterministic machine reaches, computed inside the algebra.

Equations

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

theorem Complexity.pVerdict_flag {k : ℕ} (tm : TM k) (wp tp : Polynomial ℕ) (x : List Bool) : pVerdict tm wp tp x = [true] ∨ pVerdict tm wp tp x = [false]

theorem Complexity.pVerdict_eq_true_iff {k : ℕ} (tm : TM k) {L : Language} (wp tp : Polynomial ℕ) (hdec : tm.DecidesInTime L fun (n : ℕ) => Polynomial.eval n tp) (hwp : ∀ (n : ℕ), n + Polynomial.eval n tp + 1 ≤ Polynomial.eval n wp) (hq : ∀ (n : ℕ), Fintype.card tm.Q ≤ Cobham.blockWidth (Polynomial.eval n wp)) (x : List Bool) : pVerdict tm wp tp x = [true] ↔ x ∈ L

The verdict function decides the language.

The verdict function is polynomial-time

theorem Complexity.stepFn_iterate_length_le {k : ℕ} (tm : TM k) (R z : List Bool) (hz : z.length ≤ codeBlocks k * R.length) (n : ℕ) : ((Cobham.stepFn tm R)^[n] z).length ≤ codeBlocks k * R.length

The encoded run never grows past the code width.

noncomputable def Complexity.pStateBound (k : ℕ) (wp : Polynomial ℕ) : Polynomial ℕ

The width the whole packed state stays inside.

Equations

• Complexity.pStateBound k wp = 2 * (2 * wp + 2) + 2 + Polynomial.C (Complexity.codeBlocks k) * (2 * wp + 2)

theorem Complexity.pStateBound_eval (k : ℕ) (wp : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (pStateBound k wp) = 2 * (2 * Polynomial.eval n wp + 2) + 2 + codeBlocks k * (2 * Polynomial.eval n wp + 2)

theorem Complexity.pVerdict_mem_FP {k : ℕ} (tm : TM k) (wp tp : Polynomial ℕ) (hwp : ∀ (n : ℕ), n ≤ Polynomial.eval n wp) : pVerdict tm wp tp ∈ FP

The verdict function is polynomial-time.

The bridge

theorem Complexity.exists_decisionFn_of_mem_P {L : Language} (hL : L ∈ P) : ∃ (g : List Bool → Bool), (fun (x : List Bool) => [g x]) ∈ FP ∧ ∀ (x : List Bool), x ∈ L ↔ g x = true

Every language in P has a polynomial-time verdict function. This is the converse of Complexity.mem_P_of_decisionFn_bool: a polynomial-time predicate can always be consulted from inside another polynomial-time computation.