The subregular hierarchy is star-free (aperiodicity)

Over a finite alphabet, both of the local classes SL_k and SP_k are star-free:

• Language.IsStrictlyLocal.isStarFree: SL_k ⊆ SF;
• Language.IsStrictlyPiecewise.isStarFree: SP_k ⊆ SF.

These are the "subregular hierarchy ⊆ star-free" results: each class is recognised by a finite scanner whose transition monoid (DFA.transitionMonoid) is aperiodic, hence star-free by Schützenberger's theorem ([Sch65] [McNP71]). They are gathered here — rather than in per-class …StarFree.lean files (which read like construction objects, à la mathlib's TMToPartrec), and rather than folded into the foundational StrictlyLocal / StrictlyPiecewise definition files (which would drag the heavy StarFree / TransitionMonoid imports onto every consumer of those light files). One topic-noun file isolates the heavy imports.

Constructions

• SL. The recognizer is the local scanner remembering the last k - 1 augmented symbols (a reversed window) plus an absorbing dead state none. The scanner is definite (its alive state depends only on the last k - 1 symbols), so its transition monoid is aperiodic (x ^ k = x ^ (k-1)). Boundary markers noneᵏ⁻¹ fold into the start window and acceptance set. ([McNP71] [HRT11])
• SP. The recognizer is the subsequence scanner remembering the profile of length-≤ k-1 subsequences seen so far, plus an absorbing dead state. Subsequences are blind to position, so no boundary augmentation is needed; any length-≤ k subsequence selects ≤ k symbols, so its transition monoid is aperiodic. ([HR10] [McNP71])

[Finite α] is essential throughout: these classes over an infinite alphabet need not even be regular.

Implementation notes

The SL and SP scanners share scaffolding names (scanDFA, scanHom, evalFrom_none, isStarFree_of_language_succ, …). Since private is module-scoped, each class's scaffolding is walled off in its own namespace — SLGrammar and SPGrammar — so the colliding names become distinct full names.

@[reducible, inline]

abbrev SLGrammar.Win (α : Type u_2) (n : ℕ) : Type u_2

Reversed scanner window: up to n augmented symbols, head = most recent.

Equations

• SLGrammar.Win α n = { w : List (Option α) // w.length ≤ n }

instance SLGrammar.instFiniteWin {α : Type u_1} [Finite α] (n : ℕ) : Finite (Win α n)

Aperiodicity of the transition monoid

The scanner is a definite automaton: its alive state depends only on the last n symbols read (plus the monotone dead flag). Hence reading vt n+1 or n+2 times lands in the same state — the transition monoid satisfies x ^ (n+2) = x ^ (n+1).

Recognition and the main theorem

@[reducible, inline]

abbrev SPGrammar.Sub (α : Type u_2) (n : ℕ) : Type u_2

A bounded subsequence: a list of length ≤ n, the unit a scanner profile is built from.

Equations

• SPGrammar.Sub α n = { s : List α // s.length ≤ n }

instance SPGrammar.instFiniteSub {α : Type u_1} [Finite α] (n : ℕ) : Finite (Sub α n)

@[reducible, inline]

abbrev SPGrammar.Profile (α : Type u_2) (n : ℕ) : Type u_2

A subsequence profile: the set of bounded subsequences seen so far.

Equations

• SPGrammar.Profile α n = Set (SPGrammar.Sub α n)

Aperiodicity of the transition monoid

Any subsequence of length ≤ n selects ≤ n symbols, so reading v more than n times beyond an already-v-saturated profile adds nothing new and never completes a fresh forbidden subsequence: the transition monoid satisfies x ^ (n+1) = x ^ n.

Recognition and the main theorem

theorem Language.IsStrictlyLocal.isStarFree {α : Type u_1} [Finite α] {L : Language α} {k : ℕ} (h : L.IsStrictlyLocal k) : L.IsStarFree

Strictly local languages are star-free ([McNP71]). Over a finite alphabet, the local scanner remembering the last k - 1 symbols is a finite aperiodic recognizer, so SL_k ⊆ SF. ([Finite α] is essential: SL over an infinite alphabet need not even be regular.)

theorem Language.IsStrictlyPiecewise.isStarFree {α : Type u_1} [Finite α] {L : Language α} {k : ℕ} (h : L.IsStrictlyPiecewise k) : L.IsStarFree

Strictly piecewise languages are star-free ([HR10] [McNP71]). Over a finite alphabet, the subsequence scanner remembering the length-≤ k-1 subsequences seen so far is a finite aperiodic recognizer, so SP_k ⊆ SF. ([Finite α] is essential: SP over an infinite alphabet need not even be regular.)