Reading the verdict cell out of a record

⚠️ Unreviewed by Bolton

Acceptance is a property of cell 1 of the output tape, but a code stores each tape split at its head, so where cell 1 sits depends on the head. Driving the head back to cell 0 first puts it in a fixed place: the encoding's right half-block is then the whole tape in order, two bits per cell, so cell 1 is bits 2 and 3.

That is the same rewind the completeness direction of Cobham's theorem uses to read a simulated machine's output, Cobham.rewindFn, run here as a loop of its own.

Main definitions

• Complexity.outPair — the output tape's two blocks, read out of a record
• Complexity.rewindStepP — one rewind step, on the packed state
• Complexity.rewindCode — a whole rewind

Main results

• Complexity.outPair_cfgCode — the two blocks are the output tape's code
• Complexity.rewindCode_pairCode — a long enough rewind parks the head
• Complexity.rewindStepP_mem_FP, Complexity.rewindCodeFn_mem_FP — both are polynomial-time

The output tape inside a record

theorem Complexity.blockAt_cfgCode_outputLeft {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) : blockAt (Cobham.blockRuler W) (Cobham.cfgCode W c) 3 = padTo (Cobham.blockRuler W) (Cobham.leftCode c.output)

Block 3 is the output tape's left half.

theorem Complexity.blockAt_cfgCode_outputRight {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) : blockAt (Cobham.blockRuler W) (Cobham.cfgCode W c) 4 = padTo (Cobham.blockRuler W) (Cobham.rightCode c.output W)

Block 4 is the output tape's right half.

def Complexity.outPair (R u : List Bool) : List Bool

The output tape's code, read out of a record.

Equations

• Complexity.outPair R u = Complexity.blockAt R u 3 ++ Complexity.blockAt R u 4

theorem Complexity.outPairFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => outPair (a z) (b z)) ∈ FP

theorem Complexity.outPair_cfgCode {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) : outPair (Cobham.blockRuler W) (Cobham.cfgCode W c) = Cobham.pairCode W c.output

The two blocks are the output tape's code.

The rewind loop

def Complexity.rewindStepP (z : List Bool) : List Bool

One rewind step, on the packed state pair R z.

Equations

• Complexity.rewindStepP z = Complexity.pair (Complexity.pairFst z) (Complexity.Cobham.rewindFn (Complexity.pairFst z) (Complexity.pairSnd z))

theorem Complexity.rewindStepP_pack (R z : List Bool) : rewindStepP (pair R z) = pair R (Cobham.rewindFn R z)

theorem Complexity.rewindStepP_iterate (R z : List Bool) (n : ℕ) : rewindStepP^[n] (pair R z) = pair R ((Cobham.rewindFn R)^[n] z)

def Complexity.rewindCode (R ruler z : List Bool) : List Bool

A whole rewind: one step per bit of the ruler.

Equations

• Complexity.rewindCode R ruler z = Complexity.pairSnd (Complexity.rewindStepP^[ruler.length] (Complexity.pair R z))

theorem Complexity.rewindCode_eq (R ruler z : List Bool) : rewindCode R ruler z = (Cobham.rewindFn R)^[ruler.length] z

theorem Complexity.rewindCode_pairCode (W : ℕ) (t : Tape) (hinv : t.StartInvariant) (hW : t.head ≤ W) (ruler : List Bool) (hlen : W ≤ ruler.length) : rewindCode (Cobham.blockRuler W) ruler (Cobham.pairCode W t) = Cobham.pairCode W { head := 0, cells := t.cells }

A long enough rewind parks the head at cell 0.

Both are polynomial-time

theorem Complexity.rewindFnFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => Cobham.rewindFn (a z) (b z)) ∈ FP

theorem Complexity.rewindStepP_mem_FP : rewindStepP ∈ FP

theorem Complexity.rewindCodeFn_mem_FP {Rf rulerf zf : List Bool → List Bool} (hR : Rf ∈ FP) (hruler : rulerf ∈ FP) (hz : zf ∈ FP) (hlen : ∀ (w : List Bool), (zf w).length ≤ 2 * (Rf w).length) : (fun (w : List Bool) => rewindCode (Rf w) (rulerf w) (zf w)) ∈ FP

The rewind is polynomial-time.