Deciding whether a record is accepting

⚠️ Unreviewed by Bolton

A record is accepting when its state field is the halting state and its output tape holds 1 in cell 1. The state field is block 0 truncated to the state code's width, and the verdict cell is read after the rewind of Complexitylib.Classes.Containments.Internal.CodeRewind.

Main definitions

• Complexity.verdictSym — the symbol in cell 1 of a rewound output code
• Complexity.acceptFlag — the accepting-record test

Main results

• Complexity.verdictSym_rewound — what the verdict cell reads
• Complexity.acceptFlag_cfgCode — the test decides acceptance
• Complexity.acceptFlagFn_mem_FP — the test is polynomial-time

The verdict cell

def Complexity.verdictSym (R z : List Bool) : List Bool

The symbol in cell 1 of a rewound output code.

Equations

• Complexity.verdictSym R z = List.take 2 (List.drop 2 (List.drop R.length z))

theorem Complexity.verdictSym_rewound (W : ℕ) (t : Tape) (hW : 1 ≤ W) : verdictSym (Cobham.blockRuler W) (Cobham.pairCode W { head := 0, cells := t.cells }) = Cobham.symCode (t.cells 1)

The verdict cell of a rewound output code is cell 1 of the tape.

The test

def Complexity.acceptFlag (qcode R ruler u : List Bool) : List Bool

Is the record an accepting halting configuration?

Equations

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

theorem Complexity.acceptFlag_flag (qcode R ruler u : List Bool) : acceptFlag qcode R ruler u = [true] ∨ acceptFlag qcode R ruler u = [false]

theorem Complexity.acceptFlag_cfgCode {k : ℕ} (tm : NTM 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.

The test is polynomial-time

theorem Complexity.acceptFlagFn_mem_FP (qcode : List Bool) {Rf rulerf uf : List Bool → List Bool} (hR : Rf ∈ FP) (hruler : rulerf ∈ FP) (hu : uf ∈ FP) : (fun (w : List Bool) => acceptFlag qcode (Rf w) (rulerf w) (uf w)) ∈ FP