Skip to content

Emptiness problem for linear bounded automata

InductiveFenced alphabet#✓fully proved

For an alphabet \(\Sigma\), the tape alphabet of the fenced machine consists of a symbol for each letter of \(\Sigma\), two kinds of padding cells (left and right), which the simulated machine reads as blanks, and the wall, which marks the ends of the input.

inductive FenceSymbol (Symbol : Type) where
  /-- A symbol of the simulated machine. -/
  | sym (a : Symbol)
  /-- A padding cell to the right of the input, or a blank written by the simulated machine. -/
  | pad
  /-- A padding cell to the left of the input; the start phase steps over these cells. -/
  | lpad
  /-- An end marker. -/
  | wall
  deriving DecidableEq, Fintype
Used by 15
Used byThe fenced machine halts on some padding of a word iff the machine halts on it · Emptiness of a linear bounded automaton on computable input slices is undecidable · The fenced machine · Fenced input · A transition lifted to the fenced machine · The running transition of the fenced machine · The fenced machine halts on no padding of a word iff the machine does not halt on it · Cells of a fenced input · The fenced machine is a linear bounded automaton · Length of a fenced input · Fenced cell of a write · A fenced cell of a write is never a wall · Simulated cell of a fenced cell · Reading back a copied cell · Reading back a fenced cell of a write

InductiveStates of the fenced machine#✓fully proved

For a set of states \(Q\), the states of the fenced machine are two start states, a running state for each state \(q \in Q\) of the simulated machine, and a trap state.

inductive FenceState (State : Type) where
  /-- The initial state: on a wall, move right; on any other cell, enter the trap. -/
  | start₀
  /-- Step right over the left padding; on any other cell, act as `run` of the initial state of
  the simulated machine. -/
  | start₁
  /-- Run the simulated machine in state `q`; on a wall or a blank cell, enter the trap. -/
  | run (q : State)
  /-- The trap, entered on a wall or a blank cell: loop forever, leaving the tape unchanged. -/
  | trap
  deriving Fintype
Used by 5
Used byThe fenced machine halts on some padding of a word iff the machine halts on it · The fenced machine · A transition lifted to the fenced machine · The running transition of the fenced machine · The fenced machine is a linear bounded automaton

DefinitionSimulated cell of a fenced cell#✓fully proved

The simulated cell of a cell of the fenced machine is the cell of the simulated machine that it stands for: a symbol of the simulated machine stands for itself, and every other cell (a padding cell, a wall or a blank) stands for a blank.

def FenceSymbol.read : Option (FenceSymbol Symbol) → Option Symbol
  | some (.sym a) => some a
  | _ => none
Uses 1 · Used by 3
Statement usesFenced alphabet
Used byThe fenced machine halts on some padding of a word iff the machine halts on it · Reading back a copied cell · Reading back a fenced cell of a write

DefinitionFenced cell of a write#✓fully proved

For a cell \(o\) of the simulated machine, a symbol or a blank, the fenced cell of \(o\) is the cell the fenced machine writes for a write of \(o\): \(o\) itself if \(o\) is a symbol, and the padding cell \(\mathrm{pad}\) if \(o\) is a blank.

def FenceSymbol.ofCell : Option Symbol → FenceSymbol Symbol
  | some a => .sym a
  | none => .pad
Uses 1 · Used by 4
Statement usesFenced alphabet
Used byThe fenced machine halts on some padding of a word iff the machine halts on it · A transition lifted to the fenced machine · A fenced cell of a write is never a wall · Reading back a fenced cell of a write

TheoremReading back a fenced cell of a write#✓fully proved

For every cell \(o\) of the simulated machine, a symbol or a blank, the simulated cell of the fenced cell of \(o\) is \(o\).

@[simp]
theorem FenceSymbol.read_ofCell (o : Option Symbol) : read (some (ofCell o)) = o
Uses 3 · Used by 1
Statement usesFenced alphabet · Fenced cell of a write · Simulated cell of a fenced cell
Used byThe fenced machine halts on some padding of a word iff the machine halts on it

TheoremReading back a copied cell#✓fully proved

Let \(o\) be a cell of the simulated machine, a symbol or a blank, and copy it to the fenced machine, a symbol as itself and a blank as a blank. Then the simulated cell of the copy is \(o\).

@[simp]
theorem FenceSymbol.read_map_sym (o : Option Symbol) : read (o.map sym) = o
Uses 2 · Used by 1
Statement usesFenced alphabet · Simulated cell of a fenced cell
Used byThe fenced machine halts on some padding of a word iff the machine halts on it

TheoremA fenced cell of a write is never a wall#✓fully proved

For every cell \(o\) of the simulated machine, a symbol or a blank, the fenced cell of \(o\) is not a wall.

theorem FenceSymbol.ofCell_ne_wall (o : Option Symbol) : ofCell o ≠ .wall
Uses 2 · Used by 1
Statement usesFenced alphabet · Fenced cell of a write
Used byThe fenced machine halts on some padding of a word iff the machine halts on it

DefinitionFenced input#✓fully proved

For a word \(w\) over an alphabet \(\Sigma\) and \(i, j \in \mathbb{N}\), the fenced input of \(w\) with \(i\) padding cells on the left and \(j\) on the right is the word over the fenced alphabet of \(\Sigma\) made of a wall, \(i\) left padding cells, the letters of \(w\) as symbols, \(j\) right padding cells and a wall, in this order.

def fenceInput (w : List Symbol) (i j : ℕ) : List (FenceSymbol Symbol) :=
  .wall :: List.replicate i .lpad ++ w.map .sym ++ List.replicate j .pad ++ [.wall]
Uses 1 · Used by 5
Statement usesFenced alphabet
Used byThe fenced machine halts on some padding of a word iff the machine halts on it · Emptiness of a linear bounded automaton on computable input slices is undecidable · The fenced machine halts on no padding of a word iff the machine does not halt on it · Cells of a fenced input · Length of a fenced input

TheoremCells of a fenced input#✓fully proved

Let \(w\) be a word of length \(\ell\) and \(i, j, n \in \mathbb{N}\). The cell at position \(n\), counting from \(0\), of the fenced input of \(w\) with \(i\) left and \(j\) right padding cells is the wall if \(n = 0\); a left padding cell if \(1 \le n \le i\); the letter of \(w\) at position \(n - i - 1\), also counting from \(0\), as a symbol, if \(i < n \le i + \ell\); a right padding cell if \(i + \ell < n \le i + \ell + j\); the wall if \(n = i + \ell + j + 1\); and there is no cell at a larger position \(n\).

theorem getElem?_fenceInput (w : List Symbol) (i j n : ℕ) :
    (fenceInput w i j)[n]? =
      if n = 0 then some .wall
      else if n ≤ i then some .lpad
      else if n ≤ i + w.length then (w[n - (i + 1)]?).map .sym
      else if n ≤ i + w.length + j then some .pad
      else if n = i + w.length + j + 1 then some .wall
      else none
Uses 2 · Used by 1
Statement usesFenced alphabet · Fenced input
Used byThe fenced machine halts on some padding of a word iff the machine halts on it

TheoremLength of a fenced input#✓fully proved

For a word \(w\) of length \(n\) and natural numbers \(i\) and \(j\), the fenced input of \(w\) with \(i\) padding cells on the left and \(j\) on the right has length \(i + n + j + 2\): the word, the two paddings and the two walls.

@[simp]
theorem length_fenceInput (w : List Symbol) (i j : ℕ) :
    (fenceInput w i j).length = i + w.length + j + 2
Uses 2
Statement usesFenced alphabet · Fenced input

DefinitionA transition lifted to the fenced machine#✓fully proved

A transition of a single-tape machine \(M\), made of an optional symbol to write, an optional move and an optional next state, becomes the transition of the fenced machine of \(M\) that writes the symbol, or a right padding cell where \(M\) writes a blank, makes the same move, and goes to the running state of the next state \(q\) of \(M\), or halts where \(M\) halts.

def fenceLift (r : Stmt Symbol × Option tm.State) :
    Stmt (FenceSymbol Symbol) × Option (FenceState tm.State) :=
  (⟨some (FenceSymbol.ofCell r.1.symbol), r.1.movement⟩, r.2.map .run)
Uses 3 · Used by 2
Statement usesStates of the fenced machine · Fenced alphabet · Fenced cell of a write
Used byThe fenced machine halts on some padding of a word iff the machine halts on it · The running transition of the fenced machine

DefinitionThe running transition of the fenced machine#✓fully proved

In the running state of a state \(q\) of a single-tape machine \(M\), the fenced machine of \(M\) acts on the cell under its head as follows: on a symbol \(a\) it makes the lifted transition of \(M\) in state \(q\) on \(a\); on a left or right padding cell it makes the lifted transition of \(M\) in state \(q\) on a blank; on a wall or a blank cell it leaves the cell unchanged, does not move, and enters the trap.

def fenceRun (q : tm.State) (c : Option (FenceSymbol Symbol)) :
    Stmt (FenceSymbol Symbol) × Option (FenceState tm.State) :=
  match c with
  | some (.sym a) => tm.fenceLift (tm.tr q (some a))
  | some .pad | some .lpad => tm.fenceLift (tm.tr q none)
  | _ => (⟨c, none⟩, some .trap)
Uses 3 · Used by 2
Statement usesStates of the fenced machine · Fenced alphabet · A transition lifted to the fenced machine
Used byThe fenced machine halts on some padding of a word iff the machine halts on it · The fenced machine

AbbreviationThe fenced machine#✓fully proved

For a single-tape machine \(M\) over a finite inhabited alphabet \(\Sigma\), the fenced machine of \(M\) is the single-tape machine over the fenced alphabet of \(\Sigma\) whose states are the states of the fenced machine for the states of \(M\), which starts in the first start state and acts on the cell under its head as follows. In the first start state, on a wall it moves right into the second start state, and on any other cell it leaves the cell unchanged, does not move and enters the trap. In the second start state, on a left padding cell it moves right and stays in that state, and on any other cell it makes the running transition of the initial state of \(M\). In the running state of a state \(q\) of \(M\) it makes the running transition of \(q\). In the trap it leaves the cell unchanged, does not move and stays in the trap.

So on the fenced input of a word \(w\) it moves right off the left wall and over the left padding, then runs \(M\) from its initial state, and enters the trap when it reads a wall or a blank cell. On a blank cell, in every state, it writes a blank and does not move.

abbrev fence : SingleTapeTM (FenceSymbol Symbol) where
  State := FenceState tm.State
  q₀ := .start₀
  tr
    | .start₀, c => match c with
      | some .wall => (⟨c, some .right⟩, some .start₁)
      | _ => (⟨c, none⟩, some .trap)
    | .start₁, c => match c with
      | some .lpad => (⟨c, some .right⟩, some .start₁)
      | _ => tm.fenceRun tm.q₀ c
    | .run q, c => tm.fenceRun q c
    | .trap, c => (⟨c, none⟩, some .trap)
Uses 3 · Used by 4
Statement usesStates of the fenced machine · Fenced alphabet · The running transition of the fenced machine
Used byThe fenced machine halts on some padding of a word iff the machine halts on it · Emptiness of a linear bounded automaton on computable input slices is undecidable · The fenced machine halts on no padding of a word iff the machine does not halt on it · The fenced machine is a linear bounded automaton

TheoremThe fenced machine is a linear bounded automaton#✓fully proved

For every single-tape Turing machine \(M\), the fenced machine of \(M\) is a linear bounded automaton.

On a blank cell, in every state, the fenced machine writes a blank and does not move.

theorem isLBA_fence : (fence tm).IsLBA
Uses 5 · Used by 1
Statement usesFenced alphabet · Linear bounded automaton · The fenced machine
Proof usesStates of the fenced machine · A machine that, on a blank cell, writes a blank and does not move is a linear bounded automaton
Used byEmptiness of a linear bounded automaton on computable input slices is undecidable
17 fully proved

Correctness

TheoremThe fenced machine halts on some padding of a word iff the machine halts on it#✓fully proved

Let \(M\) be a single-tape machine over a finite inhabited alphabet and \(w\) a word over that alphabet. The fenced machine of \(M\) halts on the fenced input of \(w\) with \(i\) padding cells on the left and \(j\) on the right for some \(i, j \in \mathbb{N}\) if and only if \(M\) halts on \(w\).

A halting run of \(M\) of \(n\) steps stays within \(n\) cells of its start, so it runs unchanged inside the walls of the fenced input of \(w\) with \(n + 1\) padding cells on each side; conversely, the fenced machine halts only by simulating a halting run of \(M\).

theorem exists_haltsOn_fence_iff (w : List Symbol) :
    (∃ i j, (fence tm).HaltsOn (fenceInput w i j)) ↔ tm.HaltsOn w
Uses 24 · Used by 1
Statement usesFenced alphabet · Halting on an input · The fenced machine · Fenced input
Proof usesCells of an input tape · Cells after \(n\) moves to the right · Cells after a write and an optional move · Offset of an optional head move · The offset of an optional move is at most one · Cell view of a two-way tape · States of the fenced machine · Fenced cell of a write · A fenced cell of a write is never a wall · Simulated cell of a fenced cell · Reading back a copied cell · Reading back a fenced cell of a write · Halting from a configuration · A transition lifted to the fenced machine · The running transition of the fenced machine · Cells of a fenced input · Halting from a configuration is invariant along a run · Configurations with the same successor halt together · Halting on an input is halting from the initial configuration · One step of a single-tape Turing machine
Used byThe fenced machine halts on no padding of a word iff the machine does not halt on it

TheoremThe fenced machine halts on no padding of a word iff the machine does not halt on it#✓fully proved

Let \(M\) be a single-tape machine over a finite inhabited alphabet and \(w\) a word over that alphabet. The fenced machine of \(M\) halts on none of the fenced inputs of \(w\), with \(i\) padding cells on the left and \(j\) on the right for \(i, j \in \mathbb{N}\), if and only if \(M\) does not halt on \(w\).

theorem forall_not_haltsOn_fence_iff (w : List Symbol) :
    (∀ i j, ¬(fence tm).HaltsOn (fenceInput w i j)) ↔ ¬tm.HaltsOn w
Uses 5 · Used by 1
Statement usesFenced alphabet · Halting on an input · The fenced machine · Fenced input
Proof usesThe fenced machine halts on some padding of a word iff the machine halts on it
Used byEmptiness of a linear bounded automaton on computable input slices is undecidable

Emptiness of an LBA on computable input slices is undecidable

TheoremEmptiness of a linear bounded automaton on computable input slices is undecidable#✓fully proved

There exist a finite inhabited alphabet \(\Gamma\) with a primitive recursive encoding, a linear bounded automaton \(F\) over the fenced alphabet of \(\Gamma\), and a primitive recursive map \(e\) from codes of partial recursive functions to words over \(\Gamma\), such that the set of codes \(c\) for which \(F\) halts on none of the fenced inputs of \(e(c)\), with \(i\) padding cells on the left and \(j\) on the right for any \(i, j \in \mathbb{N}\), is neither computable nor recursively enumerable.

This is the code-free form of Sipser, Theorem 5.10. Take for \(F\) the fenced machine of a single-tape recognizer \(R\) of the set of codes that halt on input \(0\), and for \(e(c)\) the input of \(c\) to \(R\): then \(F\) halts on no fenced input of \(e(c)\) iff \(c\) does not halt on \(0\). The word \(e(c)\) does not see the paddings \(i\) and \(j\), so \(F\) itself runs the computation within the space they give.

Sipser's \(E_{\mathrm{LBA}}\) is a language of machine descriptions, the LBAs with empty language; without a type of codes for machines, this is the form available. Each slice, the set of fenced inputs of \(e(c)\) over all paddings, is regular because of its shape: a wall, any number of left padding cells, the word \(e(c)\), any number of right padding cells and a wall. Informally: with codes of machines, the LBA that checks that its input lies in the slice of \(c\) and then runs \(F\) has empty language iff \(F\) halts on no input of the slice, and \(E_{\mathrm{LBA}}\) is undecidable by the same reduction.

theorem exists_isLBA_not_computablePred_forall_not_haltsOn :
    ∃ (Γ : Type) (_ : Inhabited Γ) (_ : Fintype Γ) (_ : Primcodable Γ)
      (F : SingleTapeTM (FenceSymbol Γ)) (e : Nat.Partrec.Code → List Γ), F.IsLBA ∧ Primrec e ∧
      ¬ComputablePred (fun c ↦ ∀ i j, ¬F.HaltsOn (fenceInput (e c) i j)) ∧
      ¬REPred (fun c ↦ ∀ i j, ¬F.HaltsOn (fenceInput (e c) i j))
Uses 10
Statement usesFenced alphabet · Halting on an input · Linear bounded automaton · Fenced input
Proof usesPredicates recognizable by a single-tape Turing machine · The halting problem for partial recursive codes is recognizable on single-tape machines · The fenced machine · The fenced machine halts on no padding of a word iff the machine does not halt on it · The fenced machine is a linear bounded automaton · Binary encoding, least significant bit first

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.