Nondeterministic Two-Way Automaton

A Nondeterministic Two-Way Automaton (TwoWayNA) reads a finite input word on a tape and may move its input head in either direction. A transition reads the symbol under the head and, besides changing the state, moves the head one cell to the left, keeps it in place, or moves it one cell to the right.

The input head cannot leave the input word to the left (in the sense that execution gets stuck in this case) and once it leaves the word to the right, it stops. A run is accepting if and only if it ends in an accepting state with the head just past the end of the input.

Main definitions

• TwoWayNA, the automaton itself
• TwoWayNACfg, a configuration of a TwoWayNA: Its input plus a state and the head position.
• TwoWayNA.toCfgNA, the finite acceptor on configurations whose runs on a fixed input are the runs of the two-way automaton on that input. It also provides the Acceptor instance.

Implementation notes

The definition of TwoWayNA is kept close to Vardi's, because the main point is to prove that it accepts the same languages as NA.FinAcc via his proof. This means we do not allow the head to move off the input to the left (in the sense that if the transition relation has an entry that would cause that, there is no successor configuration, the computation is stuck), but also do not provide an end marker. Once the head moves off to the right, the machine instantly stops, so it also cannot move back into the word.

References

• Moshe Y. Vardi, A Note on the Reduction of Two-Way Automata to One-Way Automata

structure Cslib.Automata.TwoWayNA (State : Type u_3) (Symbol : Type u_4) : Type (max u_3 u_4)

A nondeterministic two-way automaton: a transition relation that reads an input symbol and moves the input head, together with a set of initial and a set of accepting states.

• Tr (q : State) (x : Symbol) (m : SignType) (q' : State) : Prop

  The transition relation. Tr q x m q' means that, while reading the symbol x, the automaton attempts to transition from state q to state q' and move its head according to m.

• start : Set State

  The set of initial states of the automaton.

• accept : Set State

  The set of accepting states of the automaton.

structure Cslib.Automata.TwoWayNACfg (State : Type u_3) (Symbol : Type u_4) : Type (max u_3 u_4)

The configuration of a two-way nondeterministic automaton.

• input : List Symbol

  The original input to the automaton.

• state : State

  The state of the automaton.

• pos : Fin (self.input.length + 1)

  The input head position of the automaton: it can be on any symbol of the input or on the position one step to the right of the input.

theorem Cslib.Automata.TwoWayNACfg.ext_iff {State : Type u_3} {Symbol : Type u_4} {x y : TwoWayNACfg State Symbol} : x = y ↔ x.input = y.input ∧ x.state = y.state ∧ x.pos ≍ y.pos

theorem Cslib.Automata.TwoWayNACfg.ext {State : Type u_3} {Symbol : Type u_4} {x y : TwoWayNACfg State Symbol} (input : x.input = y.input) (state : x.state = y.state) (pos : x.pos ≍ y.pos) : x = y

def Cslib.Automata.TwoWayNACfg.IsInitialForInput {State : Type u_1} {Symbol : Type u_2} (a : TwoWayNA State Symbol) (c : TwoWayNACfg State Symbol) (input : List Symbol) : Prop

This defines the set of initial configurations on a specific input.

Equations

• Cslib.Automata.TwoWayNACfg.IsInitialForInput a c input = (c.state ∈ a.start ∧ c.pos = 0 ∧ c.input = input)

def Cslib.Automata.TwoWayNACfg.IsAccepting {State : Type u_1} {Symbol : Type u_2} (a : TwoWayNA State Symbol) (c : TwoWayNACfg State Symbol) : Prop

If a configuration is a accepting.

Equations

• Cslib.Automata.TwoWayNACfg.IsAccepting a c = (c.state ∈ a.accept ∧ c.pos = Fin.last c.input.length)

def Cslib.Automata.TwoWayNA.toCfgNA {State : Type u_3} {Symbol : Type u_4} (a : TwoWayNA State Symbol) (input : List Symbol) : NA.FinAcc (TwoWayNACfg State Symbol) (Symbol × SignType)

Returns a nondeterministic finite acceptor on the configurations as states, accepting exactly the runs of the two-way automaton on input that end in an accepting configuration.

Equations

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

@[instance_reducible]

instance Cslib.Automata.instAcceptorTwoWayNA {State : Type u_1} {Symbol : Type u_2} : Acceptor (TwoWayNA State Symbol) Symbol

Equations

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

theorem Cslib.Automata.TwoWayNA.toCfgNA_input_eq {State : Type u_3} {Symbol : Type u_4} (a : TwoWayNA State Symbol) (input : List Symbol) : (a.toCfgNA input).TrInv fun (c : TwoWayNACfg State Symbol) => c.input = input

Any reachable state of a.toCfgNA input contains the original input.

theorem Cslib.Automata.TwoWayNACfg.eta {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {c : TwoWayNACfg State Symbol} (h : c.input = input) (h' : ↑c.pos < input.length + 1) : { input := input, state := c.state, pos := ⟨↑c.pos, h'⟩ } = c

A configuration running on input is the one determined by its state and head position.

theorem Cslib.Automata.TwoWayNA.getElem_of_tr {State : Type u_1} {Symbol : Type u_2} {a : TwoWayNA State Symbol} {input : List Symbol} {c c' : TwoWayNACfg State Symbol} {x : Symbol} {m : SignType} (htr : (a.toCfgNA input).Tr c (x, m) c') (hc : c.input = input) : ∃ (h : ↑c.pos < input.length), input[↑c.pos] = x

A step reads the symbol at the head position, which therefore lies inside the input.