Configurations as words: the rewriting system of a machine

The middle layer of the RE-hardness of DescriptiveComplexity.PCP: a machine on the unbounded tape of DescriptiveComplexity.MachinesUnbounded accepts exactly when the string-rewriting system read off its transition table derives the halting word from the start word (DescriptiveComplexity.HaltPcp.acceptsU_iff_derives). Composed with DescriptiveComplexity.Pcp.History.hasMatch_iff one file up, this makes the domino system of the machine decide its acceptance; the sibling Interp file draws that domino system as a first-order interpretation.

The words

A configuration is written as a word over DescriptiveComplexity.HaltPcp.TapeLetter: a left endmarker, the symbols of a finite window of consecutive tape cells with the state letter wedged in front of the head's cell, and a right endmarker (DescriptiveComplexity.HaltPcp.Represents). The window must contain the head and every non-blank cell, and may contain any amount of blank padding beyond them – a configuration has many words, which is what lets the rules extend the window on demand.

The format is kept strict: the state letter always has a symbol letter to its right (the cell the head is on). Each rule of DescriptiveComplexity.HaltPcp.MRule preserves strictness on its own – the boundary variants of the two moves extend the window by one blank cell in the same rewriting step – so every word of a derivation between the boot and the halting letter is a configuration word, and the backward reading of a derivation is a plain case analysis on the rule applied.

The rules

• the two moves, each in a running variant and a boundary variant that writes a blank into the cell entering the window. A transition's attributes are relations, not functions, so the rules are indexed by the attribute values, with the transition existentially quantified in the side condition;
• boot: the start word carries a boot letter in the state slot, and a rule per start state replaces it. This is what lets the single start domino of the PCP construction serve a machine with several start states;
• halting: a rule per accepting state replaces the state letter by the halting letter, and two-letter erasers then melt the rest of the word away. Both sides of every rule are nonempty, as the domino construction requires – erasure consumes a neighboring letter instead of producing the empty word.

No letter of a configuration word is a boot or halting letter, so the boot rule fires only on the start word and the erasers only after an accepting state was seen: the phases of a derivation cannot mix.

The alphabet

inductive DescriptiveComplexity.HaltPcp.TapeLetter (A : Type) : Type

The alphabet configurations are written in: the two endmarkers of the window, the boot letter standing in the state slot of the start word, the halting letter, and a symbol letter and a state letter per element of the machine.

• lft {A : Type} : TapeLetter A

  The left endmarker of the window.

• rgt {A : Type} : TapeLetter A

  The right endmarker of the window.

• boot {A : Type} : TapeLetter A

  The boot letter, in the state slot of the start word.

• halt {A : Type} : TapeLetter A

  The halting letter, the one-letter word a derivation must reach.

• sym {A : Type} : A → TapeLetter A

  The contents of a tape cell.

• state {A : Type} : A → TapeLetter A

  The current state, wedged before the head's cell.

def DescriptiveComplexity.HaltPcp.TapeLetter.isState {A : Type} : TapeLetter A → Bool

Being a state letter, as a Boolean – the alphabet has no decidable equality to offer, but the constructor is decidable on its own.

Equations

• (DescriptiveComplexity.HaltPcp.TapeLetter.state a).isState = true
• x✝.isState = false

theorem DescriptiveComplexity.HaltPcp.TapeLetter.absurd_of_ne {A : Type} {P : Prop} {a b : TapeLetter A} (h : a = b) (hne : a ≠ b := by simp) : P

A letter of the words below is never a boot or halting letter; this is the shape the case analyses need.

The rules

inductive DescriptiveComplexity.HaltPcp.MRule {A : Type} (M : TMData A) : List (TapeLetter A) → List (TapeLetter A) → Prop

The rewriting system of a machine: the two moves with their boundary variants, the boot rule, and the halting rule with its erasers. The transition performing a move is existentially quantified in the side condition, since its attributes are relations rather than functions; the letters of the rule are the attribute values themselves.

• boot {A : Type} {M : TMData A} {q : A} : M.Start q → MRule M [TapeLetter.boot] [TapeLetter.state q]

  The boot letter becomes a start state.

• moveR {A : Type} {M : TMData A} {τ q a b q' c : A} : M.Tr τ → M.Right τ → M.Src τ q → M.Read τ a → M.Dst τ q' → M.Write τ b → MRule M [TapeLetter.state q, TapeLetter.sym a, TapeLetter.sym c] [TapeLetter.sym b, TapeLetter.state q', TapeLetter.sym c]

  A right move with the head staying inside the window: the letter beyond the head is carried along unchanged.

• moveREnd {A : Type} {M : TMData A} {τ q a b q' bk : A} : M.Tr τ → M.Right τ → M.Src τ q → M.Read τ a → M.Dst τ q' → M.Write τ b → M.Blank bk → MRule M [TapeLetter.state q, TapeLetter.sym a, TapeLetter.rgt] [TapeLetter.sym b, TapeLetter.state q', TapeLetter.sym bk, TapeLetter.rgt]

  A right move at the right edge of the window: the cell entering the window is blank.

• moveL {A : Type} {M : TMData A} {τ q a b q' c : A} : M.Tr τ → ¬M.Right τ → M.Src τ q → M.Read τ a → M.Dst τ q' → M.Write τ b → MRule M [TapeLetter.sym c, TapeLetter.state q, TapeLetter.sym a] [TapeLetter.state q', TapeLetter.sym c, TapeLetter.sym b]

  A left move with the head staying inside the window.

• moveLEnd {A : Type} {M : TMData A} {τ q a b q' bk : A} : M.Tr τ → ¬M.Right τ → M.Src τ q → M.Read τ a → M.Dst τ q' → M.Write τ b → M.Blank bk → MRule M [TapeLetter.lft, TapeLetter.state q, TapeLetter.sym a] [TapeLetter.lft, TapeLetter.state q', TapeLetter.sym bk, TapeLetter.sym b]

  A left move at the left edge of the window: the cell entering the window is blank.

• acc {A : Type} {M : TMData A} {q : A} : M.Acc q → MRule M [TapeLetter.state q] [TapeLetter.halt]

  An accepting state becomes the halting letter.

• eraseSymL {A : Type} {M : TMData A} (c : A) : MRule M [TapeLetter.sym c, TapeLetter.halt] [TapeLetter.halt]

  The halting letter swallows the symbol to its left.

• eraseLft {A : Type} {M : TMData A} : MRule M [TapeLetter.lft, TapeLetter.halt] [TapeLetter.halt]

  The halting letter swallows the left endmarker.

• eraseSymR {A : Type} {M : TMData A} (c : A) : MRule M [TapeLetter.halt, TapeLetter.sym c] [TapeLetter.halt]

  The halting letter swallows the symbol to its right.

• eraseRgt {A : Type} {M : TMData A} : MRule M [TapeLetter.halt, TapeLetter.rgt] [TapeLetter.halt]

  The halting letter swallows the right endmarker.

The order of the cells

The cells ℤ × A are ordered lexicographically – pages first, the machine's order on the offsets inside a page – and one DescriptiveComplexity.TMData.SuccCell step increases that order strictly. This is what makes a window a duplicate-free list and puts a cell entering it outside of it.

def DescriptiveComplexity.HaltPcp.CellLt {A : Type} (M : TMData A) (x y : ℤ × A) : Prop

The strict lexicographic order on cells.

Equations

• DescriptiveComplexity.HaltPcp.CellLt M x y = (x.1 < y.1 ∨ x.1 = y.1 ∧ M.Le x.2 y.2 ∧ x.2 ≠ y.2)

theorem DescriptiveComplexity.HaltPcp.CellLt.trans {A : Type} {M : TMData A} (hlin : IsLinOrd M.Le) {x y z : ℤ × A} (hxy : CellLt M x y) (hyz : CellLt M y z) : CellLt M x z

theorem DescriptiveComplexity.HaltPcp.CellLt.ne {A : Type} {M : TMData A} {x y : ℤ × A} (h : CellLt M x y) : x ≠ y

Every cell has a next one and a previous one

On a well-formed machine with at least one position, the strip of pages is unbounded in both directions: the mirror-image lemmas of DescriptiveComplexity.exists_predPos supply the missing successor facts.

Configuration words

A configuration is written as a window of consecutive cells: the symbols they hold, with the state letter wedged before the head's cell and an endmarker at each end. The window contains the head and every non-blank cell over a position; it may contain blank padding beyond them, so a configuration has many words.

def DescriptiveComplexity.HaltPcp.cellSyms {A : Type} (c : ConfigU A) (l : List (ℤ × A)) : List (TapeLetter A)

The symbol letters of a list of cells.

Equations

• DescriptiveComplexity.HaltPcp.cellSyms c l = List.map (fun (x : ℤ × A) => DescriptiveComplexity.HaltPcp.TapeLetter.sym (c.tape x)) l

@[simp]

theorem DescriptiveComplexity.HaltPcp.cellSyms_nil {A : Type} (c : ConfigU A) : cellSyms c [] = []

@[simp]

theorem DescriptiveComplexity.HaltPcp.cellSyms_cons {A : Type} (c : ConfigU A) (x : ℤ × A) (l : List (ℤ × A)) : cellSyms c (x :: l) = TapeLetter.sym (c.tape x) :: cellSyms c l

@[simp]

theorem DescriptiveComplexity.HaltPcp.cellSyms_append {A : Type} (c : ConfigU A) (l l' : List (ℤ × A)) : cellSyms c (l ++ l') = cellSyms c l ++ cellSyms c l'

Letters of a configuration word

A configuration word carries no boot and no halting letter, and exactly one state letter; these two facts drive the case analysis on a rewriting step.

@[simp]

theorem DescriptiveComplexity.HaltPcp.isState_lft {A : Type} : TapeLetter.lft.isState = false

@[simp]

theorem DescriptiveComplexity.HaltPcp.isState_rgt {A : Type} : TapeLetter.rgt.isState = false

@[simp]

theorem DescriptiveComplexity.HaltPcp.isState_boot {A : Type} : TapeLetter.boot.isState = false

@[simp]

theorem DescriptiveComplexity.HaltPcp.isState_halt {A : Type} : TapeLetter.halt.isState = false

@[simp]

theorem DescriptiveComplexity.HaltPcp.isState_sym {A : Type} (a : A) : (TapeLetter.sym a).isState = false

@[simp]

theorem DescriptiveComplexity.HaltPcp.isState_state {A : Type} (q : A) : (TapeLetter.state q).isState = true

def DescriptiveComplexity.HaltPcp.stateCount {A : Type} (l : List (TapeLetter A)) : ℕ

The number of state letters of a word.

Equations

• DescriptiveComplexity.HaltPcp.stateCount l = List.countP DescriptiveComplexity.HaltPcp.TapeLetter.isState l

@[simp]

theorem DescriptiveComplexity.HaltPcp.stateCount_nil {A : Type} : stateCount [] = 0

@[simp]

theorem DescriptiveComplexity.HaltPcp.stateCount_cellSyms {A : Type} (c : ConfigU A) (l : List (ℤ × A)) : stateCount (cellSyms c l) = 0

Reading a rewriting step off a configuration word

The inversion at the heart of the backward direction: a rewriting step on a configuration word either simulates one machine step or fires the halting rule on the current – hence accepting – state. Each move rule carries exactly one state letter on its left-hand side, and a configuration word carries exactly one, so the rule can only apply at the head.

Writing a machine step as a rewriting step

The forward direction: one machine step is one rewriting step – the boundary variants of the moves extend the window in the same stroke, so no separate padding step is ever needed.

Whole runs, and the halting phase

The start word

The start word writes the input page between the endmarkers, with the boot letter in the state slot; the boot rule turns it into a word of an initial configuration. The page is read along an enumeration of the positions in the machine's order.

def DescriptiveComplexity.HaltPcp.IsPosEnum {A : Type} (M : TMData A) (ps : List A) : Prop

ps enumerates the positions, in the machine's order.

Equations

• DescriptiveComplexity.HaltPcp.IsPosEnum M ps = (List.Pairwise (fun (p q : A) => M.Le p q ∧ p ≠ q) ps ∧ ∀ (p : A), p ∈ ps ↔ M.Posn p)

def DescriptiveComplexity.HaltPcp.startWord {A : Type} (inp : List A) : List (TapeLetter A)

The start word of an input page: endmarkers, the boot letter, and the symbols of the page.

Equations

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

theorem DescriptiveComplexity.HaltPcp.IsPosEnum.ne_nil {A : Type} {M : TMData A} (hwf : M.WellFormed) {ps : List A} (hps : IsPosEnum M ps) : ps ≠ []

A machine with a position has a nonempty enumeration.

theorem DescriptiveComplexity.HaltPcp.IsPosEnum.isChain {A : Type} {M : TMData A} (hlin : IsLinOrd M.Le) {ps : List A} (hps : IsPosEnum M ps) : List.IsChain (SuccPos M.Le M.Posn) ps

Consecutive entries of an enumeration are consecutive positions.

The equivalence

theorem DescriptiveComplexity.HaltPcp.acceptsU_iff_derives {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) {ps inp : List A} (hps : IsPosEnum M ps) (hinp : List.Forall₂ M.InitTape ps inp) : M.AcceptsU ↔ Pcp.History.Derives (MRule M) (startWord inp) [TapeLetter.halt]

Acceptance is derivability: the machine accepts exactly when the rewriting system derives the halting word from the start word.

theorem DescriptiveComplexity.HaltPcp.acceptsU_iff_hasMatch {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) {ps inp : List A} (hps : IsPosEnum M ps) (hinp : List.Forall₂ M.InitTape ps inp) : M.AcceptsU ↔ Pcp.History.HasMatch (MRule M) (startWord inp) TapeLetter.halt

Acceptance is having a match: the domino system of the machine's rewriting rules has a match exactly when the machine accepts.