The subregular hierarchy is star-free (aperiodicity)

Over a finite alphabet, each of the local classes SL_k, TSL_k, SP_k is star-free:

• Language.IsStrictlyLocal.isStarFree — SL_k ⊆ SF;
• Language.IsTierStrictlyLocal.isStarFree — TSL_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 / TierStrictlyLocal 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])
• TSL. A TSL language is the preimage tierProject T ⁻¹' (permitted.language k) under tier erasure, which is List.filter and hence a monoid hom Subregular.tierProjectHom. The permitted-factor language is SL_k, star-free by IsStrictlyLocal.isStarFree, and star-freeness is closed under inverse homomorphism (Language.IsStarFree.comap), so TSL_k ⊆ SF. ([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 — Subregular.SL and Subregular.SP — so the colliding names become distinct full names. The TSL helper tierProjectHom (which other modules may consume) stays public in Subregular.

@[reducible, inline]

abbrev Subregular.SL.Win (α : Type u_2) (n : ℕ) : Type u_2

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

Equations

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

instance Subregular.SL.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 Subregular.SP.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

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

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

@[reducible, inline]

abbrev Subregular.SP.Profile (α : Type u_2) (n : ℕ) : Type u_2

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

Equations

• Subregular.SP.Profile α n = Set (Subregular.SP.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

def Subregular.tierProjectHom {α : Type u_1} (T : α → Prop) [DecidablePred T] : FreeMonoid α →* FreeMonoid α

Tier erasure as a monoid hom FreeMonoid α →* FreeMonoid α: the byClass T specialization of the keystone bundled hom TierProjection.applyHom. The monoid-hom laws are inherited from applyHom rather than re-proved, since tierProject T is by definition TierProjection.apply (TierProjection.byClass T).

Equations

• Subregular.tierProjectHom T = (TierProjection.byClass T).applyHom

@[simp]

theorem Subregular.tierProjectHom_apply {α : Type u_1} (T : α → Prop) [DecidablePred T] (w : FreeMonoid α) : (tierProjectHom T) w = tierProject T w

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.IsTierStrictlyLocal.isStarFree {α : Type u_1} [Finite α] {k : ℕ} {L : Language α} (h : IsTierStrictlyLocal k L) : L.IsStarFree

Tier-based strictly local languages are star-free ([HRT11]). Over a finite alphabet, a TSL language is the inverse image of an SL_k language under the tier-erasure homomorphism, and star-freeness is closed under inverse homomorphism (IsStarFree.comap), so TSL_k ⊆ SF.

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.)