Myhill congruence

The Myhill congruence of a language l is a two-sided congruence that is finer than the Nerode congruence of the same language l (which is a right congruence). It will be used to define the syntactic monoid of l.

References

[Hol82] Holcombe, W.M.L. (1982). Algebraic automata theory. Section 5.3

@[implicit_reducible]

def Language.MyhillCongruence {α : Type} (l : Language α) : Congruence α

The Myhill congruence of a language l is the two-sided congruence on finite words such that two words are related iff all their two-sided extensions are either both in l or both not in l.

Equations

• l.MyhillCongruence = { r := fun (x y : List α) => ∀ (w z : List α), w ++ x ++ z ∈ l ↔ w ++ y ++ z ∈ l, iseqv := ⋯, left_cov := ⋯, right_cov := ⋯ }

@[reducible, inline]

abbrev Language.MyhillQuotient {α : Type} (l : Language α) : Type

The Myhill quotient of a language l is the quotient of its Myhill congruence.

Equations

• l.MyhillQuotient = Quotient l.MyhillCongruence.eq

def Language.nerodeMap {α : Type} (l : Language α) (x : List α) : l.NerodeQuotient → l.NerodeQuotient

Given a language l and a finite word x, the Nerode map is a map from the Nerode quotient to itself induced by the x-transition of the Nerode congruence deterministic automaton of l.

Equations

• l.nerodeMap x q = l.NerodeCongruenceDA.mtr q x

theorem Language.nerodeMap_append {α : Type} (l : Language α) (x y : List α) : l.nerodeMap (x ++ y) = l.nerodeMap y ∘ l.nerodeMap x

theorem Language.nerodeMap_accept {α : Type} (l : Language α) (x : List α) : x ∈ l ↔ l.nerodeMap x l.NerodeCongruenceDA.start ∈ l.NerodeCongruenceDA.accept

theorem Language.myhillCongruence_iff {α : Type} (l : Language α) (x y : List α) : l.MyhillCongruence.eq x y ↔ l.nerodeMap x = l.nerodeMap y

The Myhill congruence is in fact the congruence induced by the Nerode map.

theorem Language.IsRegular.finite_myhillQuotient {α : Type} {l : Language α} (h : l.IsRegular) : Finite l.MyhillQuotient

The Myhill quotient of a regular language is finite.

def Language.myhillCongruenceDA {α : Type} (l : Language α) : Cslib.Automata.DA.FinAcc l.MyhillQuotient α

The deterministic automaton corresponding to the Myhill congruence of a language l.

Equations

• l.myhillCongruenceDA = { toDA := Language.RightCongruence.toDA, accept := (fun (x : List α) => ⟦x⟧) '' l }

theorem Language.myhillCongruenceDA_language_eq {α : Type} (l : Language α) : Cslib.Automata.Acceptor.language l.myhillCongruenceDA = l

The deterministic automaton corresponding to the Myhill congruence of a language l accepts the same language l.

theorem Language.IsRegular.iff_finite_myhillQuotient {α : Type} (l : Language α) : l.IsRegular ↔ Finite l.MyhillQuotient

A language is regular if and only if its Myhill quotient is finite.