Polynomial-time string reversal — proof internals

The transducer reverseTM has one work tape and four control states: it copies the input onto the work tape left to right, then walks the work head back to the left-end marker, emitting each cell to the output as it passes. The result is the input read backwards, in 2 · |x| + 3 steps.

Reversal is what turns a right-to-left recursion into a left-to-right loop: recursion on notation peels the head of a string, so an iterative evaluation consumes the last bit first.

Main results

• Complexity.reverse_mem_FP — reversal is in FP

inductive Complexity.RevPhase : Type

Control states of reverseTM.

• skip : RevPhase

  Move every head off the left-end marker.

• copy : RevPhase

  Copy the input onto the work tape, left to right.

• emit : RevPhase

  Walk the work head back, emitting each cell to the output.

• done : RevPhase

  Halt.

@[implicit_reducible]

instance Complexity.instDecidableEqRevPhase : DecidableEq RevPhase

Equations

• Complexity.instDecidableEqRevPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.instFintypeRevPhase : Fintype RevPhase

Equations

• Complexity.instFintypeRevPhase = { elems := {Complexity.RevPhase.skip, Complexity.RevPhase.copy, Complexity.RevPhase.emit, Complexity.RevPhase.done}, complete := ⋯ }

def Complexity.reverseTM : TM 1

The reversal transducer. Copies the input onto its work tape, then sweeps the work head back to the left-end marker, writing each cell it passes to the output tape. Computes List.reverse.

Equations

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

theorem Complexity.reverseTM_computesInTime : reverseTM.ComputesInTime (fun (x : List Bool) => x.reverse) fun (n : ℕ) => 2 * n + 3

reverseTM computes List.reverse in 2 · |x| + 3 steps.

theorem Complexity.reverse_mem_FP : (fun (x : List Bool) => x.reverse) ∈ FP

Internal proof that string reversal is in FP.