Definite languages and the pseudovarieties D, K and LI

This file proves the Eilenberg correspondences for the definite languages and their relatives. Over a finite alphabet, the definite, reverse definite and generalized definite languages are exactly the regular languages whose syntactic semigroup lies in the pseudovariety D, K and LI respectively, and the finite or cofinite languages are those whose syntactic semigroup lies in both D and K. Both directions pass through a window characterization in the syntactic monoid: L is k-definite exactly when the class of every word of length at least k is a right zero, and similarly for the other two classes.

Main results

• Language.isDefinite_iff_forall_isRightZero_syntacticClass and its two mirrors: the windows.
• Language.IsDefinite.isRightZero_syntacticClass_of_isIdempotentElem and its two mirrors: an idempotent class of a nonempty word satisfies the window condition.
• Language.isDefinite_natCard_of_isDefinite_syntacticSemigroup and its two mirrors: a syntactic semigroup S in the pseudovariety bounds the window by |S|.
• Language.langs_definiteVariety_iff, Language.langs_reverseDefiniteVariety_iff, Language.langs_locallyTrivialVariety_iff: the Eilenberg correspondences.
• Language.isFiniteOrCofinite_iff_syntacticSemigroup: the finite or cofinite languages.

Implementation notes

The bound |S| and the route through long products follow Chapter XIV of Pin's lecture notes. The window conditions range over words of length at least k rather than over the whole syntactic monoid, because the pseudovarieties are varieties of semigroups and do not see the empty word.

References

• [PRS63]
• [Eil76]
• [Pin]

Window characterizations

Definite languages

theorem Language.IsDefinite.syntacticEquiv_append_left {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsDefinite k) {u : List α} (hu : k ≤ u.length) (t : List α) : L.SyntacticEquiv (t ++ u) u

A k-definite language is blind to a prefix prepended to a word of length at least k, since the length-k window never reaches past the word.

theorem Language.IsDefinite.isRightZero_syntacticClass {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsDefinite k) {u : List α} (hu : k ≤ u.length) : IsRightZero (L.syntacticClass u)

theorem Language.isDefinite_iff_forall_isRightZero_syntacticClass {α : Type u_1} {L : Language α} {k : ℕ} : L.IsDefinite k ↔ ∀ (u : List α), k ≤ u.length → IsRightZero (L.syntacticClass u)

A language is k-definite exactly when the syntactic class of every word of length at least k is a right zero of the syntactic monoid.

Reverse definite languages

theorem Language.IsReverseDefinite.syntacticEquiv_append_right {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsReverseDefinite k) {u : List α} (hu : k ≤ u.length) (t : List α) : L.SyntacticEquiv (u ++ t) u

A reverse k-definite language is blind to a suffix appended to a word of length at least k.

theorem Language.IsReverseDefinite.isLeftZero_syntacticClass {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsReverseDefinite k) {u : List α} (hu : k ≤ u.length) : IsLeftZero (L.syntacticClass u)

theorem Language.isReverseDefinite_iff_forall_isLeftZero_syntacticClass {α : Type u_1} {L : Language α} {k : ℕ} : L.IsReverseDefinite k ↔ ∀ (u : List α), k ≤ u.length → IsLeftZero (L.syntacticClass u)

A language is reverse k-definite exactly when the syntactic class of every word of length at least k is a left zero of the syntactic monoid.

Generalized definite languages

theorem Language.IsGeneralizedDefinite.syntacticEquiv_append_append {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsGeneralizedDefinite k) {u : List α} (hu : k ≤ u.length) (t : List α) : L.SyntacticEquiv (u ++ t ++ u) u

A generalized k-definite language is blind to anything placed between two copies of a word of length at least k.

theorem Language.IsGeneralizedDefinite.syntacticClass_mul_mul_self {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsGeneralizedDefinite k) {u : List α} (hu : k ≤ u.length) (s : L.SyntacticMonoid) : L.syntacticClass u * s * L.syntacticClass u = L.syntacticClass u

theorem Language.isGeneralizedDefinite_iff_forall_syntacticClass_mul_mul_self {α : Type u_1} {L : Language α} {k : ℕ} : L.IsGeneralizedDefinite k ↔ ∀ (u : List α), k ≤ u.length → ∀ (s : L.SyntacticMonoid), L.syntacticClass u * s * L.syntacticClass u = L.syntacticClass u

A language is generalized k-definite exactly when the syntactic class of every word of length at least k absorbs anything placed between two copies of it.

Idempotent classes

An idempotent class of a nonempty word is also the class of arbitrarily long words, so it satisfies the window condition of every window.

theorem Language.IsDefinite.isRightZero_syntacticClass_of_isIdempotentElem {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsDefinite k) {u : List α} (hu : u ≠ []) (he : IsIdempotentElem (L.syntacticClass u)) : IsRightZero (L.syntacticClass u)

In a definite language, an idempotent class of a nonempty word is a right zero.

theorem Language.IsReverseDefinite.isLeftZero_syntacticClass_of_isIdempotentElem {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsReverseDefinite k) {u : List α} (hu : u ≠ []) (he : IsIdempotentElem (L.syntacticClass u)) : IsLeftZero (L.syntacticClass u)

In a reverse definite language, an idempotent class of a nonempty word is a left zero.

theorem Language.IsGeneralizedDefinite.syntacticClass_mul_mul_self_of_isIdempotentElem {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsGeneralizedDefinite k) {u : List α} (hu : u ≠ []) (he : IsIdempotentElem (L.syntacticClass u)) (s : L.SyntacticMonoid) : L.syntacticClass u * s * L.syntacticClass u = L.syntacticClass u

In a generalized definite language, an idempotent class of a nonempty word absorbs anything placed between two copies of it.

The syntactic semigroup

theorem Language.isRightZero_iff_forall_syntacticSemigroupToMonoid_mul {α : Type u_1} {L : Language α} {x : L.SyntacticMonoid} : IsRightZero x ↔ ∀ (s : L.SyntacticSemigroup), L.syntacticSemigroupToMonoid s * x = x

An element of the syntactic monoid is a right zero once it absorbs the image of the syntactic semigroup, since everything else is the identity.

theorem Language.isLeftZero_iff_forall_mul_syntacticSemigroupToMonoid {α : Type u_1} {L : Language α} {x : L.SyntacticMonoid} : IsLeftZero x ↔ ∀ (s : L.SyntacticSemigroup), x * L.syntacticSemigroupToMonoid s = x

From the language to the semigroup

theorem Language.IsDefinite.isDefinite_syntacticSemigroup {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsDefinite k) : Semigroup.IsDefinite L.SyntacticSemigroup

The syntactic semigroup of a definite language is definite.

theorem Language.IsReverseDefinite.isReverseDefinite_syntacticSemigroup {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsReverseDefinite k) : Semigroup.IsReverseDefinite L.SyntacticSemigroup

The syntactic semigroup of a reverse definite language is reverse definite.

theorem Language.IsGeneralizedDefinite.isLocallyTrivial_syntacticSemigroup {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsGeneralizedDefinite k) : Semigroup.IsLocallyTrivial L.SyntacticSemigroup

The syntactic semigroup of a generalized definite language is locally trivial.

From the semigroup to the language

theorem Language.isDefinite_natCard_of_isDefinite_syntacticSemigroup {α : Type u_1} {L : Language α} [Finite L.SyntacticSemigroup] (h : Semigroup.IsDefinite L.SyntacticSemigroup) : L.IsDefinite (Nat.card L.SyntacticSemigroup)

A language with a definite syntactic semigroup S is |S|-definite.

theorem Language.isReverseDefinite_natCard_of_isReverseDefinite_syntacticSemigroup {α : Type u_1} {L : Language α} [Finite L.SyntacticSemigroup] (h : Semigroup.IsReverseDefinite L.SyntacticSemigroup) : L.IsReverseDefinite (Nat.card L.SyntacticSemigroup)

A language with a reverse definite syntactic semigroup S is reverse |S|-definite.

theorem Language.isGeneralizedDefinite_natCard_of_isLocallyTrivial_syntacticSemigroup {α : Type u_1} {L : Language α} [Finite L.SyntacticSemigroup] (h : Semigroup.IsLocallyTrivial L.SyntacticSemigroup) : L.IsGeneralizedDefinite (Nat.card L.SyntacticSemigroup)

A language with a locally trivial syntactic semigroup S is generalized |S|-definite.

theorem Language.isDefinite_syntacticSemigroup_iff {α : Type u_1} {L : Language α} [Finite L.SyntacticSemigroup] : Semigroup.IsDefinite L.SyntacticSemigroup ↔ ∃ (k : ℕ), L.IsDefinite k

theorem Language.isReverseDefinite_syntacticSemigroup_iff {α : Type u_1} {L : Language α} [Finite L.SyntacticSemigroup] : Semigroup.IsReverseDefinite L.SyntacticSemigroup ↔ ∃ (k : ℕ), L.IsReverseDefinite k

theorem Language.isLocallyTrivial_syntacticSemigroup_iff {α : Type u_1} {L : Language α} [Finite L.SyntacticSemigroup] : Semigroup.IsLocallyTrivial L.SyntacticSemigroup ↔ ∃ (k : ℕ), L.IsGeneralizedDefinite k

theorem Language.isFiniteOrCofinite_iff_syntacticSemigroup {α : Type u_1} {L : Language α} [Finite L.SyntacticSemigroup] [Finite α] : L.IsFiniteOrCofinite ↔ Semigroup.IsDefinite L.SyntacticSemigroup ∧ Semigroup.IsReverseDefinite L.SyntacticSemigroup

Over a finite alphabet, a language with a finite syntactic semigroup is finite or cofinite exactly when its syntactic semigroup is both definite and reverse definite.

The Eilenberg correspondences

theorem Language.IsDefinite.langs {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : L.IsDefinite k) : Semigroup.definiteVariety.langs L

A definite language over a finite alphabet lies in the language variety of D.

theorem Language.IsReverseDefinite.langs {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : L.IsReverseDefinite k) : Semigroup.reverseDefiniteVariety.langs L

A reverse definite language over a finite alphabet lies in the language variety of K.

theorem Language.IsGeneralizedDefinite.langs {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : L.IsGeneralizedDefinite k) : Semigroup.locallyTrivialVariety.langs L

A generalized definite language over a finite alphabet lies in the language variety of LI.

theorem Language.langs_definiteVariety_iff {α : Type u_1} {L : Language α} [Finite α] : Semigroup.definiteVariety.langs L ↔ ∃ (k : ℕ), L.IsDefinite k

The language variety of D consists of the definite languages.

theorem Language.langs_reverseDefiniteVariety_iff {α : Type u_1} {L : Language α} [Finite α] : Semigroup.reverseDefiniteVariety.langs L ↔ ∃ (k : ℕ), L.IsReverseDefinite k

The language variety of K consists of the reverse definite languages.

theorem Language.langs_locallyTrivialVariety_iff {α : Type u_1} {L : Language α} [Finite α] : Semigroup.locallyTrivialVariety.langs L ↔ ∃ (k : ℕ), L.IsGeneralizedDefinite k

The language variety of LI consists of the generalized definite languages.