palindromes: strings equal to their reverse

A classical non-regular language decided in linear time by a 1-work-tape TM. The machine copies the input to its work tape, rewinds the input head, then scans the input forward and the work tape backward, comparing bits.

Main definitions

• TM.palindromesTM — 6-state 1-work-tape palindrome decider.
• Language.palindromes — {x : List Bool | x = x.reverse}.

Main results

• palindromesTM_reachesIn — halts in 3·|x| + 4 steps on every input.
• palindromes_in_DTIME, palindromes_mem_P.

Design

Phases (see comments on PalindromePhase):

1. start: move all heads from cell 0 (▷) to cell 1.
2. copy: scan input forward, copying each bit to the work tape. When input reads □, move input head left and enter rewindInput.
3. rewindInput: move input head left until reading ▷. On ▷, move input head right to cell 1 and work head left by one, entering compare.
4. compare: compare input and work bits. On match, advance input right and work left. On □, halt with output 1. On mismatch, enter reject.
5. reject: consume remaining input, then halt with output 0.

inductive Complexity.TM.PalindromePhase : Type

Control states of palindromesTM.

• start : PalindromePhase
• copy : PalindromePhase
• rewindInput : PalindromePhase
• compare : PalindromePhase
• reject : PalindromePhase
• done : PalindromePhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqPalindromePhase : DecidableEq PalindromePhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypePalindromePhase : Fintype PalindromePhase

Equations

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

def Complexity.TM.palindromesTM : TM 1

Palindrome-decider TM with one work tape. The work tape is used as a copy of the input, which is then scanned backward during the compare phase.

Equations

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

structure Complexity.TM.CopyInv (c : Cfg 1 palindromesTM.Q) (x : List Bool) (k : ℕ) : Prop

Invariant during the copy phase: work tape holds the first k bits of x, heads are at cell k+1. We use List.get? via getD rather than a sized getElem to avoid embedding proofs in the structure fields.

• kle : k ≤ x.length
• ic : c.input.cells = (Tape.init (List.map Γ.ofBool x)).cells
• ih : c.input.head = k + 1
• wh : (c.work 0).head = k + 1
• wstart : (c.work 0).cells 0 = Γ.start
• wcopy (i : ℕ) : 1 ≤ i → i ≤ k → (c.work 0).cells i = (Tape.init (List.map Γ.ofBool x)).cells i
• wblank (i : ℕ) : i > k → (c.work 0).cells i = Γ.blank
• oh : c.output.head = 1
• ons : c.output.cells 1 ≠ Γ.start

structure Complexity.TM.RewindInv (c : Cfg 1 palindromesTM.Q) (x : List Bool) (j : ℕ) : Prop

Invariant during the rewindInput phase: work tape holds all of x, input head is somewhere in [0 .. x.length].

• jle : j ≤ x.length
• ic : c.input.cells = (Tape.init (List.map Γ.ofBool x)).cells
• ih : c.input.head = j
• wh : (c.work 0).head = x.length + 1
• wstart : (c.work 0).cells 0 = Γ.start
• wcopy (i : ℕ) : 1 ≤ i → i ≤ x.length → (c.work 0).cells i = (Tape.init (List.map Γ.ofBool x)).cells i
• wblank (i : ℕ) : i > x.length → (c.work 0).cells i = Γ.blank
• oh : c.output.head = 1
• ons : c.output.cells 1 ≠ Γ.start

structure Complexity.TM.CompareInv (c : Cfg 1 palindromesTM.Q) (x : List Bool) (k : ℕ) : Prop

Invariant during the compare phase after k matches: input head at k+1, work head at |x|-k.

• kle : k ≤ x.length
• ic : c.input.cells = (Tape.init (List.map Γ.ofBool x)).cells
• ih : c.input.head = k + 1
• wh : (c.work 0).head = x.length - k
• wstart : (c.work 0).cells 0 = Γ.start
• wcopy (i : ℕ) : 1 ≤ i → i ≤ x.length → (c.work 0).cells i = (Tape.init (List.map Γ.ofBool x)).cells i
• wblank (i : ℕ) : i > x.length → (c.work 0).cells i = Γ.blank
• oh : c.output.head = 1
• ons : c.output.cells 1 ≠ Γ.start

structure Complexity.TM.PalRejectInv (c : Cfg 1 palindromesTM.Q) (x : List Bool) (j : ℕ) : Prop

Invariant during the reject phase: input head somewhere in [1 .. x.length+1]; work doesn't matter.

• st : c.state = PalindromePhase.reject
• ic : c.input.cells = (Tape.init (List.map Γ.ofBool x)).cells
• ih : c.input.head = j + 1
• oh : c.output.head = 1
• ons : c.output.cells 1 ≠ Γ.start

def Complexity.TM.IsPalindrome (x : List Bool) : Prop

Pointwise palindrome condition: ∀ i < |x|, x[i] = x[|x|-1-i].

Equations

• Complexity.TM.IsPalindrome x = ∀ (i : ℕ) (hi : i < x.length), x[i] = x[x.length - 1 - i]

theorem Complexity.TM.palindromesTM_reachesIn (x : List Bool) : ∃ (c' : Cfg 1 palindromesTM.Q), palindromesTM.reachesIn (3 * x.length + 4) (palindromesTM.initCfg x) c' ∧ palindromesTM.halted c' ∧ c'.output.cells 1 = if ∀ (i : ℕ) (hi : i < x.length), x[i] = x[x.length - 1 - i] then Γ.one else Γ.zero

palindromesTM halts in 3·|x| + 4 steps on every input, writing the correct answer to output cell 1.

def Complexity.Language.palindromes : Language

The palindromes language — binary strings equal to their reverse.

Equations

• Complexity.Language.palindromes = {x : List Bool | x = x.reverse}

theorem Complexity.TM.palindromesTM_decidesInTime : palindromesTM.DecidesInTime Language.palindromes fun (n : ℕ) => 3 * n + 4

palindromesTM decides Language.palindromes in time 3·|x| + 4.

theorem Complexity.palindromes_in_DTIME : Language.palindromes ∈ DTIME fun (n : ℕ) => 3 * n + 4

palindromes ∈ DTIME(3n + 4).

theorem Complexity.palindromes_mem_P : Language.palindromes ∈ P

palindromes ∈ P.