Linear bounded automata

InductiveBoundary tag of a linear bounded automaton head#✓fully proved

Where the head sits relative to the tape boundaries: strictly inside the tape, on the first cell, on the last cell, or on the only cell of a one-cell tape. The transition function observes this tag, so the machine can tell the two ends of its tape apart from interior cells.

inductive LBABoundary where
  /-- Strictly inside the tape: not the first and not the last cell. -/
  | middle : LBABoundary
  /-- On the first cell of a tape of length at least two. -/
  | left : LBABoundary
  /-- On the last cell of a tape of length at least two. -/
  | right : LBABoundary
  /-- On the only cell of a one-cell tape. -/
  | both : LBABoundary
  deriving DecidableEq

Used by 53

Used byActivation rules of the LBA grammar · Cell symbol of the LBA grammar · Cell tuple as a grammar symbol · Conversion rules of the LBA grammar · Non-head or accepting cells convert to terminals · An LBA step is a grammar derivation step on encodings · Generated form derives the initial configuration encoding · The generator derives the middle cells and itself · The generator derives the full tail of cells · The start symbol derives the generated form of a word · Tail cells derive their activated encoding · Cell tuples of an LBA configuration from an offset · Every cell of a configuration encoding is active · Head states in a configuration encoding · Configuration encoded as a sentential form · Generated cells of a word · Generated sentential form of a word · Generation rules of the LBA grammar · Entries of the cell-tuple encoding · Entries of a configuration encoding · If the LBA accepts a nonempty word, the grammar derives it · The grammar of an LBA is context-sensitive · Nonterminals of the grammar of a linear bounded automaton · Length of the cell-tuple encoding · Length of a configuration encoding · Linear bounded automaton · Original symbols of an encoding are the input word · The start rule is a generation rule of the LBA grammar · The activation rule belongs to the LBA grammar · The accepting conversion rule belongs to the LBA grammar · The non-head conversion rule belongs to the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar · Left transitions give simulation rules · Right transitions give simulation rules · Stay transitions give simulation rules · Boundary tag of a head position · Boundary tag on a one-cell tape · Boundary tag on the first cell of a longer tape · Boundary tag at an interior head position · Boundary tag on the last cell of a longer tape · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move · One step of a linear bounded automaton · LBA steps keep the head on the tape · LBA steps preserve tape length · Tail generated cells of a word · Middle generated cells of a word · Tail generated sentential form of a word · Middle generated sentential form of a word

DefinitionBoundary tag of a head position#✓fully proved

The boundary tag of head position h on a tape of length n.

def LBABoundary.ofHead (h n : ℕ) : LBABoundary :=
  if h = 0 then (if n = 1 then .both else .left)
  else if h + 1 = n then .right else .middle

Uses 1 · Used by 16

Statement usesBoundary tag of a linear bounded automaton head

Used byAn LBA step is a grammar derivation step on encodings · Generated form derives the initial configuration encoding · Tail cells derive their activated encoding · Cell tuples of an LBA configuration from an offset · Every cell of a configuration encoding is active · Head states in a configuration encoding · Entries of the cell-tuple encoding · Entries of a configuration encoding · Original symbols of an encoding are the input word · Boundary tag on a one-cell tape · Boundary tag on the first cell of a longer tape · Boundary tag at an interior head position · Boundary tag on the last cell of a longer tape · One step of a linear bounded automaton · LBA steps keep the head on the tape · LBA steps preserve tape length

TheoremBoundary tag on a one-cell tape#✓fully proved

The boundary tag at the head of a one-cell tape.

theorem LBABoundary.ofHead_eq_both {h n : ℕ} (h0 : h = 0) (hn : n = 1) :
    LBABoundary.ofHead h n = .both

Uses 2 · Used by 1

Statement usesBoundary tag of a linear bounded automaton head · Boundary tag of a head position

Used byGenerated form derives the initial configuration encoding

TheoremBoundary tag on the first cell of a longer tape#✓fully proved

The boundary tag at the head of the first cell of a longer tape.

theorem LBABoundary.ofHead_eq_left {h n : ℕ} (h0 : h = 0) (hn : n ≠ 1) :
    LBABoundary.ofHead h n = .left

Uses 2

Statement usesBoundary tag of a linear bounded automaton head · Boundary tag of a head position

TheoremBoundary tag on the last cell of a longer tape#✓fully proved

The boundary tag at the head of the last cell of a longer tape.

theorem LBABoundary.ofHead_eq_right {h n : ℕ} (h0 : h ≠ 0) (hn : h + 1 = n) :
    LBABoundary.ofHead h n = .right

Uses 2 · Used by 1

Statement usesBoundary tag of a linear bounded automaton head · Boundary tag of a head position

Used byTail cells derive their activated encoding

TheoremBoundary tag at an interior head position#✓fully proved

The boundary tag at an interior head position.

theorem LBABoundary.ofHead_eq_middle {h n : ℕ} (h0 : h ≠ 0) (hn : h + 1 ≠ n) :
    LBABoundary.ofHead h n = .middle

Uses 2 · Used by 1

Statement usesBoundary tag of a linear bounded automaton head · Boundary tag of a head position

Used byTail cells derive their activated encoding

InductiveHead move of a linear bounded automaton#✓fully proved

A head move of a linear bounded automaton: left, stay, or right.

inductive LBAMove where
  /-- Move the head one cell to the left. -/
  | left : LBAMove
  /-- Leave the head on the same cell. -/
  | stay : LBAMove
  /-- Move the head one cell to the right. -/
  | right : LBAMove
  deriving DecidableEq

Used by 14

Used byAn LBA step is a grammar derivation step on encodings · The grammar of an LBA is context-sensitive · Legal head move of a linear bounded automaton · Linear bounded automaton · Left transitions give simulation rules · Right transitions give simulation rules · Stay transitions give simulation rules · Head position after a move · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move · One step of a linear bounded automaton · LBA steps keep the head on the tape · LBA steps preserve tape length

DefinitionHead position after a move#✓fully proved

The head position after a move: left decrements, stay keeps, right increments.

def LBAMove.moveHead (mv : LBAMove) (h : ℕ) : ℕ :=
  match mv with
  | .left => h - 1
  | .stay => h
  | .right => h + 1

Uses 1 · Used by 4

Statement usesHead move of a linear bounded automaton

Used byAn LBA step is a grammar derivation step on encodings · One step of a linear bounded automaton · LBA steps keep the head on the tape · LBA steps preserve tape length

DefinitionLegal head move of a linear bounded automaton#✓fully proved

A move is legal from the head position h on a tape of length n when the source head is on the tape and the new head position is still on the tape. In particular a left move from an out-of-bounds head is illegal, even though the truncated new head h - 1 would still be out of bounds: legality requires h < n for left moves as well.

def LBAMove.legal (mv : LBAMove) (h n : ℕ) : Prop :=
  match mv with
  | .left => 0 < h ∧ h < n
  | .stay => h < n
  | .right => h + 1 < n

Uses 1 · Used by 4

Statement usesHead move of a linear bounded automaton

Used byAn LBA step is a grammar derivation step on encodings · One step of a linear bounded automaton · LBA steps keep the head on the tape · LBA steps preserve tape length

StructureLinear bounded automaton#✓fully proved

A linear bounded automaton: a nondeterministic Turing machine whose tape is the input word. The transition function gives, for a state, the symbol under the head (none for a blank cell), and the boundary tag of the head position, the finite set of possible next states, symbols to write (none for a blank), and head moves. The boundary tag is what lets the machine detect the ends of its tape: without it the model could not recognize general context-sensitive languages. A move that would take the head off the tape is not a step.

structure LinearBoundedAutomaton (Q Γ : Type*) where
  /-- The initial state. -/
  q₀ : Q
  /-- The accepting state. -/
  qAcc : Q
  /-- The transition function: from a state, the symbol under the head,
  and the boundary tag of the head position, the finite set of possible
  (next state, written symbol, head move) triples. -/
  delta : Q → Option Γ → LBABoundary → Finset (Q × Option Γ × LBAMove)

Uses 2 · Used by 53

Statement usesBoundary tag of a linear bounded automaton head · Head move of a linear bounded automaton

Used byAcceptance by a linear bounded automaton · All rules of the LBA grammar · Conversion rules of the LBA grammar · Derivations compose under concatenation · Derivations extend by a left context · Derivations extend by a right context · Non-head or accepting cells convert to terminals · Runs of an LBA give grammar derivations · An LBA step is a grammar derivation step on encodings · Generated form derives the initial configuration encoding · The generator derives the middle cells and itself · The generator derives the full tail of cells · Replacing a block by a rule is a derivation step · Setting one list position by a production is a derivation step · Setting two adjacent list positions by a production is a derivation step · Two-cell replacement at indices \(i\) and \(j = i + 1\) · Replacing a single cell is a derivation step · Singleton-to-singleton productions are derivation steps · The start symbol derives the generated form of a word · Tail cells derive their activated encoding · Transitivity of grammar derivations · Replacing two consecutive cells is a derivation step · Configuration encoded as a sentential form · Generated cells of a word · Generated sentential form of a word · Generation rules of the LBA grammar · Entries of a configuration encoding · Initial configuration of a linear bounded automaton · Language of a linear bounded automaton · If the LBA accepts a nonempty word, the grammar derives it · The grammar of an LBA · The grammar of an LBA is context-sensitive · Length of a configuration encoding · The start rule is a generation rule of the LBA grammar · The activation rule belongs to the LBA grammar · The accepting conversion rule belongs to the LBA grammar · The non-head conversion rule belongs to the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar · Left transitions give simulation rules · Right transitions give simulation rules · Stay transitions give simulation rules · Reachable LBA configurations keep the tape length and the head on the tape · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move · One step of a linear bounded automaton · LBA steps keep the head on the tape · LBA steps preserve tape length · Tail generated sentential form of a word · Middle generated sentential form of a word

StructureConfiguration of a linear bounded automaton#✓fully proved

A configuration of a linear bounded automaton: the state, the tape (a list of cells, one per input cell; none is a blank), and the head position.

structure LBAConfig (Q Γ : Type*) where
  /-- The current state. -/
  state : Q
  /-- The tape: one cell per input cell. -/
  tape : List (Option Γ)
  /-- The head position, an index into the tape. -/
  head : ℕ

Used by 13

Used byAcceptance by a linear bounded automaton · Runs of an LBA give grammar derivations · An LBA step is a grammar derivation step on encodings · Generated form derives the initial configuration encoding · Configuration encoded as a sentential form · Entries of a configuration encoding · Initial configuration of a linear bounded automaton · If the LBA accepts a nonempty word, the grammar derives it · Length of a configuration encoding · Reachable LBA configurations keep the tape length and the head on the tape · One step of a linear bounded automaton · LBA steps keep the head on the tape · LBA steps preserve tape length

DefinitionInitial configuration of a linear bounded automaton#✓fully proved

The initial configuration on the input w: the initial state, the tape w itself (no blanks), the head on the first cell.

def initCfg (w : List Γ) : LBAConfig Q Γ :=
  ⟨M.q₀, w.map some, 0⟩

Uses 2 · Used by 5

Statement usesConfiguration of a linear bounded automaton · Linear bounded automaton

Used byAcceptance by a linear bounded automaton · Runs of an LBA give grammar derivations · Generated form derives the initial configuration encoding · If the LBA accepts a nonempty word, the grammar derives it · Reachable LBA configurations keep the tape length and the head on the tape

DefinitionOne step of a linear bounded automaton#✓fully proved

One step of the machine: choose a transition for the current state, the symbol under the head, and its boundary tag, write the symbol, move the head legally. A step from a configuration whose head is off the tape is impossible: legality requires the source head to be on the tape.

def Step (c c' : LBAConfig Q Γ) : Prop :=
  ∃ (q' : Q) (b' : Option Γ) (mv : LBAMove),
    (q', b', mv) ∈
      M.delta c.state (c.tape[c.head]?).join
        (LBABoundary.ofHead c.head c.tape.length) ∧
    c' = ⟨q', c.tape.set c.head b', mv.moveHead c.head⟩ ∧
    mv.legal c.head c.tape.length

Uses 7 · Used by 7

Statement usesBoundary tag of a linear bounded automaton head · Boundary tag of a head position · Configuration of a linear bounded automaton · Head move of a linear bounded automaton · Legal head move of a linear bounded automaton · Head position after a move · Linear bounded automaton

Used byAcceptance by a linear bounded automaton · Runs of an LBA give grammar derivations · An LBA step is a grammar derivation step on encodings · If the LBA accepts a nonempty word, the grammar derives it · Reachable LBA configurations keep the tape length and the head on the tape · LBA steps keep the head on the tape · LBA steps preserve tape length

DefinitionAcceptance by a linear bounded automaton#✓fully proved

M accepts w when some run from the initial configuration on w reaches a configuration in the accepting state.

def Accepts (w : List Γ) : Prop :=
  ∃ c : LBAConfig Q Γ, Relation.ReflTransGen M.Step (M.initCfg w) c ∧
    c.state = M.qAcc

Uses 4 · Used by 2

Statement usesConfiguration of a linear bounded automaton · Linear bounded automaton · One step of a linear bounded automaton · Initial configuration of a linear bounded automaton

Used byLanguage of a linear bounded automaton · If the LBA accepts a nonempty word, the grammar derives it

DefinitionLanguage of a linear bounded automaton#✓fully proved

The language of M: the words it accepts.

def language : Set (List Γ) :=
  {w | M.Accepts w}

Uses 2

Statement usesLinear bounded automaton · Acceptance by a linear bounded automaton

InductiveNonterminals of the grammar of a linear bounded automaton#✓fully proved

The nonterminals of the grammar of an LBA: a cell, a generator, and the start symbol. A cell records the original input symbol, the current tape symbol, the head state if the head is on the cell, whether the cell is active (simulation acts only on active cells), and the boundary tag of its position (so simulation can apply the boundary-aware transitions).

inductive LBANT (Γ Q : Type*) where
  /-- A tape cell: original symbol, current symbol, head state, active,
  boundary tag. -/
  | cell (orig : Γ) (cur : Option Γ) (st : Option Q) (active : Bool)
      (bnd : LBABoundary) : LBANT Γ Q
  /-- The generator: it produces the remaining cells, then disappears. -/
  | gen : LBANT Γ Q
  /-- The start symbol: the initial nonterminal of the grammar. -/
  | start : LBANT Γ Q
  deriving DecidableEq, Fintype

Uses 1 · Used by 52

Statement usesBoundary tag of a linear bounded automaton head

Used byActivation rules of the LBA grammar · All rules of the LBA grammar · Cell symbol of the LBA grammar · Cell tuple as a grammar symbol · Conversion rules of the LBA grammar · Derivations compose under concatenation · Derivations extend by a left context · Derivations extend by a right context · Non-head or accepting cells convert to terminals · Runs of an LBA give grammar derivations · An LBA step is a grammar derivation step on encodings · Generated form derives the initial configuration encoding · The generator derives the middle cells and itself · The generator derives the full tail of cells · Replacing a block by a rule is a derivation step · Setting one list position by a production is a derivation step · Setting two adjacent list positions by a production is a derivation step · Two-cell replacement at indices \(i\) and \(j = i + 1\) · Replacing a single cell is a derivation step · Singleton-to-singleton productions are derivation steps · The start symbol derives the generated form of a word · Tail cells derive their activated encoding · Transitivity of grammar derivations · Replacing two consecutive cells is a derivation step · Configuration encoded as a sentential form · Generated sentential form of a word · Generation rules of the LBA grammar · Generator symbol of the LBA grammar · Entries of a configuration encoding · If the LBA accepts a nonempty word, the grammar derives it · The grammar of an LBA · The grammar of an LBA is context-sensitive · Length of a configuration encoding · Original symbols of an encoding are the input word · The start rule is a generation rule of the LBA grammar · The activation rule belongs to the LBA grammar · The accepting conversion rule belongs to the LBA grammar · The non-head conversion rule belongs to the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar · Left transitions give simulation rules · Right transitions give simulation rules · Stay transitions give simulation rules · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move · Start symbol of the LBA grammar · Tail generated sentential form of a word · Middle generated sentential form of a word · Terminal symbol of the LBA grammar

AbbreviationCell symbol of the LBA grammar#✓fully proved

A grammar symbol for the LBA grammar: a cell as a nonterminal.

abbrev cellSym (orig : Γ) (cur : Option Γ) (st : Option Q) (active : Bool)
    (bnd : LBABoundary) : Symbol Γ (LBANT Γ Q) :=
  .nonterminal (.cell orig cur st active bnd)

Uses 2 · Used by 27

Statement usesBoundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton

Used byActivation rules of the LBA grammar · Cell tuple as a grammar symbol · Conversion rules of the LBA grammar · Non-head or accepting cells convert to terminals · An LBA step is a grammar derivation step on encodings · Generated form derives the initial configuration encoding · The generator derives the middle cells and itself · The generator derives the full tail of cells · The start symbol derives the generated form of a word · Tail cells derive their activated encoding · Generation rules of the LBA grammar · Entries of a configuration encoding · The grammar of an LBA is context-sensitive · The start rule is a generation rule of the LBA grammar · The activation rule belongs to the LBA grammar · The accepting conversion rule belongs to the LBA grammar · The non-head conversion rule belongs to the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar · Left transitions give simulation rules · Right transitions give simulation rules · Stay transitions give simulation rules · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move

AbbreviationStart symbol of the LBA grammar#✓fully proved

The start symbol as a grammar symbol.

abbrev startSym : Symbol Γ (LBANT Γ Q) :=
  .nonterminal .start

Uses 1 · Used by 9

Statement usesNonterminals of the grammar of a linear bounded automaton

Used byThe start symbol derives the generated form of a word · Generation rules of the LBA grammar · If the LBA accepts a nonempty word, the grammar derives it · The grammar of an LBA is context-sensitive · The start rule is a generation rule of the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar

AbbreviationGenerator symbol of the LBA grammar#✓fully proved

The generator as a grammar symbol.

abbrev genSym : Symbol Γ (LBANT Γ Q) :=
  .nonterminal .gen

Uses 1 · Used by 10

Statement usesNonterminals of the grammar of a linear bounded automaton

Used byThe generator derives the middle cells and itself · The generator derives the full tail of cells · The start symbol derives the generated form of a word · Generation rules of the LBA grammar · The grammar of an LBA is context-sensitive · The start rule is a generation rule of the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar

AbbreviationTerminal symbol of the LBA grammar#✓fully proved

A terminal symbol of the grammar.

abbrev termSym (a : Γ) : Symbol Γ (LBANT Γ Q) :=
  .terminal a

Uses 1 · Used by 7

Statement usesNonterminals of the grammar of a linear bounded automaton

Used byConversion rules of the LBA grammar · Non-head or accepting cells convert to terminals · If the LBA accepts a nonempty word, the grammar derives it · The grammar of an LBA is context-sensitive · Original symbols of an encoding are the input word · The accepting conversion rule belongs to the LBA grammar · The non-head conversion rule belongs to the LBA grammar

DefinitionGeneration rules of the LBA grammar#✓fully proved

The generation rules: the start symbol produces the first cell and the generator (or, for a one-cell word, the first cell alone, tagged both); the generator produces a middle non-head cell and itself, or a final right non-head cell. The first cell of a longer word is tagged left.

noncomputable def genRules (M : LinearBoundedAutomaton Q Γ) : List (List (Symbol Γ (LBANT Γ Q)) × List (Symbol Γ (LBANT Γ Q))) :=
  (Finset.univ.toList : List Γ).flatMap fun a ↦
    [([startSym (Γ := Γ) (Q := Q)],
       [cellSym a (some a) (some M.q₀) false .left, genSym]),
     ([startSym (Γ := Γ) (Q := Q)],
       [cellSym a (some a) (some M.q₀) false .both]),
     ([genSym (Γ := Γ) (Q := Q)],
       [cellSym a (some a) none false .middle, genSym]),
     ([genSym (Γ := Γ) (Q := Q)],
       [cellSym a (some a) none false .right])]

Uses 6 · Used by 13

Statement usesBoundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar · Generator symbol of the LBA grammar · Start symbol of the LBA grammar

Used byAll rules of the LBA grammar · The grammar of an LBA is context-sensitive · The start rule is a generation rule of the LBA grammar · The activation rule belongs to the LBA grammar · The accepting conversion rule belongs to the LBA grammar · The non-head conversion rule belongs to the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar · Left transitions give simulation rules · Right transitions give simulation rules · Stay transitions give simulation rules

DefinitionActivation rules of the LBA grammar#✓fully proved

The activation rules: an inactive cell becomes active, keeping its original, current, head state, and boundary tag.

noncomputable def activateRules :
    List (List (Symbol Γ (LBANT Γ Q)) × List (Symbol Γ (LBANT Γ Q))) :=
  (Finset.univ.toList : List (Γ × Option Γ × Option Q × LBABoundary)).flatMap
    fun ⟨a, cur, st, bnd⟩ ↦
      [([cellSym a cur st false bnd], [cellSym a cur st true bnd])]

Uses 3 · Used by 12

Statement usesBoundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Cell symbol of the LBA grammar

Used byAll rules of the LBA grammar · The grammar of an LBA is context-sensitive · The activation rule belongs to the LBA grammar · The accepting conversion rule belongs to the LBA grammar · The non-head conversion rule belongs to the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar · Left transitions give simulation rules · Right transitions give simulation rules · Stay transitions give simulation rules

DefinitionSimulation rules for a stay move#✓fully proved

The simulation rules for a stay move: the head cell rewrites its current symbol and state, staying active, keeping its boundary tag.

noncomputable def simStayRules (M : LinearBoundedAutomaton Q Γ) :
    List (List (Symbol Γ (LBANT Γ Q)) × List (Symbol Γ (LBANT Γ Q))) :=
  (Finset.univ.toList : List (Q × Option Γ × Γ × LBABoundary)).flatMap
    fun ⟨q, read, orig, bnd⟩ ↦
      ((M.delta q read bnd).toList).flatMap fun ⟨q', write, mv⟩ ↦
        match mv with
        | .stay => [([cellSym orig read (some q) true bnd],
            [cellSym orig write (some q') true bnd])]
        | _ => []

Uses 5 · Used by 12

Statement usesBoundary tag of a linear bounded automaton head · Head move of a linear bounded automaton · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar

Used byAll rules of the LBA grammar · The grammar of an LBA is context-sensitive · The activation rule belongs to the LBA grammar · The accepting conversion rule belongs to the LBA grammar · The non-head conversion rule belongs to the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar · Left transitions give simulation rules · Right transitions give simulation rules · Stay transitions give simulation rules

DefinitionSimulation rules for a right move#✓fully proved

The simulation rules for a right move: the head cell rewrites its current symbol and loses the head; the neighbouring cell gains the head. Both cells keep their boundary tags.

noncomputable def simRightRules (M : LinearBoundedAutomaton Q Γ) :
    List (List (Symbol Γ (LBANT Γ Q)) × List (Symbol Γ (LBANT Γ Q))) :=
  (Finset.univ.toList :
      List (Q × Option Γ × Γ × Γ × Option Γ × LBABoundary × LBABoundary)).flatMap
    fun ⟨q, read, orig, orig₂, cur₂, bnd, bnd₂⟩ ↦
      ((M.delta q read bnd).toList).flatMap fun ⟨q', write, mv⟩ ↦
        match mv with
        | .right => [([cellSym orig read (some q) true bnd,
              cellSym orig₂ cur₂ none true bnd₂],
            [cellSym orig write none true bnd,
              cellSym orig₂ cur₂ (some q') true bnd₂])]
        | _ => []

Uses 5 · Used by 12

Statement usesBoundary tag of a linear bounded automaton head · Head move of a linear bounded automaton · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar

Used byAll rules of the LBA grammar · The grammar of an LBA is context-sensitive · The activation rule belongs to the LBA grammar · The accepting conversion rule belongs to the LBA grammar · The non-head conversion rule belongs to the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar · Left transitions give simulation rules · Right transitions give simulation rules · Stay transitions give simulation rules

DefinitionSimulation rules for a left move#✓fully proved

The simulation rules for a left move: the neighbouring cell gains the head; the head cell rewrites its current symbol and loses the head. Both cells keep their boundary tags.

noncomputable def simLeftRules (M : LinearBoundedAutomaton Q Γ) :
    List (List (Symbol Γ (LBANT Γ Q)) × List (Symbol Γ (LBANT Γ Q))) :=
  (Finset.univ.toList :
      List (Q × Option Γ × Γ × Γ × Option Γ × LBABoundary × LBABoundary)).flatMap
    fun ⟨q, read, orig, orig₂, cur₂, bnd, bnd₂⟩ ↦
      ((M.delta q read bnd).toList).flatMap fun ⟨q', write, mv⟩ ↦
        match mv with
        | .left => [([cellSym orig₂ cur₂ none true bnd₂,
              cellSym orig read (some q) true bnd],
            [cellSym orig₂ cur₂ (some q') true bnd₂,
              cellSym orig write none true bnd])]
        | _ => []

Uses 5 · Used by 12

Statement usesBoundary tag of a linear bounded automaton head · Head move of a linear bounded automaton · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar

Used byAll rules of the LBA grammar · The grammar of an LBA is context-sensitive · The activation rule belongs to the LBA grammar · The accepting conversion rule belongs to the LBA grammar · The non-head conversion rule belongs to the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar · Left transitions give simulation rules · Right transitions give simulation rules · Stay transitions give simulation rules

DefinitionConversion rules of the LBA grammar#✓fully proved

The conversion rules: an active cell becomes its original terminal. The head cell converts only in the accepting state, so a terminal word is produced only from an accepting configuration. The boundary tag is discarded on conversion.

noncomputable def convRules (M : LinearBoundedAutomaton Q Γ) :
    List (List (Symbol Γ (LBANT Γ Q)) × List (Symbol Γ (LBANT Γ Q))) :=
  (Finset.univ.toList : List (Γ × Option Γ × LBABoundary)).flatMap
    fun ⟨a, cur, bnd⟩ ↦
      [([cellSym a cur (some M.qAcc) true bnd], [termSym a]),
       ([cellSym a cur none true bnd], [termSym a])]

Uses 5 · Used by 10

Statement usesBoundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar · Terminal symbol of the LBA grammar

Used byAll rules of the LBA grammar · The grammar of an LBA is context-sensitive · The activation rule belongs to the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar · Left transitions give simulation rules · Right transitions give simulation rules · Stay transitions give simulation rules

DefinitionAll rules of the LBA grammar#✓fully proved

All the rules of the grammar.

noncomputable def allRules (M : LinearBoundedAutomaton Q Γ) : List (List (Symbol Γ (LBANT Γ Q)) × List (Symbol Γ (LBANT Γ Q))) :=
  genRules M ++ activateRules ++ simStayRules M ++ simRightRules M ++
    simLeftRules M ++ convRules M

Uses 8 · Used by 9

Statement usesNonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Activation rules of the LBA grammar · Conversion rules of the LBA grammar · Generation rules of the LBA grammar · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move

Used byThe grammar of an LBA · The grammar of an LBA is context-sensitive · The activation rule belongs to the LBA grammar · The accepting conversion rule belongs to the LBA grammar · The non-head conversion rule belongs to the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar

DefinitionThe grammar of an LBA#✓fully proved

The grammar whose rules are the generation, activation, simulation, and conversion rules above, starting from the start symbol.

noncomputable def lbaGrammar (M : LinearBoundedAutomaton Q Γ) : CSGrammar Γ (LBANT Γ Q) where
  rules := allRules M
  initial := .start

Uses 4 · Used by 31

Statement usesUnrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · All rules of the LBA grammar

Used byDerivations compose under concatenation · Derivations extend by a left context · Derivations extend by a right context · Non-head or accepting cells convert to terminals · Runs of an LBA give grammar derivations · An LBA step is a grammar derivation step on encodings · Generated form derives the initial configuration encoding · The generator derives the middle cells and itself · The generator derives the full tail of cells · Replacing a block by a rule is a derivation step · Setting one list position by a production is a derivation step · Setting two adjacent list positions by a production is a derivation step · Two-cell replacement at indices \(i\) and \(j = i + 1\) · Replacing a single cell is a derivation step · Singleton-to-singleton productions are derivation steps · The start symbol derives the generated form of a word · Tail cells derive their activated encoding · Transitivity of grammar derivations · Replacing two consecutive cells is a derivation step · If the LBA accepts a nonempty word, the grammar derives it · The grammar of an LBA is context-sensitive · The activation rule belongs to the LBA grammar · The accepting conversion rule belongs to the LBA grammar · The non-head conversion rule belongs to the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar · Left transitions give simulation rules · Right transitions give simulation rules · Stay transitions give simulation rules

TheoremThe start rule is a generation rule of the LBA grammar#✓fully proved

The first generation rule is a rule of the grammar.

theorem mem_genRules_start (a : Γ) :
    ([startSym (Γ := Γ) (Q := Q)],
      [cellSym a (some a) (some M.q₀) false .left, genSym (Γ := Γ) (Q := Q)]) ∈
      M.genRules

Uses 7

Statement usesBoundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar · Generation rules of the LBA grammar · Generator symbol of the LBA grammar · Start symbol of the LBA grammar

TheoremThe grammar of an LBA is context-sensitive#✓fully proved

Every production has a nonterminal on its left side and does not shrink.

theorem lbaGrammar_contextSensitive : IsContextSensitive M.lbaGrammar

Uses 19

Statement usesContext-sensitive grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · The grammar of an LBA

Proof usesUnrestricted grammar · Boundary tag of a linear bounded automaton head · Head move of a linear bounded automaton · Activation rules of the LBA grammar · All rules of the LBA grammar · Cell symbol of the LBA grammar · Conversion rules of the LBA grammar · Generation rules of the LBA grammar · Generator symbol of the LBA grammar · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move · Start symbol of the LBA grammar · Terminal symbol of the LBA grammar · Nonterminal grammar symbols

DefinitionCell tuples of an LBA configuration from an offset#✓fully proved

The cells of a configuration, as a list of cell tuples: original symbol, current symbol, head state, active, boundary tag. The head is given as some i for the head position, or none once it has been passed. The start index is the position of the first cell in the whole word and total is the whole word's length, so the boundary tag of the cell at offset j is ofHead (start + j) total.

def encodeCellsAux : List Γ → List (Option Γ) → Option ℕ → Q → ℕ → ℕ →
    List (Γ × Option Γ × Option Q × Bool × LBABoundary)
  | [], _, _, _, _, _ => []
  | _ :: _, [], _, _, _, _ => []
  | a :: w, cur :: tape, some 0, q, i, total =>
      (a, cur, some q, true, LBABoundary.ofHead i total) ::
        encodeCellsAux w tape none q (i + 1) total
  | a :: w, cur :: tape, some (k + 1), q, i, total =>
      (a, cur, none, true, LBABoundary.ofHead i total) ::
        encodeCellsAux w tape (some k) q (i + 1) total
  | a :: w, cur :: tape, none, q, i, total =>
      (a, cur, none, true, LBABoundary.ofHead i total) ::
        encodeCellsAux w tape none q (i + 1) total

Uses 2 · Used by 11

Statement usesBoundary tag of a linear bounded automaton head · Boundary tag of a head position

Used byGenerated form derives the initial configuration encoding · Tail cells derive their activated encoding · Every cell of a configuration encoding is active · Head states in a configuration encoding · Configuration encoded as a sentential form · Entries of the cell-tuple encoding · Entries of a configuration encoding · If the LBA accepts a nonempty word, the grammar derives it · Length of the cell-tuple encoding · Length of a configuration encoding · Original symbols of an encoding are the input word

DefinitionCell tuple as a grammar symbol#✓fully proved

A cell tuple as a grammar symbol.

def cellTupleSym : Γ × Option Γ × Option Q × Bool × LBABoundary →
    Symbol Γ (LBANT Γ Q)
  | ⟨orig, cur, st, active, bnd⟩ => cellSym orig cur st active bnd

Uses 3 · Used by 13

Statement usesBoundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Cell symbol of the LBA grammar

Used byNon-head or accepting cells convert to terminals · Generated form derives the initial configuration encoding · The generator derives the middle cells and itself · The generator derives the full tail of cells · The start symbol derives the generated form of a word · Tail cells derive their activated encoding · Configuration encoded as a sentential form · Generated sentential form of a word · Entries of a configuration encoding · If the LBA accepts a nonempty word, the grammar derives it · Length of a configuration encoding · Tail generated sentential form of a word · Middle generated sentential form of a word

DefinitionConfiguration encoded as a sentential form#✓fully proved

A configuration as a sentential form: the cells of its tape, with the original symbols taken from the input word w.

def encodeCfg (_M : LinearBoundedAutomaton Q Γ) (w : List Γ) (cfg : LBAConfig Q Γ) :
    List (Symbol Γ (LBANT Γ Q)) :=
  (encodeCellsAux w cfg.tape (if cfg.head < w.length then some cfg.head else none)
    cfg.state 0 w.length).map cellTupleSym

Uses 6 · Used by 6

Statement usesBoundary tag of a linear bounded automaton head · Configuration of a linear bounded automaton · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell tuple as a grammar symbol · Cell tuples of an LBA configuration from an offset

Used byRuns of an LBA give grammar derivations · An LBA step is a grammar derivation step on encodings · Generated form derives the initial configuration encoding · Entries of a configuration encoding · If the LBA accepts a nonempty word, the grammar derives it · Length of a configuration encoding

DefinitionMiddle generated cells of a word#✓fully proved

The middle non-head generated cells of a word, inactive: the cells the generator produces while the generator remains.

def tailCellsMid : List Γ → List (Γ × Option Γ × Option Q × Bool × LBABoundary)
  | [] => []
  | a :: w => (a, some a, none, false, .middle) :: tailCellsMid w

Uses 1 · Used by 2

Statement usesBoundary tag of a linear bounded automaton head

Used byThe generator derives the middle cells and itself · Middle generated sentential form of a word

DefinitionTail generated cells of a word#✓fully proved

The non-head generated cells of a word, inactive, as the tail of a generated word: middle cells and a final right cell.

def tailCells : List Γ → List (Γ × Option Γ × Option Q × Bool × LBABoundary)
  | [] => []
  | [a] => [(a, some a, none, false, .right)]
  | a :: b :: w => (a, some a, none, false, .middle) :: tailCells (b :: w)

Uses 1 · Used by 6

Statement usesBoundary tag of a linear bounded automaton head

Used byGenerated form derives the initial configuration encoding · The generator derives the full tail of cells · The start symbol derives the generated form of a word · Tail cells derive their activated encoding · Generated cells of a word · Tail generated sentential form of a word

DefinitionGenerated cells of a word#✓fully proved

The generated cells of a word, inactive, with the head state on the first cell: the sentential form generation produces. The first cell is tagged both for a one-cell word and left otherwise; the tail is tailCells.

def genCells (M : LinearBoundedAutomaton Q Γ) :
    List Γ → List (Γ × Option Γ × Option Q × Bool × LBABoundary)
  | [] => []
  | [a] => [(a, some a, some M.q₀, false, .both)]
  | a :: b :: w => (a, some a, some M.q₀, false, .left) :: tailCells (b :: w)

Uses 3 · Used by 1

Statement usesBoundary tag of a linear bounded automaton head · Linear bounded automaton · Tail generated cells of a word

Used byGenerated sentential form of a word

DefinitionGenerated sentential form of a word#✓fully proved

The generated sentential form of a word.

def genEncode (M : LinearBoundedAutomaton Q Γ) (w : List Γ) :
    List (Symbol Γ (LBANT Γ Q)) :=
  (genCells (M := M) w).map cellTupleSym

Uses 5 · Used by 3

Statement usesBoundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell tuple as a grammar symbol · Generated cells of a word

Used byGenerated form derives the initial configuration encoding · The start symbol derives the generated form of a word · If the LBA accepts a nonempty word, the grammar derives it

DefinitionTail generated sentential form of a word#✓fully proved

The non-head generated sentential form of a word.

def tailEncode (_M : LinearBoundedAutomaton Q Γ) (w : List Γ) :
    List (Symbol Γ (LBANT Γ Q)) :=
  (tailCells w).map cellTupleSym

Uses 5 · Used by 4

Statement usesBoundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell tuple as a grammar symbol · Tail generated cells of a word

Used byGenerated form derives the initial configuration encoding · The generator derives the full tail of cells · The start symbol derives the generated form of a word · Tail cells derive their activated encoding

DefinitionMiddle generated sentential form of a word#✓fully proved

The middle non-head generated sentential form of a word: every cell tagged middle, for the generator's intermediate stage.

def tailEncodeMid (_M : LinearBoundedAutomaton Q Γ) (w : List Γ) :
    List (Symbol Γ (LBANT Γ Q)) :=
  (tailCellsMid w).map cellTupleSym

Uses 5 · Used by 1

Statement usesBoundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell tuple as a grammar symbol · Middle generated cells of a word

Used byThe generator derives the middle cells and itself

TheoremLength of the cell-tuple encoding#✓fully proved

The encoding has as many cells as the input word, when the tape has the same length.

theorem length_encodeCellsAux {w : List Γ} {tape : List (Option Γ)} {h : Option ℕ} {q : Q}
    {start total : ℕ} (hl : w.length = tape.length) :
    (encodeCellsAux w tape h q start total).length = w.length

Uses 2 · Used by 3

Statement usesBoundary tag of a linear bounded automaton head · Cell tuples of an LBA configuration from an offset

Used byEntries of the cell-tuple encoding · Entries of a configuration encoding · Length of a configuration encoding

TheoremEntries of the cell-tuple encoding#✓fully proved

The i-th cell of the encoding: original w[i], current tape[i], head state exactly at the head position, boundary tag of position start + i in a word of length total.

theorem getElem_encodeCellsAux {w : List Γ} {tape : List (Option Γ)} {h : Option ℕ} {q : Q}
    {start total i : ℕ} (hl : w.length = tape.length) (hi : i < w.length) :
    (encodeCellsAux w tape h q start total)[i]'
        (by rw [length_encodeCellsAux hl]; exact hi) =
      (w[i]'hi, (tape[i]?).join, if h = some i then some q else none, true,
        LBABoundary.ofHead (start + i) total)

Uses 4 · Used by 1

Statement usesBoundary tag of a linear bounded automaton head · Boundary tag of a head position · Cell tuples of an LBA configuration from an offset · Length of the cell-tuple encoding

Used byEntries of a configuration encoding

TheoremReplacing a block by a rule is a derivation step#✓fully proved

One grammar step replacing a block: if u splits as p ++ lhs ++ q and (lhs, rhs) is a rule, then u derives p ++ rhs ++ q.

theorem derives_replace_list {u p q lhs rhs : List (Symbol Γ (LBANT Γ Q))}
    (hu : u = p ++ lhs ++ q) (hrule : (lhs, rhs) ∈ M.lbaGrammar.rules) :
    Derives M.lbaGrammar u (p ++ rhs ++ q)

Uses 8 · Used by 8

Statement usesUnrestricted grammar · Derivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · The grammar of an LBA

Proof usesDerivations in a string rewriting system · Rewriting rules · One-step rewriting

Used byThe generator derives the middle cells and itself · The generator derives the full tail of cells · Setting one list position by a production is a derivation step · Setting two adjacent list positions by a production is a derivation step · Replacing a single cell is a derivation step · Singleton-to-singleton productions are derivation steps · The start symbol derives the generated form of a word · Replacing two consecutive cells is a derivation step

TheoremReplacing a single cell is a derivation step#✓fully proved

One grammar step replacing a single cell by a single cell.

theorem derives_single_cell {u p q : List (Symbol Γ (LBANT Γ Q))}
    {x y : Symbol Γ (LBANT Γ Q)} (hu : u = p ++ [x] ++ q)
    (hrule : ([x], [y]) ∈ M.lbaGrammar.rules) :
    Derives M.lbaGrammar u (p ++ [y] ++ q)

Uses 6

Statement usesUnrestricted grammar · Derivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · The grammar of an LBA

Proof usesReplacing a block by a rule is a derivation step

TheoremReplacing two consecutive cells is a derivation step#✓fully proved

One grammar step replacing two consecutive cells.

theorem derives_two_cells {u p q : List (Symbol Γ (LBANT Γ Q))}
    {x₁ x₂ y₁ y₂ : Symbol Γ (LBANT Γ Q)} (hu : u = p ++ [x₁, x₂] ++ q)
    (hrule : ([x₁, x₂], [y₁, y₂]) ∈ M.lbaGrammar.rules) :
    Derives M.lbaGrammar u (p ++ [y₁, y₂] ++ q)

Uses 6

Statement usesUnrestricted grammar · Derivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · The grammar of an LBA

Proof usesReplacing a block by a rule is a derivation step

TheoremSingleton-to-singleton productions are derivation steps#✓fully proved

A singleton-to-singleton production is a derivation step.

theorem derives_singleton_cell {x y : Symbol Γ (LBANT Γ Q)}
    (hrule : ([x], [y]) ∈ M.lbaGrammar.rules) :
    Derives M.lbaGrammar [x] [y]

Uses 6 · Used by 5

Statement usesUnrestricted grammar · Derivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · The grammar of an LBA

Proof usesReplacing a block by a rule is a derivation step

Used byNon-head or accepting cells convert to terminals · Generated form derives the initial configuration encoding · The generator derives the full tail of cells · The start symbol derives the generated form of a word · Tail cells derive their activated encoding

TheoremDerivations extend by a left context#✓fully proved

A derivation may be appended on the left.

theorem derives_append_left {u v : List (Symbol Γ (LBANT Γ Q))}
    (p : List (Symbol Γ (LBANT Γ Q))) (h : Derives M.lbaGrammar u v) :
    Derives M.lbaGrammar (p ++ u) (p ++ v)

Uses 8 · Used by 3

Statement usesDerivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · The grammar of an LBA

Proof usesDerivations in a string rewriting system · Rewriting rules · One-step rewriting · Unrestricted grammar

Used byThe generator derives the middle cells and itself · The generator derives the full tail of cells · The start symbol derives the generated form of a word

TheoremDerivations extend by a right context#✓fully proved

A derivation may be appended on the right.

theorem derives_append_right {u v : List (Symbol Γ (LBANT Γ Q))}
    (p : List (Symbol Γ (LBANT Γ Q))) (h : Derives M.lbaGrammar u v) :
    Derives M.lbaGrammar (u ++ p) (v ++ p)

Uses 8

Statement usesDerivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · The grammar of an LBA

Proof usesDerivations in a string rewriting system · Rewriting rules · One-step rewriting · Unrestricted grammar

TheoremDerivations compose under concatenation#✓fully proved

Derivations compose under append.

theorem derives_append {a b c d : List (Symbol Γ (LBANT Γ Q))}
    (h₁ : Derives M.lbaGrammar a b) (h₂ : Derives M.lbaGrammar c d) :
    Derives M.lbaGrammar (a ++ c) (b ++ d)

Uses 8 · Used by 3

Statement usesDerivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · The grammar of an LBA

Proof usesDerivations in a string rewriting system · Rewriting rules · One-step rewriting · Unrestricted grammar

Used byNon-head or accepting cells convert to terminals · Generated form derives the initial configuration encoding · Tail cells derive their activated encoding

TheoremTransitivity of grammar derivations#✓fully proved

Derivations are transitive.

theorem derives_trans {a b c : List (Symbol Γ (LBANT Γ Q))}
    (h₁ : Derives M.lbaGrammar a b) (h₂ : Derives M.lbaGrammar b c) :
    Derives M.lbaGrammar a c

Uses 8 · Used by 5

Statement usesDerivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · The grammar of an LBA

Proof usesDerivations in a string rewriting system · Rewriting rules · One-step rewriting · Unrestricted grammar

Used byRuns of an LBA give grammar derivations · The generator derives the middle cells and itself · The generator derives the full tail of cells · The start symbol derives the generated form of a word · If the LBA accepts a nonempty word, the grammar derives it

TheoremThe first generation rule belongs to the LBA grammar#✓fully proved

The first generation rule is a rule of the grammar.

theorem mem_rule_gen_start (a : Γ) :
    ([startSym (Γ := Γ) (Q := Q)],
      [cellSym a (some a) (some M.q₀) false .left, genSym (Γ := Γ) (Q := Q)]) ∈
      M.lbaGrammar.rules

Uses 15 · Used by 1

Statement usesUnrestricted grammar · Boundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar · Generator symbol of the LBA grammar · The grammar of an LBA · Start symbol of the LBA grammar

Proof usesActivation rules of the LBA grammar · All rules of the LBA grammar · Conversion rules of the LBA grammar · Generation rules of the LBA grammar · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move

Used byThe start symbol derives the generated form of a word

TheoremThe one-cell generation rule belongs to the LBA grammar#✓fully proved

The one-cell generation rule is a rule of the grammar.

theorem mem_rule_gen_single (a : Γ) :
    ([startSym (Γ := Γ) (Q := Q)],
      [cellSym a (some a) (some M.q₀) false .both]) ∈
      M.lbaGrammar.rules

Uses 15 · Used by 1

Statement usesUnrestricted grammar · Boundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar · The grammar of an LBA · Start symbol of the LBA grammar

Proof usesActivation rules of the LBA grammar · All rules of the LBA grammar · Conversion rules of the LBA grammar · Generation rules of the LBA grammar · Generator symbol of the LBA grammar · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move

Used byThe start symbol derives the generated form of a word

TheoremThe generator step rule belongs to the LBA grammar#✓fully proved

The generator step rule is a rule of the grammar.

theorem mem_rule_gen_step (a : Γ) :
    ([genSym (Γ := Γ) (Q := Q)],
      [cellSym a (some a) none false .middle, genSym (Γ := Γ) (Q := Q)]) ∈
      M.lbaGrammar.rules

Uses 15 · Used by 2

Statement usesUnrestricted grammar · Boundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar · Generator symbol of the LBA grammar · The grammar of an LBA

Proof usesActivation rules of the LBA grammar · All rules of the LBA grammar · Conversion rules of the LBA grammar · Generation rules of the LBA grammar · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move · Start symbol of the LBA grammar

Used byThe generator derives the middle cells and itself · The generator derives the full tail of cells

TheoremThe final generation rule belongs to the LBA grammar#✓fully proved

The final generation rule is a rule of the grammar.

theorem mem_rule_gen_last (a : Γ) :
    ([genSym (Γ := Γ) (Q := Q)], [cellSym a (some a) none false .right]) ∈
      M.lbaGrammar.rules

Uses 15 · Used by 1

Statement usesUnrestricted grammar · Boundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar · Generator symbol of the LBA grammar · The grammar of an LBA

Proof usesActivation rules of the LBA grammar · All rules of the LBA grammar · Conversion rules of the LBA grammar · Generation rules of the LBA grammar · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move · Start symbol of the LBA grammar

Used byThe generator derives the full tail of cells

TheoremThe activation rule belongs to the LBA grammar#✓fully proved

The activation rule is a rule of the grammar.

theorem mem_rule_activate (a : Γ) (cur : Option Γ) (st : Option Q)
    (bnd : LBABoundary) :
    ([cellSym a cur st false bnd], [cellSym a cur st true bnd]) ∈
      M.lbaGrammar.rules

Uses 13 · Used by 2

Statement usesUnrestricted grammar · Boundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar · The grammar of an LBA

Proof usesActivation rules of the LBA grammar · All rules of the LBA grammar · Conversion rules of the LBA grammar · Generation rules of the LBA grammar · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move

Used byGenerated form derives the initial configuration encoding · Tail cells derive their activated encoding

TheoremStay transitions give simulation rules#✓fully proved

A stay transition gives a simulation rule.

theorem mem_rule_sim_stay {q q' : Q} {read write : Option Γ} {orig : Γ}
    {bnd : LBABoundary}
    (h : (q', write, LBAMove.stay) ∈ M.delta q read bnd) :
    ([cellSym orig read (some q) true bnd],
      [cellSym orig write (some q') true bnd]) ∈
      M.lbaGrammar.rules

Uses 13 · Used by 1

Statement usesUnrestricted grammar · Boundary tag of a linear bounded automaton head · Head move of a linear bounded automaton · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar · The grammar of an LBA

Proof usesActivation rules of the LBA grammar · Conversion rules of the LBA grammar · Generation rules of the LBA grammar · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move

Used byAn LBA step is a grammar derivation step on encodings

TheoremRight transitions give simulation rules#✓fully proved

A right transition gives a simulation rule.

theorem mem_rule_sim_right {q q' : Q} {read write : Option Γ} {orig orig₂ : Γ}
    {cur₂ : Option Γ} {bnd bnd₂ : LBABoundary}
    (h : (q', write, LBAMove.right) ∈ M.delta q read bnd) :
    ([cellSym orig read (some q) true bnd, cellSym orig₂ cur₂ none true bnd₂],
      [cellSym orig write none true bnd, cellSym orig₂ cur₂ (some q') true bnd₂]) ∈
      M.lbaGrammar.rules

Uses 13 · Used by 1

Statement usesUnrestricted grammar · Boundary tag of a linear bounded automaton head · Head move of a linear bounded automaton · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar · The grammar of an LBA

Proof usesActivation rules of the LBA grammar · Conversion rules of the LBA grammar · Generation rules of the LBA grammar · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move

Used byAn LBA step is a grammar derivation step on encodings

TheoremLeft transitions give simulation rules#✓fully proved

A left transition gives a simulation rule.

theorem mem_rule_sim_left {q q' : Q} {read write : Option Γ} {orig orig₂ : Γ}
    {cur₂ : Option Γ} {bnd bnd₂ : LBABoundary}
    (h : (q', write, LBAMove.left) ∈ M.delta q read bnd) :
    ([cellSym orig₂ cur₂ none true bnd₂, cellSym orig read (some q) true bnd],
      [cellSym orig₂ cur₂ (some q') true bnd₂, cellSym orig write none true bnd]) ∈
      M.lbaGrammar.rules

Uses 13 · Used by 1

Statement usesUnrestricted grammar · Boundary tag of a linear bounded automaton head · Head move of a linear bounded automaton · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar · The grammar of an LBA

Proof usesActivation rules of the LBA grammar · Conversion rules of the LBA grammar · Generation rules of the LBA grammar · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move

Used byAn LBA step is a grammar derivation step on encodings

TheoremThe accepting conversion rule belongs to the LBA grammar#✓fully proved

The accepting conversion rule is a rule of the grammar.

theorem mem_rule_conv_acc (a : Γ) (cur : Option Γ) (bnd : LBABoundary) :
    ([cellSym a cur (some M.qAcc) true bnd], [termSym a]) ∈ M.lbaGrammar.rules

Uses 13 · Used by 1

Statement usesUnrestricted grammar · Boundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar · The grammar of an LBA · Terminal symbol of the LBA grammar

Proof usesActivation rules of the LBA grammar · All rules of the LBA grammar · Generation rules of the LBA grammar · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move

Used byNon-head or accepting cells convert to terminals

TheoremThe non-head conversion rule belongs to the LBA grammar#✓fully proved

The non-head conversion rule is a rule of the grammar.

theorem mem_rule_conv_none (a : Γ) (cur : Option Γ) (bnd : LBABoundary) :
    ([cellSym a cur none true bnd], [termSym a]) ∈ M.lbaGrammar.rules

Uses 13 · Used by 1

Statement usesUnrestricted grammar · Boundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar · The grammar of an LBA · Terminal symbol of the LBA grammar

Proof usesActivation rules of the LBA grammar · All rules of the LBA grammar · Generation rules of the LBA grammar · Simulation rules for a left move · Simulation rules for a right move · Simulation rules for a stay move

Used byNon-head or accepting cells convert to terminals

TheoremThe generator derives the middle cells and itself#✓fully proved

The generator derives the middle tail cells followed by itself.

theorem derives_gen_tail : ∀ w : List Γ,
    Derives M.lbaGrammar [genSym (Γ := Γ) (Q := Q)]
      (tailEncodeMid M w ++ [genSym])

Uses 18

Statement usesDerivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Generator symbol of the LBA grammar · The grammar of an LBA · Middle generated sentential form of a word

Proof usesDerivations in a string rewriting system · Rewriting rules · One-step rewriting · Unrestricted grammar · Boundary tag of a linear bounded automaton head · Cell symbol of the LBA grammar · Cell tuple as a grammar symbol · Derivations extend by a left context · Replacing a block by a rule is a derivation step · Transitivity of grammar derivations · The generator step rule belongs to the LBA grammar · Middle generated cells of a word

TheoremThe generator derives the full tail of cells#✓fully proved

The generator derives the tail cells, ending the generation.

theorem derives_gen_tail_last : ∀ w : List Γ, w ≠ [] →
    Derives M.lbaGrammar [genSym (Γ := Γ) (Q := Q)] (tailEncode M w)

Uses 16 · Used by 1

Statement usesDerivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Generator symbol of the LBA grammar · The grammar of an LBA · Tail generated sentential form of a word

Proof usesBoundary tag of a linear bounded automaton head · Cell symbol of the LBA grammar · Cell tuple as a grammar symbol · Derivations extend by a left context · Replacing a block by a rule is a derivation step · Singleton-to-singleton productions are derivation steps · Transitivity of grammar derivations · The final generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar · Tail generated cells of a word

Used byThe start symbol derives the generated form of a word

TheoremThe start symbol derives the generated form of a word#✓fully proved

The start symbol derives the generated sentential form of a word.

theorem derives_start_genEncode : ∀ w : List Γ, w ≠ [] →
    Derives M.lbaGrammar [startSym (Γ := Γ) (Q := Q)] (genEncode M w)

Uses 19 · Used by 1

Statement usesDerivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Generated sentential form of a word · The grammar of an LBA · Start symbol of the LBA grammar

Proof usesBoundary tag of a linear bounded automaton head · Cell symbol of the LBA grammar · Cell tuple as a grammar symbol · Derivations extend by a left context · The generator derives the full tail of cells · Replacing a block by a rule is a derivation step · Singleton-to-singleton productions are derivation steps · Transitivity of grammar derivations · Generator symbol of the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · Tail generated cells of a word · Tail generated sentential form of a word

Used byIf the LBA accepts a nonempty word, the grammar derives it

TheoremTail cells derive their activated encoding#✓fully proved

The tail cells, sitting at offset start ≥ 1 in a word of total length start + w.length, derive their activated encoding. The offset stays ≥ 1 in the induction step, so the first tail cell is never tagged left: it is right when it is the last cell and middle otherwise.

theorem derives_tail_activate : ∀ (w : List Γ) (start : ℕ), 1 ≤ start →
    Derives M.lbaGrammar (tailEncode M w)
      ((encodeCellsAux w (w.map some) none M.q₀ start (w.length + start)).map
        cellTupleSym)

Uses 20 · Used by 1

Statement usesDerivation in an unrestricted grammar · Boundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell tuple as a grammar symbol · Cell tuples of an LBA configuration from an offset · The grammar of an LBA · Tail generated sentential form of a word

Proof usesDerivations in a string rewriting system · Rewriting rules · One-step rewriting · Unrestricted grammar · Boundary tag of a head position · Boundary tag at an interior head position · Boundary tag on the last cell of a longer tape · Cell symbol of the LBA grammar · Derivations compose under concatenation · Singleton-to-singleton productions are derivation steps · The activation rule belongs to the LBA grammar · Tail generated cells of a word

Used byGenerated form derives the initial configuration encoding

TheoremGenerated form derives the initial configuration encoding#✓fully proved

The generated form derives the encoding of the initial configuration.

theorem derives_gen_activate : ∀ w : List Γ,
    Derives M.lbaGrammar (genEncode M w) (encodeCfg M w (M.initCfg w))

Uses 24 · Used by 1

Statement usesDerivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Configuration encoded as a sentential form · Generated sentential form of a word · Initial configuration of a linear bounded automaton · The grammar of an LBA

Proof usesDerivations in a string rewriting system · Rewriting rules · One-step rewriting · Unrestricted grammar · Boundary tag of a linear bounded automaton head · Boundary tag of a head position · Boundary tag on a one-cell tape · Configuration of a linear bounded automaton · Cell symbol of the LBA grammar · Cell tuple as a grammar symbol · Derivations compose under concatenation · Singleton-to-singleton productions are derivation steps · Tail cells derive their activated encoding · Cell tuples of an LBA configuration from an offset · The activation rule belongs to the LBA grammar · Tail generated cells of a word · Tail generated sentential form of a word

Used byIf the LBA accepts a nonempty word, the grammar derives it

TheoremSplitting a list at two consecutive positions#✓fully proved

A list splits at two consecutive positions.

theorem take_append_two {α : Type*} {l : List α} {i : ℕ} (hi : i + 1 < l.length) :
    l = List.take i l ++ [l[i]'(by omega), l[i + 1]'hi] ++ List.drop (i + 2) l

Used by 1

Used bySetting two adjacent list positions by a production is a derivation step

TheoremSetting one list position by a production is a derivation step#✓fully proved

A single-cell replacement that is a production is a derivation step.

theorem derives_set_single {u : List (Symbol Γ (LBANT Γ Q))} {i : ℕ}
    {y : Symbol Γ (LBANT Γ Q)} (hi : i < u.length)
    (hrule : ([u[i]'hi], [y]) ∈ M.lbaGrammar.rules) :
    Derives M.lbaGrammar u (u.set i y)

Uses 6 · Used by 1

Statement usesUnrestricted grammar · Derivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · The grammar of an LBA

Proof usesReplacing a block by a rule is a derivation step

Used byAn LBA step is a grammar derivation step on encodings

TheoremDropping past an updated list position#✓fully proved

Dropping past a set position is unaffected by the set.

theorem drop_set_of_gt {α : Type*} {l : List α} {i : ℕ} {y : α} (hi : i < l.length) :
    List.drop (i + 2) (l.set i y) = List.drop (i + 2) l

Used by 1

Used bySetting two adjacent list positions by a production is a derivation step

TheoremTaking past an updated list position#✓fully proved

Taking past a set position keeps the new value at that position.

theorem take_set {α : Type*} {l : List α} {i : ℕ} {y : α} (hi : i < l.length) :
    List.take (i + 1) (l.set i y) = List.take i l ++ [y]

Used by 1

Used bySetting two adjacent list positions by a production is a derivation step

TheoremSetting two adjacent list positions by a production is a derivation step#✓fully proved

A two-cell replacement that is a production is a derivation step.

theorem derives_set_two {u : List (Symbol Γ (LBANT Γ Q))} {i : ℕ}
    {y₁ y₂ : Symbol Γ (LBANT Γ Q)} (hi : i + 1 < u.length)
    (hrule : ([u[i]'(by omega), u[i + 1]'hi], [y₁, y₂]) ∈ M.lbaGrammar.rules) :
    Derives M.lbaGrammar u ((u.set i y₁).set (i + 1) y₂)

Uses 9 · Used by 2

Statement usesUnrestricted grammar · Derivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · The grammar of an LBA

Proof usesReplacing a block by a rule is a derivation step · Dropping past an updated list position · Splitting a list at two consecutive positions · Taking past an updated list position

Used byAn LBA step is a grammar derivation step on encodings · Two-cell replacement at indices \(i\) and \(j = i + 1\)

TheoremTwo-cell replacement at indices \(i\) and \(j = i + 1\)#✓fully proved

A two-cell replacement at positions i and j = i + 1.

theorem derives_set_two' {u : List (Symbol Γ (LBANT Γ Q))} {i j : ℕ}
    {y₁ y₂ : Symbol Γ (LBANT Γ Q)} (hi : i + 1 < u.length) (hj : j = i + 1)
    (hrule : ([u[i]'(by omega), u[j]'(by omega)], [y₁, y₂]) ∈ M.lbaGrammar.rules) :
    Derives M.lbaGrammar u ((u.set i y₁).set j y₂)

Uses 6 · Used by 1

Statement usesUnrestricted grammar · Derivation in an unrestricted grammar · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · The grammar of an LBA

Proof usesSetting two adjacent list positions by a production is a derivation step

Used byAn LBA step is a grammar derivation step on encodings

TheoremLength of a configuration encoding#✓fully proved

The encoding of a configuration has as many cells as the input word.

theorem length_encodeCfg {w : List Γ} {cfg : LBAConfig Q Γ}
    (hl : cfg.tape.length = w.length) : (encodeCfg M w cfg).length = w.length

Uses 8 · Used by 2

Statement usesConfiguration of a linear bounded automaton · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Configuration encoded as a sentential form

Proof usesBoundary tag of a linear bounded automaton head · Cell tuple as a grammar symbol · Cell tuples of an LBA configuration from an offset · Length of the cell-tuple encoding

Used byAn LBA step is a grammar derivation step on encodings · Entries of a configuration encoding

TheoremEntries of a configuration encoding#✓fully proved

The i-th cell of the encoding.

theorem getElem_encodeCfg {w : List Γ} {cfg : LBAConfig Q Γ} {i : ℕ}
    (hl : cfg.tape.length = w.length) (hhead : cfg.head < w.length)
    (hi : i < w.length) :
    (encodeCfg M w cfg)[i]'(by rw [length_encodeCfg hl]; exact hi) =
      cellSym (w[i]'hi) ((cfg.tape[i]?).join)
        (if i = cfg.head then some cfg.state else none) true
        (LBABoundary.ofHead i w.length)

Uses 12 · Used by 1

Statement usesBoundary tag of a head position · Configuration of a linear bounded automaton · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell symbol of the LBA grammar · Configuration encoded as a sentential form · Length of a configuration encoding

Proof usesBoundary tag of a linear bounded automaton head · Cell tuple as a grammar symbol · Cell tuples of an LBA configuration from an offset · Entries of the cell-tuple encoding · Length of the cell-tuple encoding

Used byAn LBA step is a grammar derivation step on encodings

TheoremLBA steps preserve tape length#✓fully proved

One step preserves the tape length.

theorem step_tape_length {c c' : LBAConfig Q Γ} (h : M.Step c c') :
    c'.tape.length = c.tape.length

Uses 8 · Used by 2

Statement usesConfiguration of a linear bounded automaton · Linear bounded automaton · One step of a linear bounded automaton

Proof usesBoundary tag of a linear bounded automaton head · Boundary tag of a head position · Head move of a linear bounded automaton · Legal head move of a linear bounded automaton · Head position after a move

Used byRuns of an LBA give grammar derivations · Reachable LBA configurations keep the tape length and the head on the tape

TheoremLBA steps keep the head on the tape#✓fully proved

One step keeps the head on the tape, when the source head is on the tape.

theorem step_head_lt {c c' : LBAConfig Q Γ} (h : M.Step c c')
    (hhead : c.head < c.tape.length) : c'.head < c'.tape.length

Uses 8 · Used by 2

Statement usesConfiguration of a linear bounded automaton · Linear bounded automaton · One step of a linear bounded automaton

Proof usesBoundary tag of a linear bounded automaton head · Boundary tag of a head position · Head move of a linear bounded automaton · Legal head move of a linear bounded automaton · Head position after a move

Used byRuns of an LBA give grammar derivations · Reachable LBA configurations keep the tape length and the head on the tape

TheoremReachable LBA configurations keep the tape length and the head on the tape#✓fully proved

Reachable configurations have the input tape length and the head on the tape, for a nonempty input word.

theorem reachable_tape_length {w : List Γ} {c : LBAConfig Q Γ} (hw : w ≠ [])
    (h : Relation.ReflTransGen M.Step (M.initCfg w) c) :
    c.tape.length = w.length ∧ c.head < c.tape.length

Uses 6

Statement usesConfiguration of a linear bounded automaton · Linear bounded automaton · One step of a linear bounded automaton · Initial configuration of a linear bounded automaton

Proof usesLBA steps keep the head on the tape · LBA steps preserve tape length

TheoremAn LBA step is a grammar derivation step on encodings#✓fully proved

One machine step is one grammar derivation step on encodings.

theorem derives_encodeCfg_step {w : List Γ} {c c' : LBAConfig Q Γ}
    (_hw : w ≠ []) (hstep : M.Step c c')
    (hl : c.tape.length = w.length) (hhead : c.head < c.tape.length) :
    Derives M.lbaGrammar (encodeCfg M w c) (encodeCfg M w c')

Uses 22 · Used by 1

Statement usesDerivation in an unrestricted grammar · Configuration of a linear bounded automaton · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · One step of a linear bounded automaton · Configuration encoded as a sentential form · The grammar of an LBA

Proof usesUnrestricted grammar · Boundary tag of a linear bounded automaton head · Boundary tag of a head position · Head move of a linear bounded automaton · Legal head move of a linear bounded automaton · Head position after a move · Cell symbol of the LBA grammar · Setting one list position by a production is a derivation step · Setting two adjacent list positions by a production is a derivation step · Two-cell replacement at indices \(i\) and \(j = i + 1\) · Entries of a configuration encoding · Length of a configuration encoding · Left transitions give simulation rules · Right transitions give simulation rules · Stay transitions give simulation rules

Used byRuns of an LBA give grammar derivations

TheoremHead states in a configuration encoding#✓fully proved

Every cell of an encoding has head state none or the given state.

theorem encodeCellsAux_state {w : List Γ} {tape : List (Option Γ)} {h : Option ℕ} {q : Q}
    {start total : ℕ}
    {cell : Γ × Option Γ × Option Q × Bool × LBABoundary}
    (hmem : cell ∈ encodeCellsAux w tape h q start total) :
    cell.2.2.1 = none ∨ cell.2.2.1 = some q

Uses 3 · Used by 1

Statement usesBoundary tag of a linear bounded automaton head · Cell tuples of an LBA configuration from an offset

Proof usesBoundary tag of a head position

Used byIf the LBA accepts a nonempty word, the grammar derives it

TheoremEvery cell of a configuration encoding is active#✓fully proved

Every cell of an encoding is active.

theorem encodeCellsAux_active {w : List Γ} {tape : List (Option Γ)} {h : Option ℕ} {q : Q}
    {start total : ℕ}
    {cell : Γ × Option Γ × Option Q × Bool × LBABoundary}
    (hmem : cell ∈ encodeCellsAux w tape h q start total) :
    cell.2.2.2.1 = true

Uses 3 · Used by 1

Statement usesBoundary tag of a linear bounded automaton head · Cell tuples of an LBA configuration from an offset

Proof usesBoundary tag of a head position

Used byIf the LBA accepts a nonempty word, the grammar derives it

TheoremOriginal symbols of an encoding are the input word#✓fully proved

The original symbols of an encoding are the input word.

theorem map_orig_encodeCellsAux {w : List Γ} {tape : List (Option Γ)} {h : Option ℕ} {q : Q}
    {start total : ℕ} (hl : w.length = tape.length) :
    (encodeCellsAux w tape h q start total).map (fun cell ↦ termSym (Q := Q) cell.1) =
      w.map (termSym (Q := Q))

Uses 5 · Used by 1

Statement usesBoundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Cell tuples of an LBA configuration from an offset · Terminal symbol of the LBA grammar

Proof usesBoundary tag of a head position

Used byIf the LBA accepts a nonempty word, the grammar derives it

TheoremNon-head or accepting cells convert to terminals#✓fully proved

A list of cells, each non-head or accepting, converts to its original terminals.

theorem derives_convert_cells :
    ∀ (cells : List (Γ × Option Γ × Option Q × Bool × LBABoundary)),
    (∀ cell ∈ cells, (cell.2.2.1 = none ∨ cell.2.2.1 = some M.qAcc) ∧
      cell.2.2.2.1 = true) →
    Derives M.lbaGrammar (cells.map cellTupleSym)
      (cells.map fun cell ↦ termSym (Q := Q) cell.1)

Uses 16 · Used by 1

Statement usesDerivation in an unrestricted grammar · Boundary tag of a linear bounded automaton head · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Cell tuple as a grammar symbol · The grammar of an LBA · Terminal symbol of the LBA grammar

Proof usesDerivations in a string rewriting system · Rewriting rules · One-step rewriting · Unrestricted grammar · Cell symbol of the LBA grammar · Derivations compose under concatenation · Singleton-to-singleton productions are derivation steps · The accepting conversion rule belongs to the LBA grammar · The non-head conversion rule belongs to the LBA grammar

Used byIf the LBA accepts a nonempty word, the grammar derives it

TheoremRuns of an LBA give grammar derivations#✓fully proved

Derivations along a run, keeping the tape length and head on the tape.

theorem derives_encodeCfg_reflTransGen {w : List Γ} {c : LBAConfig Q Γ} (hw : w ≠ [])
    (h : Relation.ReflTransGen M.Step (M.initCfg w) c) :
    c.tape.length = w.length ∧ c.head < c.tape.length ∧
      Derives M.lbaGrammar (encodeCfg M w (M.initCfg w)) (encodeCfg M w c)

Uses 16 · Used by 1

Statement usesDerivation in an unrestricted grammar · Configuration of a linear bounded automaton · Nonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · One step of a linear bounded automaton · Configuration encoded as a sentential form · Initial configuration of a linear bounded automaton · The grammar of an LBA

Proof usesDerivations in a string rewriting system · Rewriting rules · One-step rewriting · Unrestricted grammar · An LBA step is a grammar derivation step on encodings · Transitivity of grammar derivations · LBA steps keep the head on the tape · LBA steps preserve tape length

Used byIf the LBA accepts a nonempty word, the grammar derives it

TheoremIf the LBA accepts a nonempty word, the grammar derives it#✓fully proved

This is one inclusion of the LBA-to-grammar direction.

theorem lba_accepts_implies_grammar_derives {w : List Γ} (hw : w ≠ [])
    (h : M.Accepts w) : w ∈ Cslib.Language.language M.lbaGrammar

Uses 24

Statement usesNonterminals of the grammar of a linear bounded automaton · Linear bounded automaton · Acceptance by a linear bounded automaton · The grammar of an LBA · Language of an unrestricted grammar

Proof usesDerivation in an unrestricted grammar · Boundary tag of a linear bounded automaton head · Configuration of a linear bounded automaton · One step of a linear bounded automaton · Cell tuple as a grammar symbol · Non-head or accepting cells convert to terminals · Runs of an LBA give grammar derivations · Generated form derives the initial configuration encoding · The start symbol derives the generated form of a word · Transitivity of grammar derivations · Cell tuples of an LBA configuration from an offset · Every cell of a configuration encoding is active · Head states in a configuration encoding · Configuration encoded as a sentential form · Generated sentential form of a word · Initial configuration of a linear bounded automaton · Original symbols of an encoding are the input word · Start symbol of the LBA grammar · Terminal symbol of the LBA grammar

DefinitionSpace-bounded single-tape machines#✓fully proved

Let \(s : \mathbb{N} \to \mathbb{N}\). A single-tape Turing machine \(M\) runs in space \(s\) when, for every input word \(l\) of length \(|l|\), every configuration reachable from the initial configuration of \(M\) on \(l\) uses at most \(s(|l|)\) cells, whether or not the run halts. The cells used by a configuration are the head cell together with the cells on each side of it up to the outermost non-blank cell.

def SpaceBoundedBy (s : ℕ → ℕ) : Prop :=
  ∀ (l : List Symbol) (c : tm.Cfg), ReflTransGen tm.TransitionRelation (tm.initCfg l) c →
    c.spaceUsed ≤ s l.length

Used by 5

Used byHalting of a machine running in computable space is computable · Space-bounded machines halt within the configuration bound · Linear bounded automaton · A space bound is at least the space of the input · Space bounds can be weakened

DefinitionLinear bounded automaton#✓fully proved

A single-tape machine is a linear bounded automaton when it runs in space \(n + 1\) on inputs of length \(n\): every configuration of its run on an input of length \(n\) uses at most \(n + 1\) cells, whether or not the run halts.

The input itself uses \(\max(1, n)\) cells, and the extra cell lets the head step onto a blank cell next to the input, the analogue of Sipser's endmarkers. With the bound \(n\) instead, no machine would qualify, since the empty input already uses one cell.

def IsLBA : Prop :=
  tm.SpaceBoundedBy (· + 1)

Uses 1 · Used by 6

Statement usesSpace-bounded single-tape machines

Used byHalting of a linear bounded automaton is decidable · Halting of a linear bounded automaton on binary codes is decidable · A machine that, on a blank cell, writes a blank and does not move is a linear bounded automaton · A single-tape machine decides the halting problem of a linear bounded automaton · Emptiness of a linear bounded automaton on computable input slices is undecidable · The fenced machine is a linear bounded automaton

TheoremSpace bounds can be weakened#✓fully proved

If a single-tape machine runs in space \(s : \mathbb{N} \to \mathbb{N}\) and \(s' : \mathbb{N} \to \mathbb{N}\) satisfies \(s(n) \le s'(n)\) for every \(n \in \mathbb{N}\), then it runs in space \(s'\).

theorem SpaceBoundedBy.mono {s s' : ℕ → ℕ} (h : tm.SpaceBoundedBy s) (hs : ∀ n, s n ≤ s' n) :
    tm.SpaceBoundedBy s'

Uses 1

Statement usesSpace-bounded single-tape machines

TheoremA space bound is at least the space of the input#✓fully proved

If a single-tape machine runs in space \(s : \mathbb{N} \to \mathbb{N}\), then \(\max(1, n) \le s(n)\) for the length \(n\) of every input word, since the initial configuration on an input of length \(n\) uses \(\max(1, n)\) cells.

theorem SpaceBoundedBy.max_one_le {s : ℕ → ℕ} (h : tm.SpaceBoundedBy s) (l : List Symbol) :
    max 1 l.length ≤ s l.length

Uses 1

Statement usesSpace-bounded single-tape machines

TheoremA machine that, on a blank cell, writes a blank and does not move is a linear bounded automaton#✓fully proved

A machine that, on a blank cell, writes a blank and does not move is a linear bounded automaton. Its head never leaves a blank cell, so it stays on the input or on the two blank cells next to it, and it writes non-blank symbols only on the input. The machine may change state on a blank cell, or halt there.

theorem isLBA_of_stays_on_blank (h : ∀ q, (tm.tr q none).1 = ⟨none, none⟩) : tm.IsLBA

Uses 3 · Used by 1

Statement usesLinear bounded automaton

Proof usesOne step of a single-tape Turing machine · Tail of a stack tape, on cell lists

Used byThe fenced machine is a linear bounded automaton

DefinitionConfiguration bound#✓fully proved

For a single-tape machine with state set \(Q\) over a finite alphabet \(\Sigma\) and \(k \in \mathbb{N}\), the configuration bound at \(k\) is the number \((|Q| + 1)(|\Sigma| + 1)(|\Sigma| + 2)^{2k}\).

A configuration that uses at most \(k\) cells is determined by a state or the halting state, the symbol or blank under the head, and the first \(k\) cells to either side of the head, each a symbol, a blank, or past the last non-blank cell; so this number bounds how many such configurations there are.

def cfgBound (k : ℕ) : ℕ :=
  (Fintype.card tm.State + 1) * (Fintype.card Symbol + 1) * (Fintype.card Symbol + 2) ^ (2 * k)

Used by 3

Used byHalting of a machine running in computable space is computable · Configurations of bounded space are finitely many · Space-bounded machines halt within the configuration bound

TheoremConfigurations of bounded space are finitely many#✓fully proved

Let \(M\) be a single-tape machine with state set \(Q\) over a finite alphabet \(\Sigma\), where a configuration uses the cell under the head and the cells on either side of it up to the last non-blank one. For every \(k \in \mathbb{N}\), at most \((|Q| + 1)(|\Sigma| + 1)(|\Sigma| + 2)^{2k}\) configurations of \(M\) use at most \(k\) cells.

theorem encard_le_cfgBound (k : ℕ) : {c : tm.Cfg | c.spaceUsed ≤ k}.encard ≤ tm.cfgBound k

Uses 1 · Used by 1

Statement usesConfiguration bound

Used bySpace-bounded machines halt within the configuration bound

TheoremSpace-bounded machines halt within the configuration bound#✓fully proved

Let \(M\) be a single-tape machine with state set \(Q\) over a finite alphabet \(\Sigma\) that runs in space \(s : \mathbb{N} \to \mathbb{N}\). If \(M\) halts on an input word \(w\) of length \(n\), then from the initial configuration on \(w\) it reaches a configuration in the halting state in at most \((|Q| + 1)(|\Sigma| + 1)(|\Sigma| + 2)^{2 s(n)}\) steps.

Its run visits only configurations of space at most \(s(n)\), and does not repeat one before halting.

theorem SpaceBoundedBy.exists_halted_relatesWithinSteps {s : ℕ → ℕ} (h : tm.SpaceBoundedBy s)
    {l : List Symbol} (hl : tm.HaltsOn l) :
    ∃ c : tm.Cfg, RelatesWithinSteps tm.TransitionRelation (tm.initCfg l) c
      (tm.cfgBound (s l.length)) ∧ c.state = none

Uses 4 · Used by 1

Statement usesHalting on an input · Space-bounded single-tape machines · Configuration bound

Proof usesConfigurations of bounded space are finitely many

Used byHalting of a machine running in computable space is computable

TheoremHalting of a machine running in computable space is computable#✓fully proved

Let \(M\) be a single-tape machine with state set \(Q\) over a finite alphabet \(\Sigma\), fix any primitive recursive coding of \(\Sigma\), and let \(s : \mathbb{N} \to \mathbb{N}\) be computable. If \(M\) runs in space \(s\), then the set of input words over \(\Sigma\) on which \(M\) halts is computable.

The decision procedure runs \(M\) for \((|Q| + 1)(|\Sigma| + 1)(|\Sigma| + 2)^{2 s(n)}\) steps on an input of length \(n\) and checks whether it has halted.

theorem SpaceBoundedBy.computablePred_haltsOn [Primcodable Symbol] {s : ℕ → ℕ}
    (hs : Computable s) (h : tm.SpaceBoundedBy s) : ComputablePred tm.HaltsOn

Uses 10 · Used by 1

Statement usesHalting on an input · Space-bounded single-tape machines

Proof usesCode of a single-tape configuration · Coded configurations of a single-tape machine · Space-bounded machines halt within the configuration bound · Configuration bound · One step of a single-tape machine on coded configurations · The coded step commutes with coding · The coded step of a single-tape machine is primitive recursive · The code of the initial configuration is primitive recursive

Used byHalting of a linear bounded automaton is decidable

TheoremHalting of a linear bounded automaton is decidable#✓fully proved

Let \(M\) be a single-tape machine over a finite alphabet \(\Sigma\), and fix any primitive recursive coding of \(\Sigma\). If \(M\) is a linear bounded automaton, then the set of input words over \(\Sigma\) on which \(M\) halts is computable.

theorem IsLBA.computablePred_haltsOn [Primcodable Symbol] (h : tm.IsLBA) :
    ComputablePred tm.HaltsOn

Sources

• Sipser, Introduction to the Theory of Computation, Theorem 5.9, of which this is a fixed-machine halting analogue: Sipser decides acceptance uniformly over machine descriptions, which needs a code type for CSLib machines.

Uses 3 · Used by 1

Statement usesHalting on an input · Linear bounded automaton

Proof usesHalting of a machine running in computable space is computable

Used byHalting of a linear bounded automaton on binary codes is decidable

TheoremHalting of a linear bounded automaton on binary codes is decidable#✓fully proved

Let \(M\) be a single-tape machine over a finite alphabet \(\Sigma\) that is a linear bounded automaton, let \(\alpha\) be a primitive recursively coded type, and let \(\iota : \{0, 1\} \to \Sigma\) be any map. For \(a \in \alpha\), let \(w_a\) be the word over \(\Sigma\) obtained by applying \(\iota\) to each bit of the binary expansion, least significant bit first and without leading zeros, of the natural-number code of \(a\); so \(w_a\) is empty when that code is \(0\). Then the set of \(a \in \alpha\) such that \(M\) halts on \(w_a\) is computable.

theorem IsLBA.computablePred_haltsOn_encodeNat {α : Type*} [Primcodable α] (h : tm.IsLBA)
    (ι : Bool → Symbol) : ComputablePred fun a : α ↦ tm.HaltsOn ((encodeNat (encode a)).map ι)

Uses 4 · Used by 1

Statement usesHalting on an input · Linear bounded automaton

Proof usesHalting of a linear bounded automaton is decidable · Binary encoding, least significant bit first

Used byA single-tape machine decides the halting problem of a linear bounded automaton

TheoremA single-tape machine decides the halting problem of a linear bounded automaton#✓fully proved

Let \(M\) be a linear bounded automaton over a finite tape alphabet \(\Sigma\), let \(\iota\) be any map from the Booleans to \(\Sigma\), and let \(\alpha\) be a primitively encodable type. For \(a \in \alpha\), let \(w_a\) be the word obtained by writing, letter by letter through \(\iota\), the binary expansion (least significant bit first) of the natural-number code of \(a\). Then the predicate on \(\alpha\) that holds at \(a\) exactly when \(M\) halts on the input \(w_a\) is decidable by a single-tape machine.

theorem IsLBA.singleTapeDecidable_haltsOn_encodeNat {α : Type*} [Primcodable α] (h : tm.IsLBA)
    (ι : Bool → Symbol) :
    Decidability.SingleTapeDecidable fun a : α ↦ tm.HaltsOn ((encodeNat (encode a)).map ι)

Uses 5

Statement usesPredicates decidable by a single-tape Turing machine · Halting on an input · Linear bounded automaton

Proof usesSingle-tape decidable predicates are exactly the computable predicates · Halting of a linear bounded automaton on binary codes is decidable

94 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.