Documentation

Complexitylib.Interop.Cslib.Regular

Regular languages in Complexitylib's classes #

Every language that is regular in the sense shared by Mathlib and CSLib (Language.IsRegular: accepted by a finite deterministic automaton) is decided by Complexitylib's finite-state scanner TM.scannerTM, which runs the automaton left to right over the input. The scanner halts in n + 2 steps, has no work tapes, never moves its input head past the first blank after the input, and never moves its output head past the verdict cell. It therefore decides the language in time n + 2 and in zero auxiliary space under Cfg.WithinDecisionSpace, and, since its output head never moves left, it is a transducer. Regular languages thus lie in DTIME(n + 2), P, DSPACE(0), and L.

CSLib's characterizations of regularity then transfer these memberships to the languages of finite nondeterministic automata, of finite two-way nondeterministic automata, of regular expressions, and to preimages of subsets of finite monoids under homomorphisms from the free monoid on Bool.

Main results #

CSLib's closure properties of regular languages (union, intersection, complement, concatenation, Kleene star, reversal, inverse homomorphic images) combine with mem_L_of_isRegular to give L-membership of the resulting languages directly.

source
theorem Complexity.TM.scannerTM_isTransducer {S : Type} [DecidableEq S] [Fintype S] (s₀ : S) (scanStep : S → Bool → S) (finalOutput : S → Γw) :
(scannerTM s₀ scanStep finalOutput).IsTransducer

The scanner never moves its output head left, so it is a transducer.

source
theorem Complexity.TM.scannerTM_decidesInSpace {S : Type} [DecidableEq S] [Fintype S] (s₀ : S) (scanStep : S → Bool → S) (accept : S → Bool) {L : Language} (hL : ∀ (x : List Bool), x ∈ L ↔ accept (List.foldl scanStep s₀ x) = true) :
(scannerTM s₀ scanStep fun (s : S) => if accept s = true then Γw.one else Γw.zero).DecidesInSpace L fun (x : ℕ) => 0

The scanner runs in zero auxiliary space. Whenever a language L is characterized by a decision predicate accept : S → Bool applied to the fold, the scanner decides L in space 0 under Cfg.WithinDecisionSpace: it has no work tapes, its input head never passes the first blank after the input, and its output head never passes the verdict cell.

source
theorem Complexity.mem_DTIME_of_isRegular {A : Language} (hA : Language.IsRegular A) :
A ∈ DTIME fun (n : ℕ) => n + 2

Regular languages are decidable in linear time. Every language that is regular in the sense shared by Mathlib and CSLib (accepted by a finite deterministic automaton) is decided in n + 2 steps by the finite-state scanner that runs the automaton.

source
theorem Complexity.mem_P_of_isRegular {A : Language} (hA : Language.IsRegular A) :
A ∈ P

Regular languages are in P.

source
theorem Complexity.mem_DSPACE_zero_of_isRegular {A : Language} (hA : Language.IsRegular A) :
A ∈ DSPACE fun (x : ℕ) => 0

Regular languages are decidable in zero auxiliary space. Every regular language is decided by the finite-state scanner, which uses no work tape and keeps its input and output heads within the free region of Cfg.WithinDecisionSpace.

source
theorem Complexity.mem_DSPACE_of_isRegular {A : Language} (hA : Language.IsRegular A) (S : ℕ → ℕ) :
A ∈ DSPACE S

Regular languages lie in every space class. Zero auxiliary space is O(S) for every bound S.

source
theorem Complexity.mem_L_of_isRegular {A : Language} (hA : Language.IsRegular A) :
A ∈ L

Regular languages are in L. The finite-state scanner is a transducer deciding the language in zero auxiliary space.

CSLib automata and algebraic characterizations #

source
theorem Complexity.mem_P_of_nfa {State : Type} [Finite State] (nfa : Cslib.Automata.NA.FinAcc State Bool) :
Cslib.Automata.Acceptor.language nfa ∈ P

Finite nondeterministic automata decide in polynomial time. Every language accepted by a finite nondeterministic automaton from CSLib's automata library is in P: CSLib's subset construction makes it regular, and the scanner runs the resulting deterministic automaton.

source
theorem Complexity.mem_L_of_nfa {State : Type} [Finite State] (nfa : Cslib.Automata.NA.FinAcc State Bool) :
Cslib.Automata.Acceptor.language nfa ∈ L

Finite nondeterministic automata decide in logarithmic space. Every language accepted by a finite nondeterministic automaton from CSLib's automata library is in L.

source
theorem Complexity.mem_P_of_twoWayNA {State : Type} [Finite State] (a : Cslib.Automata.TwoWayNA State Bool) :
Cslib.Automata.Acceptor.language a ∈ P

Two-way automata decide in polynomial time. Every language accepted by a finite two-way nondeterministic automaton from CSLib is in P: CSLib proves such languages regular.

source
theorem Complexity.mem_L_of_twoWayNA {State : Type} [Finite State] (a : Cslib.Automata.TwoWayNA State Bool) :
Cslib.Automata.Acceptor.language a ∈ L

Two-way automata decide in logarithmic space. Every language accepted by a finite two-way nondeterministic automaton from CSLib is in L.

source
theorem Complexity.mem_P_of_finite_monoid {M : Type u_1} [Monoid M] [Finite M] (f : FreeMonoid Bool →* M) (s : Set M) :
⇑f ∘ ⇑FreeMonoid.ofList ⁻¹' s ∈ P

Finite-monoid recognizable languages are in P. The preimage of any subset of a finite monoid under a monoid homomorphism from the free monoid on Bool is in P: CSLib proves such preimages regular.

source
theorem Complexity.mem_L_of_finite_monoid {M : Type u_1} [Monoid M] [Finite M] (f : FreeMonoid Bool →* M) (s : Set M) :
⇑f ∘ ⇑FreeMonoid.ofList ⁻¹' s ∈ L

Finite-monoid recognizable languages are in L. The preimage of any subset of a finite monoid under a monoid homomorphism from the free monoid on Bool is in L.

source
theorem Complexity.mem_L_of_regex (r : RegularExpression Bool) :
r.matches' ∈ L

Regular expressions match in logarithmic space. The language matched by any regular expression over Bool is in L, since CSLib proves it regular.