Equational characterizations of the definite subregular classes

[Lam26] characterizes base classes of subregular languages by equations on the syntactic semigroup. This file gives the finite-k forms for the definite (𝒟), reverse-definite (𝒦), and generalized definite (ℒℐ) classes; the classical ω-power forms in Pin.lean are derived from them.

Main definitions

• Language.kDefiniteEquation, Language.kReverseDefiniteEquation, Language.kGeneralizedDefiniteEquation — for every syntactic-monoid element s and length-k word αs, prepending, appending, resp. sandwiching s around the class of αs fixes it (s * [αs] = [αs], [αs] * s = [αs], [αs] * s * [αs] = [αs]), where [αs] is L.syntacticClass αs.

Main results

• Language.isDefinite_iff_satisfies_kDefiniteEquation, Language.isReverseDefinite_iff_satisfies_kReverseDefiniteEquation, Language.isGeneralizedDefinite_iff_satisfies_kGeneralizedDefiniteEquation ([Lam26]) — each class equals the languages whose syntactic monoid satisfies the corresponding equation.

Implementation notes

The xᵢ range over length-k letter sequences (αs : List α), not arbitrary monoid elements: the latter is strictly weaker, ignoring L-trivial letters (e.g. (a|b)* over {a, b, c} would spuriously qualify). [Lam26] works in the syntactic semigroup (no empty word); we keep mathlib's Con (FreeMonoid α) monoid and recover the characterization through this letter-sequence quantification.

The equations

def Language.kDefiniteEquation {α : Type u_1} (L : Language α) (k : ℕ) : Prop

The definite (𝒟) equation: every length-k word's class is a right zero (∀ s, s * [αs] = [αs]).

Equations

• L.kDefiniteEquation k = ∀ (αs : List α), αs.length = k → IsRightZero (L.syntacticClass αs)

def Language.kReverseDefiniteEquation {α : Type u_1} (L : Language α) (k : ℕ) : Prop

The reverse-definite (𝒦) equation: every length-k word's class is a left zero (∀ s, [αs] * s = [αs]).

Equations

• L.kReverseDefiniteEquation k = ∀ (αs : List α), αs.length = k → IsLeftZero (L.syntacticClass αs)

def Language.kGeneralizedDefiniteEquation {α : Type u_1} (L : Language α) (k : ℕ) : Prop

The generalized-definite (ℒℐ) equation: [αs] * s * [αs] = [αs] (|αs| = k).

Equations

• L.kGeneralizedDefiniteEquation k = ∀ (s : L.syntacticMonoid) (αs : List α), αs.length = k → L.syntacticClass αs * s * L.syntacticClass αs = L.syntacticClass αs

Definite (𝒟)

theorem Language.IsDefinite.satisfies_kDefiniteEquation {α : Type u_1} {L : Language α} {k : ℕ} (hL : L.IsDefinite k) : L.kDefiniteEquation k

Forward: a k-definite language satisfies the 𝒟 equation.

theorem Language.isDefinite_of_satisfies_kDefiniteEquation {α : Type u_1} {L : Language α} {k : ℕ} (h : L.kDefiniteEquation k) : L.IsDefinite k

Reverse: the 𝒟 equation forces k-definiteness.

theorem Language.isDefinite_iff_satisfies_kDefiniteEquation {α : Type u_1} {L : Language α} {k : ℕ} : L.IsDefinite k ↔ L.kDefiniteEquation k

k-definite ↔ the 𝒟 equation.

Reverse-definite (𝒦) — by reverse duality

theorem Language.kReverseDefiniteEquation_iff_reverse {α : Type u_1} {L : Language α} {k : ℕ} : L.kReverseDefiniteEquation k ↔ L.reverse.kDefiniteEquation k

The 𝒦 equation for L is the 𝒟 equation for L.reverse.

theorem Language.isReverseDefinite_iff_satisfies_kReverseDefiniteEquation {α : Type u_1} {L : Language α} {k : ℕ} : L.IsReverseDefinite k ↔ L.kReverseDefiniteEquation k

reverse-k-definite ↔ the 𝒦 equation (reverse duality with 𝒟).

theorem Language.IsReverseDefinite.satisfies_kReverseDefiniteEquation {α : Type u_1} {L : Language α} {k : ℕ} (hL : L.IsReverseDefinite k) : L.kReverseDefiniteEquation k

Forward: a reverse-k-definite language satisfies the 𝒦 equation.

theorem Language.isReverseDefinite_of_satisfies_kReverseDefiniteEquation {α : Type u_1} {L : Language α} {k : ℕ} (h : L.kReverseDefiniteEquation k) : L.IsReverseDefinite k

Reverse: the 𝒦 equation forces reverse-k-definiteness.

Generalized definite (ℒℐ)

theorem Language.IsGeneralizedDefinite.satisfies_kGeneralizedDefiniteEquation {α : Type u_1} {L : Language α} {k : ℕ} (hL : L.IsGeneralizedDefinite k) : L.kGeneralizedDefiniteEquation k

Forward: a generalized-k-definite language satisfies the ℒℐ equation.

theorem Language.isGeneralizedDefinite_of_satisfies_kGeneralizedDefiniteEquation {α : Type u_1} {L : Language α} {k : ℕ} (h : L.kGeneralizedDefiniteEquation k) : L.IsGeneralizedDefinite k

Reverse: the ℒℐ equation forces generalized-k-definiteness.

theorem Language.isGeneralizedDefinite_iff_satisfies_kGeneralizedDefiniteEquation {α : Type u_1} {L : Language α} {k : ℕ} : L.IsGeneralizedDefinite k ↔ L.kGeneralizedDefiniteEquation k

generalized-k-definite ↔ the ℒℐ equation.