Two-way finite automata

13 fully proved

Automata

StructureDeterministic two-way automaton#✓fully proved

A deterministic two-way automaton with state set \(Q\) over the alphabet \(\Sigma\) consists of a partial transition function, which assigns to each state \(q \in Q\) and input symbol \(a \in \Sigma\) at most one pair of a successor state and a head move (left, stay or right), together with a single start state and a set of accepting states.

structure TwoWayDFA (State Symbol : Type*) where
  /-- The deterministic transition function: `step q a` is the successor state and head
  move when reading `a` in state `q`, or `none` when the run gets stuck. -/
  step : State → Symbol → Option (State × SignType)
  /-- The single start state. -/
  start : State
  /-- The set of accepting states. -/
  accept : Set State

Used by 8

Used byRegular languages are accepted by two-way deterministic automata · Language of a deterministic two-way automaton · Finite two-way deterministic automata accept regular languages · Membership in the language of a two-way deterministic automaton · A DFA as a two-way deterministic automaton · A deterministic two-way automaton as a nondeterministic one · Deterministic two-way automata have unique transitions · Transition relation of a deterministic two-way automaton

Two Way DFA

DefinitionA deterministic two-way automaton as a nondeterministic one#✓fully proved

A deterministic two-way automaton \(A\) is viewed as the nondeterministic two-way automaton with the same states and accepting states, whose only start state is the start state of \(A\), and which can go from state \(q\) reading a symbol \(a\) to state \(q'\) with head move \(m\) exactly when the step function of \(A\) at \(q\) and \(a\) returns \(q'\) and \(m\).

def toTwoWayNA (A : TwoWayDFA State Symbol) : TwoWayNA State Symbol where
  Tr q x m q' := A.step q x = some (q', m)
  start := {A.start}
  accept := A.accept

Uses 1 · Used by 7

Statement usesDeterministic two-way automaton

Used byLanguage of a deterministic two-way automaton · Finite two-way deterministic automata accept regular languages · The two-way simulation of a DFA accepts the same language · Membership in the language of a two-way deterministic automaton · The two-way simulation of a DFA agrees with that of its NFA · Deterministic two-way automata have unique transitions · Transition relation of a deterministic two-way automaton

TheoremTransition relation of a deterministic two-way automaton#✓fully proved

Let \(A\) be a deterministic two-way automaton, viewed as a nondeterministic two-way automaton. On reading the symbol \(x\) in state \(q\), it has a transition to state \(q'\) with head move \(m\) if and only if the transition function of \(A\) sends \((q, x)\) to the pair \((q', m)\).

theorem tr_iff {A : TwoWayDFA State Symbol} {q : State} {x : Symbol} {m : SignType}
    {q' : State} : A.toTwoWayNA.Tr q x m q' ↔ A.step q x = some (q', m)

Uses 2

Statement usesDeterministic two-way automaton · A deterministic two-way automaton as a nondeterministic one

TheoremDeterministic two-way automata have unique transitions#✓fully proved

Let \(A\) be a deterministic two-way automaton, viewed as a nondeterministic two-way automaton. If, on reading the symbol \(x\) in state \(q\), it has a transition to state \(q'\) with head move \(m\) and a transition to state \(q''\) with head move \(m'\), then \(m = m'\) and \(q' = q''\).

theorem tr_functional {A : TwoWayDFA State Symbol} {q : State} {x : Symbol} {m m' : SignType}
    {q' q'' : State} (h₁ : A.toTwoWayNA.Tr q x m q') (h₂ : A.toTwoWayNA.Tr q x m' q'') :
    (m, q') = (m', q'')

Uses 2

Statement usesDeterministic two-way automaton · A deterministic two-way automaton as a nondeterministic one

DefinitionLanguage of a deterministic two-way automaton#✓fully proved

The language of a deterministic two-way automaton \(A\) is the set of words accepted by \(A\) viewed as a nondeterministic two-way automaton: a word \(w\) belongs to it when, starting in the start state with the head at the first position of \(w\) and following the step function of \(A\) (which moves the head one position left, keeps it in place, or moves it one position right, and gets stuck when it is undefined or would move the head left of the first position), the automaton reaches an accepting state with the head just past the last symbol of \(w\).

def language (A : TwoWayDFA State Symbol) : Language Symbol :=
  Acceptor.language A.toTwoWayNA

Uses 2 · Used by 4

Statement usesDeterministic two-way automaton · A deterministic two-way automaton as a nondeterministic one

Used byRegular languages are accepted by two-way deterministic automata · Finite two-way deterministic automata accept regular languages · The two-way simulation of a DFA accepts the same language · Membership in the language of a two-way deterministic automaton

TheoremMembership in the language of a two-way deterministic automaton#✓fully proved

For every deterministic two-way automaton \(A\) and every word \(w\), \(w\) belongs to the language of \(A\) if and only if \(w\) is accepted by \(A\) viewed as a nondeterministic two-way automaton.

theorem mem_language (A : TwoWayDFA State Symbol) (xs : List Symbol) :
    xs ∈ A.language ↔ Acceptor.Accepts A.toTwoWayNA xs

Uses 3

Statement usesDeterministic two-way automaton · Language of a deterministic two-way automaton · A deterministic two-way automaton as a nondeterministic one

TheoremFinite two-way deterministic automata accept regular languages#✓fully proved

The language of every deterministic two-way automaton with finitely many states is regular.

theorem language_isRegular {State : Type} [Finite State] (A : TwoWayDFA State Symbol) :
    A.language.IsRegular

Uses 3

Statement usesDeterministic two-way automaton · Language of a deterministic two-way automaton

Proof usesA deterministic two-way automaton as a nondeterministic one

DefinitionA DFA as a two-way deterministic automaton#✓fully proved

For a DFA \(M\) with transition function \(\delta\), this is the deterministic two-way automaton with the same states, start state and accepting states as \(M\) which, in state \(q\) reading a symbol \(a\), goes to state \(\delta(q, a)\) and moves its head one symbol to the right.

def ofDFA (M : DFA Symbol State) : TwoWayDFA State Symbol where
  step q a := some (M.step q a, SignType.pos)
  start := M.start
  accept := M.accept

Uses 1 · Used by 3

Statement usesDeterministic two-way automaton

Used byRegular languages are accepted by two-way deterministic automata · The two-way simulation of a DFA accepts the same language · The two-way simulation of a DFA agrees with that of its NFA

TheoremThe two-way simulation of a DFA agrees with that of its NFA#✓fully proved

For every DFA \(M\), the deterministic two-way automaton that simulates \(M\), viewed as a nondeterministic two-way automaton, equals the nondeterministic two-way automaton obtained by viewing \(M\) as an NFA and letting that NFA always move its head one symbol to the right.

theorem toTwoWayNA_ofDFA (M : DFA Symbol State) :
    (TwoWayDFA.ofDFA M).toTwoWayNA =
      (DA.FinAcc.toNAFinAcc (DA.FinAcc.ofDFA M)).toTwoWayNA

Uses 3 · Used by 1

Statement usesMathlib DFAs as CSLib automata · A DFA as a two-way deterministic automaton · A deterministic two-way automaton as a nondeterministic one

Used byThe two-way simulation of a DFA accepts the same language

TheoremThe two-way simulation of a DFA accepts the same language#✓fully proved

For every DFA \(M\), the deterministic two-way automaton that simulates \(M\) by always moving its head one symbol to the right has exactly the language accepted by \(M\).

theorem language_ofDFA (M : DFA Symbol State) :
    (TwoWayDFA.ofDFA M).language = M.accepts

Uses 5 · Used by 1

Statement usesLanguage of a deterministic two-way automaton · A DFA as a two-way deterministic automaton

Proof usesMathlib DFAs as CSLib automata · A deterministic two-way automaton as a nondeterministic one · The two-way simulation of a DFA agrees with that of its NFA

Used byRegular languages are accepted by two-way deterministic automata

TheoremRegular languages are accepted by two-way deterministic automata#✓fully proved

For every regular language \(L\) over an alphabet, there is a deterministic two-way automaton with finitely many states whose language is exactly \(L\).

theorem exists_ofDFA_of_isRegular {L : Language Symbol} (hL : L.IsRegular) :
    ∃ (S : Type) (_ : Fintype S) (A : TwoWayDFA S Symbol), A.language = L

Uses 4

Statement usesDeterministic two-way automaton · Language of a deterministic two-way automaton

Proof usesThe two-way simulation of a DFA accepts the same language · A DFA as a two-way deterministic automaton

Automata

TheoremFinite two-way nondeterministic automata accept regular languages#✓fully proved

Every nondeterministic two-way automaton with finitely many states accepts a regular language.

A run of such an automaton on a word starts in a start state with the head at the first position; each step reads the symbol under the head, changes the state and moves the head one position left, keeps it in place, or moves it one position right, and the run is stuck if the head would move left of the first position. A word is accepted when some run ends in an accepting state with the head just past the last symbol.

theorem TwoWayNA.language_isRegular {State : Type} [Finite State] (a : TwoWayNA State Symbol) :
    (Acceptor.language a).IsRegular

TheoremRegular languages are accepted by two-way nondeterministic automata#✓fully proved

For every regular language \(L\) over an alphabet, there is a nondeterministic two-way automaton with finitely many states that accepts exactly the words of \(L\).

A run of such an automaton on a word starts in a start state with the head at the first position; each step reads the symbol under the head, changes the state and moves the head one position left, keeps it in place, or moves it one position right, and the run is stuck if the head would move left of the first position. A word is accepted when some run ends in an accepting state with the head just past the last symbol.

theorem exists_twoWayNA_of_isRegular {L : Language Symbol} (hL : L.IsRegular) :
    ∃ (S : Type) (_ : Finite S) (a : TwoWayNA S Symbol),
      Acceptor.language a = L

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.