Finite acceptors as two-way automata

A nondeterministic finite acceptor (NA.FinAcc) is the special case of a nondeterministic two-way automaton (TwoWayNA) that moves its head one symbol to the right in every step, NA.FinAcc.toTwoWayNA.

The head of a.toTwoWayNA is thus at position i exactly when a has read the first i symbols of the input, so the runs of the two-way automaton are in lockstep with the multistep transitions of a (TwoWayNA.mTr_take_of_mTr_toCfgNA, TwoWayNA.mTr_toCfgNA_of_mTr) and the two accept the same words (TwoWayNA.accepts_toTwoWayNA_iff, TwoWayNA.language_toTwoWayNA).

def Cslib.Automata.NA.FinAcc.toTwoWayNA {State : Type u_1} {Symbol : Type u_2} (n : FinAcc State Symbol) : TwoWayNA State Symbol

The two-way automaton that performs the transitions of the nondeterministic finite acceptor n, always moving its head one symbol to the right.

Equations

• n.toTwoWayNA = { Tr := fun (q : State) (x : Symbol) (m : SignType) (q' : State) => m = SignType.pos ∧ n.Tr q x q', start := n.start, accept := n.accept }

theorem Cslib.Automata.TwoWayNA.mTr_take_of_mTr_toCfgNA {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {a : NA.FinAcc State Symbol} {c c' : TwoWayNACfg State Symbol} {μs : List (Symbol × SignType)} (hstart : c ∈ (a.toTwoWayNA.toCfgNA input).start) (hrun : (a.toTwoWayNA.toCfgNA input).MTr c μs c') : a.MTr c.state (List.take (↑c'.pos) input) c'.state

A run of a.toTwoWayNA that starts in an initial configuration reads a multistep transition of a over the prefix of input that its head has scanned.

theorem Cslib.Automata.TwoWayNA.mTr_toCfgNA_of_mTr {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {a : NA.FinAcc State Symbol} {s s' : State} {pre : List Symbol} (hpre : pre <+: input) (hmtr : a.MTr s pre s') : (a.toTwoWayNA.toCfgNA input).MTr { input := input, state := s, pos := 0 } (List.map (fun (x : Symbol) => (x, SignType.pos)) pre) { input := input, state := s', pos := ⟨pre.length, ⋯⟩ }

A multistep transition of a over a prefix of input is read by the run of a.toTwoWayNA that takes its head from the beginning of the input to the end of that prefix, moving one symbol to the right in every step.

theorem Cslib.Automata.TwoWayNA.accepts_toTwoWayNA_iff {State : Type u_1} {Symbol : Type u_2} (a : NA.FinAcc State Symbol) (input : List Symbol) : Acceptor.Accepts a.toTwoWayNA input ↔ Acceptor.Accepts a input

A nondeterministic finite acceptor and its two-way rendering accept the same words.

theorem Cslib.Automata.TwoWayNA.language_toTwoWayNA {State : Type u_1} {Symbol : Type u_2} (a : NA.FinAcc State Symbol) : Acceptor.language a.toTwoWayNA = Acceptor.language a

A nondeterministic finite acceptor and its two-way rendering recognise the same language.