feat(Automata): Two-way automata accept exactly the regular languages - #888
feat(Automata): Two-way automata accept exactly the regular languages#888crei wants to merge 4 commits into
Conversation
crei
changed the title
| automaton with finitely many states. -/ | ||
| public theorem IsRegular.iff_twoWayNA {Symbol : Type*} {l : Language Symbol} : | ||
| l.IsRegular ↔ ∃ State : Type, ∃ _ : Finite State, | ||
| ∃ a : Automata.TwoWayNA State Symbol, language a = l := by |
There was a problem hiding this comment.
The Automata. prefix is unnecessary.
| public import Cslib.Computability.Automata.TwoWayNA.Basic | ||
| public import Cslib.Foundations.Semantics.LTS.Relation | ||
|
|
||
| /-! # A finite acceptor for the complement of the language of a two-way automaton |
There was a problem hiding this comment.
I think this file should be renamed to ComplToNA.lean.
|
|
||
| For every nondeterministic two-way automaton (`TwoWayNA`) `a`, this file constructs a | ||
| nondeterministic finite acceptor (`NA.FinAcc`) that accepts exactly the words rejected by `a` | ||
| (`TwoWayNA.toNAComplement`, `TwoWayNA.language_toNAComplement`). We follow Vardi's proof, which -- |
There was a problem hiding this comment.
I think complToNA is better than toNAComplement.
| exact List.getElem?_eq_some_iff.mp hx.symm | ||
|
|
||
| @[simp, scoped grind =] | ||
| instance : Acceptor (TwoWayNA State Symbol) Symbol where |
There was a problem hiding this comment.
I would move this instance definition to immediately after the TwoWayNA.toCfgNAFinAcc definition, before starting proving theorems.
|
|
||
| /-- A nondeterministic finite acceptor and its two-way rendering accept the same words. -/ | ||
| theorem accepts_ofNA_iff (a : NA.FinAcc State Symbol) (input : List Symbol) : | ||
| Acceptor.Accepts (ofNA a) input ↔ Acceptor.Accepts a input := by |
There was a problem hiding this comment.
open Acceptor, so that all the Acceptor. prefixes become unnecessary.
| public import Cslib.Computability.Automata.TwoWayNA.OfNA | ||
| public import Cslib.Computability.Automata.TwoWayNA.ToNA | ||
| public import Cslib.Computability.Languages.RegularLanguage |
There was a problem hiding this comment.
Since Vardi's proof doesn't use the Myhill-Nerode theorem, I think you can move the contents of this file into Cslib.Computability.Languages.RegularLanguage itself, rather than creating a new dependency.
|
|
||
| /-- Every move of `a` out of a state in `C` while reading `x` lands in `P`, in `C` or in `N`, | ||
| according to whether it moves the head to the left, keeps it in place, or moves it to the right. -/ | ||
| def LocalOK (a : TwoWayNA State Symbol) (x : Symbol) (P C N : Set State) : Prop := |
There was a problem hiding this comment.
The naming convention says names of things of type Set State should begin with a lowercase letter.
Also, it is a bit confusing that .neg => P and .pos => N reverse the first letters. Perhaps instead of P C N, we have ns cs ps?
|
|
||
| /-- The subset that `T` attaches to the position to the left of `i`, and everything at position | ||
| `0`, which has no position to its left. -/ | ||
| def prevSet (T : ℕ → Set State) : ℕ → Set State |
There was a problem hiding this comment.
I think you should consider using ωSequence (Set State) as the type of T. Then prevSet T can be written as Set.univ ::ω T, which is clearer. See also the comment about certToList below.
| Tr PC x PC' := PC'.1 = PC.2 ∧ a.LocalOK x PC.1 PC.2 PC'.2 | ||
| start := {PC | PC.1 = Set.univ ∧ a.start ⊆ PC.2} | ||
| accept := {PC | ∀ s ∈ PC.2, s ∉ a.accept} |
There was a problem hiding this comment.
Names of objects of type Set State should begin with lowercase letters.
| def certToList (input : List Symbol) (T : ℕ → Set State) : List (Set State) := | ||
| Set.univ :: (List.range (input.length + 1)).map T |
There was a problem hiding this comment.
If the type of T is ωSequence (Set State), then we can write:
Set.univ :: T.take (input.length + 1)
2 participants
This implements Vardi's construction of a (one-way) finite automaton that accepts the complement of the language accepted by a two-way automaton. Together with closure of regular languages under complement and a simple mapping of one-way automata to two-way automata we get that two-way automata accept exactly the regular languages.
AI disclosure: Claude was used throughout bit in a tight review loop.