Syntactic monoid

DefinitionSyntactic equivalence#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). Two words \(x, y \in \Sigma^*\) are syntactically equivalent for \(L\) when, for all words \(u, v \in \Sigma^*\), \(uxv \in L\) if and only if \(uyv \in L\).

def syntacticRel (L : Language Symbol) (x y : FreeMonoid Symbol) : Prop :=
  ∀ u v, FreeMonoid.toList (u * x * v) ∈ L ↔ FreeMonoid.toList (u * y * v) ∈ L
Used by 17
Used bySyntactic equivalence pulls back along an alphabet map · Syntactic equivalence pulls back along a word morphism · Syntactic equivalence via context quotients · Equal syntactic classes give equal Nerode classes · Action of the syntactic monoid on states · Image of the syntactic action · Syntactic congruence · Syntactic congruence as a kernel · Syntactic equivalence is compatible with concatenation · Syntactic equivalence via transition actions · Syntactically equivalent words agree on membership · Syntactic equivalence refines Nerode equivalence · Words with equal recognizer images are syntactically equivalent · Words with the same transition action are syntactically equivalent · Syntactic equivalence is stable under left multiplication · Syntactic equivalence is stable under right multiplication · Syntactically equivalent words act identically

TheoremSyntactic equivalence is stable under left multiplication#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). If two words \(x, y \in \Sigma^*\) are syntactically equivalent for \(L\), then for every word \(w \in \Sigma^*\) the words \(wx\) and \(wy\) are syntactically equivalent for \(L\).

theorem syntacticRel_prefix (L : Language Symbol) {x y : FreeMonoid Symbol}
    (h : syntacticRel L x y) (w : FreeMonoid Symbol) : syntacticRel L (w * x) (w * y)
Uses 1 · Used by 1
Statement usesSyntactic equivalence
Used bySyntactic equivalence is compatible with concatenation

TheoremSyntactic equivalence is stable under right multiplication#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). If two words \(x, y \in \Sigma^*\) are syntactically equivalent for \(L\), then for every word \(w \in \Sigma^*\) the words \(xw\) and \(yw\) are syntactically equivalent for \(L\).

theorem syntacticRel_suffix (L : Language Symbol) {x y : FreeMonoid Symbol}
    (h : syntacticRel L x y) (w : FreeMonoid Symbol) : syntacticRel L (x * w) (y * w)
Uses 1 · Used by 1
Statement usesSyntactic equivalence
Used bySyntactic equivalence is compatible with concatenation

TheoremSyntactic equivalence is compatible with concatenation#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\) and let \(w, x, y, z \in \Sigma^*\) be words. If \(w\) and \(x\) are syntactically equivalent for \(L\), and \(y\) and \(z\) are syntactically equivalent for \(L\), then \(wy\) and \(xz\) are syntactically equivalent for \(L\).

theorem syntacticRel_append (L : Language Symbol) {w x y z : FreeMonoid Symbol}
    (h₁ : syntacticRel L w x) (h₂ : syntacticRel L y z) :
    syntacticRel L (w * y) (x * z)
Uses 3 · Used by 1
Statement usesSyntactic equivalence
Proof usesSyntactic equivalence is stable under left multiplication · Syntactic equivalence is stable under right multiplication
Used bySyntactic congruence

DefinitionSyntactic congruence#✓fully proved

For a language \(L\) over an alphabet \(\Sigma\), the syntactic congruence of \(L\) is the monoid congruence on the free monoid \(\Sigma^*\) that relates words \(x\) and \(y\) when, for all words \(u\) and \(v\), \(uxv \in L\) if and only if \(uyv \in L\).

def syntacticCon (L : Language Symbol) : Con (FreeMonoid Symbol) where
  r := syntacticRel L
  iseqv := ⟨syntacticRel_refl L, syntacticRel_symm L, syntacticRel_trans L⟩
  mul' := syntacticRel_append L
Uses 2 · Used by 36
Statement usesSyntactic equivalence · Syntactic equivalence is compatible with concatenation
Used byAlphabet preimage morphism · The alphabet preimage morphism refines the preimage's syntactic congruence · Division map for the syntactic monoid of an alphabet preimage · Alphabet preimages preserve finiteness of the syntactic monoid · Inverse images under word morphisms preserve finiteness of the syntactic monoid · The alphabet preimage morphism recognizes the alphabet preimage · Division map for the syntactic monoid of an inverse image · Recognizing morphism of an inverse image · Size bound for the syntactic monoid of a context quotient · The canonical map to the syntactic monoid of a context quotient · Context quotients preserve finiteness of the syntactic monoid · Left quotients preserve finiteness of the syntactic monoid · Right quotients preserve finiteness of the syntactic monoid · The canonical map to the syntactic monoid of a left quotient · The canonical map to the syntactic monoid of a right quotient · Finite recognizers give finite syntactic monoids · The syntactic morphism recognizes the language · Equal syntactic classes give equal Nerode classes · Map from a recognizer's image to the syntactic monoid · The image of a recognizer maps onto the syntactic monoid · Recognizer kernels refine the syntactic congruence · Canonical map from a recognizer's kernel quotient to the syntactic monoid · The kernel quotient of a recognizer maps onto the syntactic monoid · The syntactic morphism recognizes its language · Accepting set of the syntactic monoid · Action of the syntactic monoid on states · Image of the syntactic action · Syntactic congruence as a kernel · The syntactic DFA · The syntactic DFA accepts its language · The syntactic DFA is accessible · Runs of the syntactic DFA · Syntactic monoid · Syntactic morphism · The syntactic monoid is no larger than the transition monoid · The transition monoid maps to the syntactic monoid

AbbreviationSyntactic monoid#✓fully proved

For a language \(L\) over an alphabet \(\Sigma\), the syntactic monoid of \(L\) is the quotient of the free monoid \(\Sigma^*\) of words by the syntactic congruence of \(L\), which relates words \(x\) and \(y\) when \(uxv \in L \iff uyv \in L\) for all words \(u\) and \(v\).

abbrev SyntacticMonoid (L : Language Symbol) := (syntacticCon L).Quotient
Uses 1 · Used by 44
Statement usesSyntactic congruence
Used byRegular languages are closed under alphabet preimages · Alphabet preimage morphism · The alphabet preimage morphism refines the preimage's syntactic congruence · Division map for the syntactic monoid of an alphabet preimage · Alphabet preimages preserve finiteness of the syntactic monoid · Finiteness of the syntactic monoid is invariant under renaming letters · Inverse images under word morphisms preserve finiteness of the syntactic monoid · The alphabet preimage morphism recognizes the alphabet preimage · Regular languages are closed under inverse word morphisms · Division map for the syntactic monoid of an inverse image · Recognizing morphism of an inverse image · Size bound for the syntactic monoid of a context quotient · Regular languages are closed under context quotients · The canonical map to the syntactic monoid of a context quotient · Context quotients preserve finiteness of the syntactic monoid · Left quotients preserve finiteness of the syntactic monoid · Right quotients preserve finiteness of the syntactic monoid · The canonical map to the syntactic monoid of a left quotient · Regular languages are closed under right quotients by fixed words · The canonical map to the syntactic monoid of a right quotient · The syntactic DFA of a language with finite syntactic monoid · Languages of finite automata have finite syntactic monoids · Finite recognizers give finite syntactic monoids · Finite syntactic monoid implies regularity · The syntactic morphism recognizes the language · Equal syntactic classes give equal Nerode classes · Map from a recognizer's image to the syntactic monoid · The image of a recognizer maps onto the syntactic monoid · Canonical map from a recognizer's kernel quotient to the syntactic monoid · The kernel quotient of a recognizer maps onto the syntactic monoid · The syntactic morphism recognizes its language · Accepting set of the syntactic monoid · Action of the syntactic monoid on states · Image of the syntactic action · The syntactic DFA · The syntactic DFA accepts its language · The syntactic DFA is accessible · Runs of the syntactic DFA · Syntactic morphism · Endofunction bound for the syntactic monoid · The syntactic monoid is no larger than the transition monoid · Regular languages have finite syntactic monoids · Regular languages are those with finite syntactic monoid · The transition monoid maps to the syntactic monoid

DefinitionSyntactic morphism#✓fully proved

For a language \(L\) over an alphabet \(\Sigma\), the syntactic morphism of \(L\) is the monoid homomorphism from the free monoid \(\Sigma^*\) of words to the syntactic monoid of \(L\) that sends each word to its class under the syntactic congruence of \(L\).

def syntacticMorphism (L : Language Symbol) : FreeMonoid Symbol →* SyntacticMonoid L :=
  Con.mk' (syntacticCon L)
Uses 2 · Used by 22
Statement usesSyntactic monoid · Syntactic congruence
Used byAlphabet preimage morphism · Inverse images under word morphisms preserve finiteness of the syntactic monoid · The alphabet preimage morphism recognizes the alphabet preimage · Division map for the syntactic monoid of an inverse image · Recognizing morphism of an inverse image · Size bound for the syntactic monoid of a context quotient · The canonical map to the syntactic monoid of a context quotient · Context quotients preserve finiteness of the syntactic monoid · Left quotients preserve finiteness of the syntactic monoid · Right quotients preserve finiteness of the syntactic monoid · The canonical map to the syntactic monoid of a left quotient · The canonical map to the syntactic monoid of a right quotient · The syntactic morphism recognizes the language · Equal syntactic classes give equal Nerode classes · The image of a recognizer maps onto the syntactic monoid · The kernel quotient of a recognizer maps onto the syntactic monoid · The syntactic morphism recognizes its language · Image of the syntactic action · The syntactic DFA · The syntactic DFA accepts its language · The syntactic DFA is accessible · Runs of the syntactic DFA

TheoremSyntactically equivalent words agree on membership#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). If two words \(x, y \in \Sigma^*\) are syntactically equivalent for \(L\), then \(x \in L\) if and only if \(y \in L\).

theorem syntacticRel_mem_iff (L : Language Symbol) {x y : FreeMonoid Symbol}
    (h : syntacticRel L x y) : FreeMonoid.toList x ∈ L ↔ FreeMonoid.toList y ∈ L
Uses 1 · Used by 1
Statement usesSyntactic equivalence
Used byAccepting set of the syntactic monoid

DefinitionAccepting set of the syntactic monoid#✓fully proved

For a language \(L\), the accepting set of the syntactic monoid of \(L\) is the set of syntactic classes of words of \(L\): a class belongs to it when its representatives lie in \(L\), which does not depend on the representative chosen.

def syntacticAccept (L : Language Symbol) : Set (SyntacticMonoid L) :=
  {q | Con.liftOn q (fun x ↦ FreeMonoid.toList x ∈ L)
    (fun _ _ h ↦ propext (syntacticRel_mem_iff L h))}
Uses 3 · Used by 17
Statement usesSyntactic monoid · Syntactic congruence · Syntactically equivalent words agree on membership
Used byThe alphabet preimage morphism refines the preimage's syntactic congruence · Division map for the syntactic monoid of an alphabet preimage · Alphabet preimages preserve finiteness of the syntactic monoid · Inverse images under word morphisms preserve finiteness of the syntactic monoid · The alphabet preimage morphism recognizes the alphabet preimage · Division map for the syntactic monoid of an inverse image · Size bound for the syntactic monoid of a context quotient · The canonical map to the syntactic monoid of a context quotient · Context quotients preserve finiteness of the syntactic monoid · Left quotients preserve finiteness of the syntactic monoid · Right quotients preserve finiteness of the syntactic monoid · The canonical map to the syntactic monoid of a left quotient · The canonical map to the syntactic monoid of a right quotient · The syntactic morphism recognizes the language · The syntactic morphism recognizes its language · The syntactic DFA · The syntactic DFA accepts its language

TheoremThe syntactic morphism recognizes the language#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). For every word \(x \in \Sigma^*\), \(x \in L\) if and only if the image of \(x\) under the syntactic morphism of \(L\) lies in the accepting set of the syntactic monoid of \(L\), the set of syntactic classes of words of \(L\).

theorem mem_iff_syntacticMorphism_mem (L : Language Symbol) (x : FreeMonoid Symbol) :
    FreeMonoid.toList x ∈ L ↔ syntacticMorphism L x ∈ syntacticAccept L
Uses 4
Statement usesSyntactic monoid · Accepting set of the syntactic monoid · Syntactic congruence · Syntactic morphism

TheoremSyntactic equivalence refines Nerode equivalence#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). If two words \(x, y \in \Sigma^*\) are syntactically equivalent for \(L\), then they are Nerode equivalent for \(L\): the sets \(\{z : xz \in L\}\) and \(\{z : yz \in L\}\) are equal.

theorem syntacticRel_nerodeRel (L : Language Symbol) {x y : FreeMonoid Symbol}
    (h : syntacticRel L x y) : nerodeRel L (FreeMonoid.toList x) (FreeMonoid.toList y)
Uses 3 · Used by 1
Statement usesNerode equivalence · Syntactic equivalence
Proof usesContinuation characterization of Nerode equivalence
Used byEqual syntactic classes give equal Nerode classes

TheoremEqual syntactic classes give equal Nerode classes#✓fully proved

Let \(L\) be a language. For all words \(x\) and \(y\), if the syntactic morphism of \(L\) sends \(x\) and \(y\) to the same element of the syntactic monoid of \(L\), then \(x\) and \(y\) have the same Nerode class with respect to \(L\).

theorem nerodeClass_eq_of_syntacticMorphism_eq (L : Language Symbol) {x y : FreeMonoid Symbol}
    (h : syntacticMorphism L x = syntacticMorphism L y) :
    nerodeClass L (FreeMonoid.toList x) = nerodeClass L (FreeMonoid.toList y)
Uses 9
Statement usesNerode classes · Syntactic monoid · Nerode class of a word · Syntactic congruence · Syntactic morphism
Proof usesNerode equivalence · The Nerode setoid · Syntactic equivalence · Syntactic equivalence refines Nerode equivalence

DefinitionTransition action of a word#✓fully proved

For a DFA \(M\) and a word \(x\), the transition action of \(x\) is the map sending each state \(q\) of \(M\) to the state that \(M\) reaches by reading \(x\) starting from \(q\).

def transitionAction (M : DFA Symbol State) (x : FreeMonoid Symbol) : State → State :=
  fun q ↦ M.evalFrom q (FreeMonoid.toList x)
Used by 7
Used byAction of the syntactic monoid on states · Image of the syntactic action · Syntactic congruence as a kernel · Syntactic equivalence via transition actions · Words with the same transition action are syntactically equivalent · Syntactically equivalent words act identically · Transition transformation of a word

TheoremWords with the same transition action are syntactically equivalent#✓fully proved

Let \(M\) be a DFA over an alphabet \(\Sigma\) and let \(L\) be the language accepted by \(M\). If two words \(x, y \in \Sigma^*\) have the same transition action on \(M\), that is, for every state \(q\), running \(M\) from \(q\) on \(x\) ends in the same state as running \(M\) from \(q\) on \(y\), then \(x\) and \(y\) are syntactically equivalent for \(L\).

theorem syntacticRel_of_transitionAction_eq (M : DFA Symbol State) {x y : FreeMonoid Symbol}
    (h : transitionAction M x = transitionAction M y) : syntacticRel M.accepts x y
Uses 2 · Used by 1
Statement usesSyntactic equivalence · Transition action of a word
Used bySyntactic equivalence via transition actions

TheoremSyntactically equivalent words act identically#✓fully proved

Let \(M\) be a DFA that is accessible (every state is reachable from the start state) and state-separated (two states with the same continuation language are equal). If two words \(x\) and \(y\) are syntactically equivalent for the language accepted by \(M\), then \(x\) and \(y\) have the same transition action on \(M\): for every state \(q\), reading \(x\) from \(q\) and reading \(y\) from \(q\) lead to the same state.

theorem transitionAction_eq_of_syntacticRel (M : DFA Symbol State) (hacc : Accessible M)
    (hsep : StateSeparated M) {x y : FreeMonoid Symbol} (h : syntacticRel M.accepts x y) :
    transitionAction M x = transitionAction M y
Uses 6 · Used by 1
Statement usesAccessible DFA · State-separated DFA · Syntactic equivalence · Transition action of a word
Proof usesReachable state of a DFA · Equivalent states of a DFA
Used bySyntactic equivalence via transition actions

TheoremSyntactic equivalence via transition actions#✓fully proved

Let \(M\) be a DFA over an alphabet \(\Sigma\) that is accessible (every state is reached from the start state by some word) and state-separated (distinct states have distinct continuation languages), and let \(L\) be the language accepted by \(M\). Then two words \(x, y \in \Sigma^*\) are syntactically equivalent for \(L\) if and only if they have the same transition action on \(M\): for every state \(q\), running \(M\) from \(q\) on \(x\) ends in the same state as running \(M\) from \(q\) on \(y\).

theorem syntacticRel_iff_transitionAction_eq (M : DFA Symbol State) (hacc : Accessible M)
    (hsep : StateSeparated M) (x y : FreeMonoid Symbol) :
    syntacticRel M.accepts x y ↔ transitionAction M x = transitionAction M y
Uses 6 · Used by 3
Statement usesAccessible DFA · State-separated DFA · Syntactic equivalence · Transition action of a word
Proof usesWords with the same transition action are syntactically equivalent · Syntactically equivalent words act identically
Used byAction of the syntactic monoid on states · Image of the syntactic action · Syntactic congruence as a kernel

AbbreviationState transformation monoid#✓fully proved

For a type \(Q\) of states, the state transformation monoid of \(Q\) consists of all functions \(Q \to Q\), multiplied by composition in the opposite order: the product \(fg\) first applies \(f\) and then \(g\), so \((fg)(q) = g(f(q))\), and the unit is the identity function.

abbrev StateTransformation (State : Type v) := (Function.End State)ᵐᵒᵖ
Used by 18
Used byLanguages of finite automata have finite syntactic monoids · The transition morphism of a DFA recognizes its language · State transformations as functions · Action of the syntactic monoid on states · Image of the syntactic action · Syntactic congruence as a kernel · Transition monoid element of a word · Transition monoid of a DFA · Transition morphism of a DFA · Transition transformation of a word · Endofunction bound for the syntactic monoid · The syntactic monoid is no larger than the transition monoid · Finitely many state transformations · Transition monoids of finite automata are finite · The transition monoid recognizes the accepted language · The transition morphism recognizes through accepting transformations · Accepting transformations of a DFA · The transition monoid maps to the syntactic monoid

DefinitionState transformations as functions#✓fully proved

For a type \(Q\) of states, the bijection from the state transformations of \(Q\) to the functions \(Q \to Q\) that sends each transformation to its underlying function; it forgets the multiplication of state transformations.

def stateTransformationEquiv : StateTransformation State ≃ (State → State) where
  toFun f := MulOpposite.unop f
  invFun f := MulOpposite.op f
  left_inv := MulOpposite.op_unop
  right_inv := MulOpposite.unop_op
Uses 1 · Used by 3
Statement usesState transformation monoid
Used byLanguages of finite automata have finite syntactic monoids · Endofunction bound for the syntactic monoid · Finitely many state transformations

DefinitionTransition transformation of a word#✓fully proved

For a DFA \(M\) and a word \(x\), the transition transformation of \(x\) is the transition action of \(x\), the map sending each state \(q\) to the state that \(M\) reaches by reading \(x\) from \(q\), regarded as an element of the monoid of state transformations of \(M\) (multiplied in reading order: \(fg\) applies \(f\) first, then \(g\)).

def transitionTransformation (M : DFA Symbol State) (x : FreeMonoid Symbol) :
    StateTransformation State :=
  MulOpposite.op (transitionAction M x)
Uses 2 · Used by 1
Statement usesState transformation monoid · Transition action of a word
Used byTransition morphism of a DFA

DefinitionTransition morphism of a DFA#✓fully proved

For a DFA \(M\), the transition morphism is the monoid homomorphism from the free monoid of words to the state transformations of \(M\) that sends each word \(x\) to its transition action, the map taking each state \(q\) to the state that \(M\) reaches by reading \(x\) from \(q\). State transformations are multiplied in reading order, so the product \(fg\) applies \(f\) first and then \(g\); with this order, the word \(xy\) is sent to the product of the images of \(x\) and \(y\).

def transitionMorphism (M : DFA Symbol State) :
    FreeMonoid Symbol →* StateTransformation State where
  toFun := transitionTransformation M
  map_one' := transitionTransformation_one M
  map_mul' := transitionTransformation_mul M
Uses 2 · Used by 11
Statement usesState transformation monoid · Transition transformation of a word
Used byLanguages of finite automata have finite syntactic monoids · The transition morphism of a DFA recognizes its language · Action of the syntactic monoid on states · Image of the syntactic action · Syntactic congruence as a kernel · Transition monoid element of a word · Transition monoid of a DFA · The syntactic monoid is no larger than the transition monoid · The transition monoid recognizes the accepted language · The transition morphism recognizes through accepting transformations · The transition monoid maps to the syntactic monoid

DefinitionTransition monoid of a DFA#✓fully proved

The transition monoid of a DFA \(M\) is the image of the transition morphism of \(M\): the submonoid of state transformations of \(M\) consisting of the transition actions of all words, where a word \(x\) acts by sending each state \(q\) to the state that \(M\) reaches by reading \(x\) from \(q\). State transformations are multiplied in reading order, so the product \(fg\) applies \(f\) first and then \(g\).

def TransitionMonoid (M : DFA Symbol State) := MonoidHom.mrange (transitionMorphism M)
Uses 2 · Used by 7
Statement usesState transformation monoid · Transition morphism of a DFA
Used byImage of the syntactic action · Transition monoid element of a word · Endofunction bound for the syntactic monoid · The syntactic monoid is no larger than the transition monoid · Transition monoids of finite automata are finite · The transition monoid recognizes the accepted language · The transition monoid maps to the syntactic monoid

DefinitionTransition monoid element of a word#✓fully proved

Let \(M\) be a DFA over an alphabet \(\Sigma\). Each word \(x \in \Sigma^*\) determines the element of the transition monoid of \(M\) given by the state transformation that sends each state \(q\) to the state \(M\) reaches from \(q\) after reading \(x\).

def toTransitionMonoid (M : DFA Symbol State) (x : FreeMonoid Symbol) : TransitionMonoid M :=
  ⟨transitionMorphism M x, ⟨x, rfl⟩⟩
Uses 3
Statement usesState transformation monoid · Transition monoid of a DFA · Transition morphism of a DFA

TheoremSyntactic congruence as a kernel#✓fully proved

Let \(M\) be an accessible, state-separated DFA and let \(L\) be the language \(M\) accepts. The syntactic congruence of \(L\) equals the kernel of the transition morphism of \(M\): two words are syntactically equivalent for \(L\) if and only if they induce the same transformation of the states of \(M\).

theorem syntacticCon_eq_transitionMorphism_ker (M : DFA Symbol State) (hacc : Accessible M)
    (hsep : StateSeparated M) : syntacticCon M.accepts = Con.ker (transitionMorphism M)
Uses 8
Statement usesAccessible DFA · State-separated DFA · State transformation monoid · Syntactic congruence · Transition morphism of a DFA
Proof usesSyntactic equivalence · Syntactic equivalence via transition actions · Transition action of a word

DefinitionAction of the syntactic monoid on states#✓fully proved

Let \(M\) be an accessible, state-separated DFA with state type \(Q\), and let \(L\) be the language \(M\) accepts. This is the monoid homomorphism from the syntactic monoid of \(L\) to the state transformation monoid of \(Q\) that sends the syntactic class of each word \(x\) to the map taking each state \(q\) to the state \(M\) reaches from \(q\) by reading \(x\). It is well defined because syntactically equivalent words act identically on the states of such a DFA.

def syntacticActionHom (M : DFA Symbol State) (hacc : Accessible M) (hsep : StateSeparated M) :
    SyntacticMonoid M.accepts →* StateTransformation State :=
  (syntacticCon M.accepts).lift (transitionMorphism M) <| by
    intro x y hxy
    exact (transitionMorphism_eq_iff M x y).mpr <|
      (syntacticRel_iff_transitionAction_eq M hacc hsep x y).mp hxy
Uses 9 · Used by 1
Statement usesAccessible DFA · State-separated DFA · State transformation monoid · Syntactic monoid · Syntactic congruence · Syntactic equivalence · Syntactic equivalence via transition actions · Transition action of a word · Transition morphism of a DFA
Used byImage of the syntactic action

TheoremImage of the syntactic action#✓fully proved

Let \(M\) be an accessible, state-separated DFA and let \(L\) be the language \(M\) accepts. The image of the action of the syntactic monoid of \(L\) on the states of \(M\), the monoid homomorphism sending the syntactic class of each word \(x\) to the state transformation induced by reading \(x\), is exactly the transition monoid of \(M\).

theorem syntacticActionHom_range (M : DFA Symbol State) (hacc : Accessible M)
    (hsep : StateSeparated M) :
    MonoidHom.mrange (syntacticActionHom M hacc hsep) = TransitionMonoid M
Uses 12
Statement usesAccessible DFA · State-separated DFA · State transformation monoid · Syntactic monoid · Transition monoid of a DFA · Action of the syntactic monoid on states · Syntactic congruence
Proof usesSyntactic morphism · Syntactic equivalence · Syntactic equivalence via transition actions · Transition action of a word · Transition morphism of a DFA

DefinitionRecognition of a language by a monoid morphism#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\), let \(\varphi : \Sigma^* \to M\) be a monoid morphism from the free monoid on \(\Sigma\) into a monoid \(M\), and let \(A \subseteq M\). Then \(\varphi\) recognizes \(L\) through \(A\) when, for every word \(w \in \Sigma^*\), \(w \in L\) if and only if \(\varphi(w) \in A\).

def Recognizes [Monoid Carrier] (L : Language Symbol) (morphism : FreeMonoid Symbol →* Carrier)
    (accept : Set Carrier) : Prop :=
  ∀ x, FreeMonoid.toList x ∈ L ↔ morphism x ∈ accept
Used by 23
Used byInverse images under word morphisms preserve finiteness of the syntactic monoid · The alphabet preimage morphism recognizes the alphabet preimage · Division map for the syntactic monoid of an inverse image · Recognizers recognize context quotients · The canonical map to the syntactic monoid of a context quotient · Recognizers recognize left quotients · The canonical map to the syntactic monoid of a left quotient · Recognizers recognize right quotients · The canonical map to the syntactic monoid of a right quotient · Recognition pulls back along a factorization · Changing the accepting set off the image of a recognizer · Finite recognizers give finite syntactic monoids · Map from a recognizer's image to the syntactic monoid · The image of a recognizer maps onto the syntactic monoid · Recognizer kernels refine the syntactic congruence · Canonical map from a recognizer's kernel quotient to the syntactic monoid · The kernel quotient of a recognizer maps onto the syntactic monoid · Recognition as an inverse image · The syntactic morphism recognizes its language · The transition morphism of a DFA recognizes its language · Words with equal recognizer images are syntactically equivalent · The transition monoid recognizes the accepted language · The transition morphism recognizes through accepting transformations

TheoremThe syntactic morphism recognizes its language#✓fully proved

For every language \(L\) over an alphabet \(\Sigma\), the syntactic morphism of \(L\), from the free monoid \(\Sigma^*\) to the syntactic monoid of \(L\), recognizes \(L\) through the accepting subset of the syntactic monoid, namely the set of syntactic classes of words in \(L\).

theorem recognizes_syntacticMorphism (L : Language Symbol) :
    Recognizes L (syntacticMorphism L) (syntacticAccept L)
Uses 5 · Used by 7
Statement usesRecognition of a language by a monoid morphism · Syntactic monoid · Accepting set of the syntactic monoid · Syntactic congruence · Syntactic morphism
Used bySize bound for the syntactic monoid of a context quotient · The canonical map to the syntactic monoid of a context quotient · Context quotients preserve finiteness of the syntactic monoid · Left quotients preserve finiteness of the syntactic monoid · Right quotients preserve finiteness of the syntactic monoid · The canonical map to the syntactic monoid of a left quotient · The canonical map to the syntactic monoid of a right quotient

TheoremRecognition pulls back along a factorization#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\) and let \(\varphi : \Sigma^* \to C\) be a monoid morphism from the free monoid \(\Sigma^*\) that recognizes \(L\) through a subset \(A \subseteq C\). If \(\varphi = f \circ \psi\) for monoid morphisms \(\psi : \Sigma^* \to T\) and \(f : T \to C\), then \(\psi\) recognizes \(L\) through the preimage \(f^{-1}(A)\).

theorem Recognizes.comp [Monoid Carrier] {Target : Type*} [Monoid Target]
    {L : Language Symbol} {morphism : FreeMonoid Symbol →* Carrier} {accept : Set Carrier}
    (h : Recognizes L morphism accept) (factor : Target →* Carrier)
    (source : FreeMonoid Symbol →* Target) (hfactor : factor.comp source = morphism) :
    Recognizes L source (factor ⁻¹' accept)
Uses 1
Statement usesRecognition of a language by a monoid morphism

TheoremWords with equal recognizer images are syntactically equivalent#✓fully proved

Let \(\varphi : \Sigma^* \to M\) be a monoid morphism from the free monoid on an alphabet \(\Sigma\) into a monoid \(M\) that recognizes a language \(L\) over \(\Sigma\) through a set \(A \subseteq M\). If two words \(x, y \in \Sigma^*\) satisfy \(\varphi(x) = \varphi(y)\), then \(x\) and \(y\) are syntactically equivalent for \(L\): for all words \(u, v \in \Sigma^*\), \(uxv \in L\) if and only if \(uyv \in L\).

theorem syntacticRel_of_recognizer_eq [Monoid Carrier] {L : Language Symbol}
    {morphism : FreeMonoid Symbol →* Carrier} {accept : Set Carrier}
    (hrec : Recognizes L morphism accept) {x y : FreeMonoid Symbol}
    (hxy : morphism x = morphism y) : syntacticRel L x y
Uses 2 · Used by 1
Statement usesRecognition of a language by a monoid morphism · Syntactic equivalence
Used byRecognizer kernels refine the syntactic congruence

TheoremRecognizer kernels refine the syntactic congruence#✓fully proved

If a monoid morphism \(\varphi\) from the free monoid \(\Sigma^*\) recognizes a language \(L\) over \(\Sigma\) through a subset \(A\) of its codomain, then the kernel congruence of \(\varphi\) is contained in the syntactic congruence of \(L\): any words \(x, y\) with \(\varphi(x) = \varphi(y)\) are syntactically equivalent for \(L\).

theorem recognizer_ker_le_syntacticCon [Monoid Carrier] {L : Language Symbol}
    {morphism : FreeMonoid Symbol →* Carrier} {accept : Set Carrier}
    (hrec : Recognizes L morphism accept) : Con.ker morphism ≤ syntacticCon L
Uses 3 · Used by 2
Statement usesRecognition of a language by a monoid morphism · Syntactic congruence
Proof usesWords with equal recognizer images are syntactically equivalent
Used byThe alphabet preimage morphism refines the preimage's syntactic congruence · Canonical map from a recognizer's kernel quotient to the syntactic monoid

DefinitionCanonical map from a recognizer's kernel quotient to the syntactic monoid#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\), let \(\varphi : \Sigma^* \to M\) be a monoid morphism from the free monoid on \(\Sigma\) into a monoid \(M\), and let \(A \subseteq M\) be such that \(\varphi\) recognizes \(L\) through \(A\). Since the kernel congruence of \(\varphi\) (words \(x, y\) with \(\varphi(x) = \varphi(y)\)) is contained in the syntactic congruence of \(L\), there is a monoid morphism from the quotient of \(\Sigma^*\) by the kernel of \(\varphi\) to the syntactic monoid of \(L\) sending the class of each word \(w\) to the syntactic class of \(w\).

This is the algebraic minimality map before identifying the kernel quotient with the image of the recognizer.

def recognizerQuotientToSyntactic [Monoid Carrier] {L : Language Symbol}
    (morphism : FreeMonoid Symbol →* Carrier) (accept : Set Carrier)
    (hrec : Recognizes L morphism accept) :
    (Con.ker morphism).Quotient →* SyntacticMonoid L :=
  Con.map (Con.ker morphism) (syntacticCon L) (recognizer_ker_le_syntacticCon hrec)
Uses 4 · Used by 3
Statement usesRecognition of a language by a monoid morphism · Syntactic monoid · Recognizer kernels refine the syntactic congruence · Syntactic congruence
Used byMap from a recognizer's image to the syntactic monoid · The image of a recognizer maps onto the syntactic monoid · The kernel quotient of a recognizer maps onto the syntactic monoid

TheoremThe kernel quotient of a recognizer maps onto the syntactic monoid#✓fully proved

If a monoid morphism \(\varphi\) from the free monoid \(\Sigma^*\) recognizes a language \(L\) over \(\Sigma\) through a subset \(A\) of its codomain, then the canonical monoid morphism from the quotient of \(\Sigma^*\) by the kernel congruence of \(\varphi\) to the syntactic monoid of \(L\), which sends the class of a word \(x\) to its syntactic class, is surjective.

theorem recognizerQuotientToSyntactic_surjective [Monoid Carrier] {L : Language Symbol}
    (morphism : FreeMonoid Symbol →* Carrier) (accept : Set Carrier)
    (hrec : Recognizes L morphism accept) :
    Function.Surjective (recognizerQuotientToSyntactic morphism accept hrec)
Uses 5
Statement usesRecognition of a language by a monoid morphism · Syntactic monoid · Canonical map from a recognizer's kernel quotient to the syntactic monoid · Syntactic congruence
Proof usesSyntactic morphism

DefinitionMap from a recognizer's image to the syntactic monoid#✓fully proved

Let \(\varphi : \Sigma^* \to M\) be a monoid morphism from the free monoid \(\Sigma^*\) that recognizes a language \(L\) over \(\Sigma\) through a subset \(A \subseteq M\). This is the monoid morphism from the image \(\varphi(\Sigma^*)\) to the syntactic monoid of \(L\) that sends \(\varphi(x)\) to the syntactic class of \(x\) for every word \(x\). It is well defined because words with the same image under \(\varphi\) are syntactically equivalent for \(L\).

noncomputable def recognizerImageToSyntactic [Monoid Carrier] {L : Language Symbol}
    (morphism : FreeMonoid Symbol →* Carrier) (accept : Set Carrier)
    (hrec : Recognizes L morphism accept) :
    MonoidHom.mrange morphism →* SyntacticMonoid L :=
  (recognizerQuotientToSyntactic morphism accept hrec).comp
    (Con.quotientKerEquivRange morphism).symm.toMonoidHom
Uses 4 · Used by 8
Statement usesRecognition of a language by a monoid morphism · Syntactic monoid · Canonical map from a recognizer's kernel quotient to the syntactic monoid · Syntactic congruence
Used byDivision map for the syntactic monoid of an alphabet preimage · Division map for the syntactic monoid of an inverse image · The canonical map to the syntactic monoid of a context quotient · The canonical map to the syntactic monoid of a left quotient · The canonical map to the syntactic monoid of a right quotient · Finite recognizers give finite syntactic monoids · The image of a recognizer maps onto the syntactic monoid · The transition monoid maps to the syntactic monoid

TheoremThe image of a recognizer maps onto the syntactic monoid#✓fully proved

Let \(\varphi : \Sigma^* \to M\) be a monoid morphism from the free monoid \(\Sigma^*\) that recognizes a language \(L\) over \(\Sigma\) through a subset \(A \subseteq M\). Then the canonical monoid morphism from the image \(\varphi(\Sigma^*)\) to the syntactic monoid of \(L\), which sends \(\varphi(x)\) to the syntactic class of \(x\), is surjective.

theorem recognizerImageToSyntactic_surjective [Monoid Carrier] {L : Language Symbol}
    (morphism : FreeMonoid Symbol →* Carrier) (accept : Set Carrier)
    (hrec : Recognizes L morphism accept) :
    Function.Surjective (recognizerImageToSyntactic morphism accept hrec)
Uses 6 · Used by 3
Statement usesRecognition of a language by a monoid morphism · Syntactic monoid · Map from a recognizer's image to the syntactic monoid · Syntactic congruence
Proof usesCanonical map from a recognizer's kernel quotient to the syntactic monoid · Syntactic morphism
Used bySize bound for the syntactic monoid of a context quotient · Finite recognizers give finite syntactic monoids · The syntactic monoid is no larger than the transition monoid

TheoremFinite recognizers give finite syntactic monoids#✓fully proved

If a monoid morphism from the free monoid \(\Sigma^*\) to a finite monoid \(M\) recognizes a language \(L\) over \(\Sigma\) through some subset of \(M\), then the syntactic monoid of \(L\) is finite.

theorem finite_syntacticMonoid_of_recognizer [Monoid Carrier] [Finite Carrier]
    {L : Language Symbol} (morphism : FreeMonoid Symbol →* Carrier) (accept : Set Carrier)
    (hrec : Recognizes L morphism accept) : Finite (SyntacticMonoid L)
Uses 5 · Used by 6
Statement usesRecognition of a language by a monoid morphism · Syntactic monoid
Proof usesMap from a recognizer's image to the syntactic monoid · The image of a recognizer maps onto the syntactic monoid · Syntactic congruence
Used byAlphabet preimages preserve finiteness of the syntactic monoid · Inverse images under word morphisms preserve finiteness of the syntactic monoid · Context quotients preserve finiteness of the syntactic monoid · Left quotients preserve finiteness of the syntactic monoid · Right quotients preserve finiteness of the syntactic monoid · Languages of finite automata have finite syntactic monoids

TheoremRecognition as an inverse image#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\), let \(\varphi : \Sigma^* \to M\) be a monoid morphism from the free monoid on \(\Sigma\) into a monoid \(M\), and let \(A \subseteq M\). Then \(\varphi\) recognizes \(L\) through \(A\) if and only if the set of words of \(\Sigma^*\) that belong to \(L\) equals \(\varphi^{-1}(A)\).

theorem recognizes_iff_preimage [Monoid Carrier] (L : Language Symbol)
    (morphism : FreeMonoid Symbol →* Carrier) (accept : Set Carrier) :
    Recognizes L morphism accept ↔
      {x | FreeMonoid.toList x ∈ L} = morphism ⁻¹' accept
Uses 1
Statement usesRecognition of a language by a monoid morphism

TheoremChanging the accepting set off the image of a recognizer#✓fully proved

Let \(\varphi : \Sigma^* \to M\) be a monoid morphism from the free monoid \(\Sigma^*\) that recognizes a language \(L\) over \(\Sigma\) through a subset \(A_1 \subseteq M\). If \(A_2 \subseteq M\) satisfies \(\varphi(x) \in A_1 \iff \varphi(x) \in A_2\) for every word \(x\), then \(\varphi\) also recognizes \(L\) through \(A_2\).

theorem Recognizes.congr_accept [Monoid Carrier] {L : Language Symbol}
    {morphism : FreeMonoid Symbol →* Carrier} {accept₁ accept₂ : Set Carrier}
    (hrec : Recognizes L morphism accept₁)
    (haccept : ∀ x, morphism x ∈ accept₁ ↔ morphism x ∈ accept₂) :
    Recognizes L morphism accept₂
Uses 1
Statement usesRecognition of a language by a monoid morphism

DefinitionThe syntactic DFA#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). The syntactic DFA of \(L\) has the syntactic monoid of \(L\) as its set of states, the identity \(1\) as start state, and the syntactic classes of the words of \(L\) as accepting states; from a state \(q\), reading a letter \(a \in \Sigma\) leads to \(q \cdot [a]\), where \([a]\) is the syntactic class of the one-letter word \(a\).

It is the direct automata-theoretic presentation of the canonical syntactic recognizer.

def syntacticDFA (L : Language Symbol) : DFA Symbol (SyntacticMonoid L) where
  step q a := q * syntacticMorphism L (FreeMonoid.of a)
  start := 1
  accept := syntacticAccept L
Uses 4 · Used by 5
Statement usesSyntactic monoid · Accepting set of the syntactic monoid · Syntactic congruence · Syntactic morphism
Used byThe syntactic DFA of a language with finite syntactic monoid · Finite syntactic monoid implies regularity · The syntactic DFA accepts its language · The syntactic DFA is accessible · Runs of the syntactic DFA

TheoremRuns of the syntactic DFA#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). For every state \(q\) of the syntactic DFA of \(L\) (an element of the syntactic monoid of \(L\)) and every word \(x \in \Sigma^*\), the state reached from \(q\) by reading \(x\) is \(q \cdot [x]\), where \([x]\) is the image of \(x\) under the syntactic morphism of \(L\).

theorem syntacticDFA_evalFrom (L : Language Symbol) (q : SyntacticMonoid L)
    (x : List Symbol) :
    (syntacticDFA L).evalFrom q x = q * syntacticMorphism L (FreeMonoid.ofList x)
Uses 4 · Used by 2
Statement usesSyntactic monoid · Syntactic congruence · The syntactic DFA · Syntactic morphism
Used byThe syntactic DFA accepts its language · The syntactic DFA is accessible

TheoremThe syntactic DFA accepts its language#✓fully proved

For every language \(L\), the syntactic DFA of \(L\) accepts exactly \(L\).

theorem syntacticDFA_accepts (L : Language Symbol) : (syntacticDFA L).accepts = L
Uses 6 · Used by 2
Statement usesSyntactic monoid · The syntactic DFA
Proof usesAccepting set of the syntactic monoid · Syntactic congruence · Runs of the syntactic DFA · Syntactic morphism
Used byThe syntactic DFA of a language with finite syntactic monoid · Finite syntactic monoid implies regularity

TheoremThe syntactic DFA is accessible#✓fully proved

For every language \(L\), every state of the syntactic DFA of \(L\) is reachable: some word leads to it from the start state.

theorem syntacticDFA_accessible (L : Language Symbol) : Accessible (syntacticDFA L)
Uses 7
Statement usesAccessible DFA · Syntactic monoid · The syntactic DFA
Proof usesReachable state of a DFA · Syntactic congruence · Runs of the syntactic DFA · Syntactic morphism

TheoremFinite syntactic monoid implies regularity#✓fully proved

Every language whose syntactic monoid is finite is regular.

theorem isRegular_of_finite_syntacticMonoid (L : Language Symbol)
    [Finite (SyntacticMonoid L)] : L.IsRegular
Uses 3 · Used by 1
Statement usesSyntactic monoid
Proof usesThe syntactic DFA · The syntactic DFA accepts its language
Used byRegular languages are those with finite syntactic monoid

TheoremThe syntactic DFA of a language with finite syntactic monoid#✓fully proved

If the syntactic monoid of a language \(L\) is finite, then the syntactic DFA of \(L\) has finitely many states and accepts exactly \(L\).

This gives a specific finite recognizer, the syntactic DFA, rather than merely the existence of some finite DFA.

theorem exists_finite_syntacticDFA (L : Language Symbol) [Finite (SyntacticMonoid L)] :
    ∃ _ : Fintype (SyntacticMonoid L), (syntacticDFA L).accepts = L
Uses 3
Statement usesSyntactic monoid · The syntactic DFA
Proof usesThe syntactic DFA accepts its language

TheoremThe transition morphism of a DFA recognizes its language#✓fully proved

Let \(M\) be a DFA over an alphabet \(\Sigma\) with state set \(Q\), start state \(q_0\) and set of accepting states \(F\). The transition morphism of \(M\), from the free monoid \(\Sigma^*\) to the monoid of state transformations of \(Q\), recognizes the language accepted by \(M\) through the set of transformations \(f\) with \(f(q_0) \in F\).

No accessibility or state-separation hypothesis on \(M\) is needed.

theorem recognizes_transitionMorphism (M : DFA Symbol State) :
    Recognizes M.accepts (transitionMorphism M) {f | f M.start ∈ M.accept}
Uses 3 · Used by 2
Statement usesRecognition of a language by a monoid morphism · State transformation monoid · Transition morphism of a DFA
Used byLanguages of finite automata have finite syntactic monoids · The transition morphism recognizes through accepting transformations

TheoremLanguages of finite automata have finite syntactic monoids#✓fully proved

Every language accepted by a DFA with finitely many states has a finite syntactic monoid.

theorem finite_syntacticMonoid_of_finite_dfa (M : DFA Symbol State)
    [Finite State] : Finite (SyntacticMonoid M.accepts)
Uses 6 · Used by 1
Statement usesSyntactic monoid
Proof usesState transformation monoid · Finite recognizers give finite syntactic monoids · The transition morphism of a DFA recognizes its language · State transformations as functions · Transition morphism of a DFA
Used byRegular languages have finite syntactic monoids
45 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.