Documentation

Linglib.Core.Computability.Variety.Definite

Definite languages and the pseudovarieties D and K #

The Eilenberg correspondence sends the pseudovariety D of definite semigroups to the definite languages, and K to the reverse-definite ones ([Eil76] Ch. VIII, [Pin]). This file proves both correspondences over a finite alphabet.

The forward half rests on screening: a k-definite language cannot see anything prepended to a word of length ≥ k, because the prepended block falls outside the length-k window (List.rtake_append_append_of_le_length). Idempotence supplies representatives of unbounded length, which turns the language statement into the semigroup equation s * e = e. The reverse-definite case mirrors this through the left edge.

The converse half is not reproved here. Variety.OmegaEquations already algebraizes these classes — and LI and N — as omega-power equations on the syntactic monoid, converses included. This file relates the two presentations by transporting along syntacticSemigroupToMonoid, whose range is everything but the class of the empty word, and then reads the converses off Pin's theorems.

Main results #

Shared machinery #

Definite languages and D #

source
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

Screening, right edge. A k-definite language is blind to a prefix prepended to a word of length ≥ k: the length-k window never reaches past u.

source
theorem Language.IsDefinite.syntacticEquiv_of_rtake_eq {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsDefinite k) {u v : List α} (huv : u.rtake k = v.rtake k) :
L.SyntacticEquiv u v

Words sharing their length-k suffix are L-equivalent — definiteness restated as a bound on the syntactic congruence.

source
theorem Language.IsDefinite.isRegular {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : L.IsDefinite k) :
L.IsRegular

A definite language over a finite alphabet is regular — the length-k suffix picks a bounded representative from each syntactic class.

source
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: s * e = e for idempotent e. Idempotence lets e be represented by an arbitrarily long word, and screening then makes the left factor invisible.

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

The language half of D: a definite language over a finite alphabet lies in the language variety of the pseudovariety D.

Reverse-definite languages and K #

The mirror through the left edge. Screening is cheaper here, since List.take_append_of_le_length already says a long enough prefix ignores what follows.

source
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

Screening, left edge. A reverse-k-definite language is blind to a suffix appended to a word of length ≥ k.

source
theorem Language.IsReverseDefinite.syntacticEquiv_of_take_eq {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsReverseDefinite k) {u v : List α} (huv : List.take k u = List.take k v) :
L.SyntacticEquiv u v

Words sharing their length-k prefix are L-equivalent.

source
theorem Language.IsReverseDefinite.isRegular {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : L.IsReverseDefinite k) :
L.IsRegular

A reverse-definite language over a finite alphabet is regular — the length-k prefix picks a bounded representative from each syntactic class.

source
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: e * s = e for idempotent e.

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

The language half of K: a reverse-definite language over a finite alphabet lies in the language variety of the pseudovariety K.

Agreement with the omega-power equations #

Variety.OmegaEquations algebraizes the same classes as equations on the syntactic monoid. The two presentations agree: syntacticSemigroupToMonoid is injective, its range is everything but the class of the empty word, and idempotents correspond to omega-powers of classes of nonempty words. Transporting across it turns the pseudovariety statements into Pin's equations, and so yields the langs characterisations from the omega-power theorems.

source
theorem Language.isDefinite_syntacticSemigroup_iff_omegaDefiniteEquation {α : Type u_1} {L : Language α} [Finite L.SyntacticMonoid] :
Semigroup.IsDefinite L.SyntacticSemigroup ↔ L.omegaDefiniteEquation

The two algebraizations of D agree: the syntactic semigroup is definite exactly when the syntactic monoid satisfies Pin's omega-power equation.

source
theorem Language.isReverseDefinite_syntacticSemigroup_iff_omegaReverseDefiniteEquation {α : Type u_1} {L : Language α} [Finite L.SyntacticMonoid] :
Semigroup.IsReverseDefinite L.SyntacticSemigroup ↔ L.omegaReverseDefiniteEquation

The two algebraizations of K agree — the mirror of isDefinite_syntacticSemigroup_iff_omegaDefiniteEquation.

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

Eilenberg's correspondence for D: the language variety of the pseudovariety D is exactly the definite languages.

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

Eilenberg's correspondence for K: the language variety of the pseudovariety K is exactly the reverse-definite languages.