Language quotients and syntactic monoids

DefinitionContext quotient#✓fully proved

Let \(L\) be a language over an alphabet \(A\) and let \(u, v\) be words over \(A\). The context quotient of \(L\) by \((u, v)\) is the language \(u^{-1} L v^{-1} = \{x \in A^* \mid uxv \in L\}\) of words that land in \(L\) when placed between \(u\) and \(v\).

def contextQuotient (L : Language Symbol) (left right : List Symbol) : Language Symbol :=
  {x | left ++ x ++ right ∈ L}

Used by 8

Used bySize bound for the syntactic monoid of a context quotient · Recognizers recognize context quotients · Regular languages are closed under context quotients · Composing context quotients · The canonical map to the syntactic monoid of a context quotient · Context quotients preserve finiteness of the syntactic monoid · Syntactic equivalence via context quotients · Non-universality makes the reduction language non-regular

TheoremComposing context quotients#✓fully proved

Let \(L\) be a language over an alphabet \(A\), and for words \(u, v\) over \(A\) write \(u^{-1} L v^{-1} = \{x \mid uxv \in L\}\). Then for all words \(u_1, v_1, u_2, v_2\) over \(A\), \(u_2^{-1} (u_1^{-1} L v_1^{-1}) v_2^{-1} = (u_1 u_2)^{-1} L (v_2 v_1)^{-1}\).

theorem contextQuotient_contextQuotient (L : Language Symbol)
    (outerLeft outerRight innerLeft innerRight : List Symbol) :
    contextQuotient (contextQuotient L outerLeft outerRight) innerLeft innerRight =
      contextQuotient L (outerLeft ++ innerLeft) (innerRight ++ outerRight)

Uses 1

Statement usesContext quotient

DefinitionAccepting set for a context quotient#✓fully proved

Let \(\varphi \colon A^* \to M\) be a monoid morphism from the free monoid on an alphabet \(A\) to a monoid \(M\), let \(P \subseteq M\), and let \(u, v\) be words over \(A\). The accepting set for the context \((u, v)\) is \(\{m \in M \mid \varphi(u)\, m\, \varphi(v) \in P\}\).

def contextAccept [Monoid Carrier] (morphism : FreeMonoid Symbol →* Carrier)
    (accept : Set Carrier) (left right : List Symbol) : Set Carrier :=
  {m | morphism (FreeMonoid.ofList left) * m * morphism (FreeMonoid.ofList right) ∈ accept}

Used by 4

Used bySize bound for the syntactic monoid of a context quotient · Recognizers recognize context quotients · The canonical map to the syntactic monoid of a context quotient · Context quotients preserve finiteness of the syntactic monoid

TheoremRecognizers recognize context quotients#✓fully proved

Let \(\varphi \colon A^* \to M\) be a monoid morphism from the free monoid on an alphabet \(A\) to a monoid \(M\) that recognizes a language \(L\) over \(A\) through \(P \subseteq M\), that is, a word \(x\) lies in \(L\) exactly when \(\varphi(x) \in P\). Then for all words \(u, v\) over \(A\), \(\varphi\) recognizes the context quotient \(\{x \mid uxv \in L\}\) through the set \(\{m \in M \mid \varphi(u)\, m\, \varphi(v) \in P\}\).

theorem Recognizes.contextQuotient [Monoid Carrier] {L : Language Symbol}
    {morphism : FreeMonoid Symbol →* Carrier} {accept : Set Carrier}
    (hrec : Recognizes L morphism accept) (left right : List Symbol) :
    Recognizes (contextQuotient L left right) morphism
      (contextAccept morphism accept left right)

Uses 3 · Used by 3

Statement usesRecognition of a language by a monoid morphism · Accepting set for a context quotient · Context quotient

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

DefinitionThe canonical map to the syntactic monoid of a context quotient#✓fully proved

Let \(L\) be a language over an alphabet \(A\), let \(u, v\) be words over \(A\), and write \(u^{-1} L v^{-1} = \{x \mid uxv \in L\}\). Let \(\eta\) be the syntactic morphism of \(L\) and \(\eta'\) the syntactic morphism of \(u^{-1} L v^{-1}\). This is the monoid morphism from the image of \(\eta\) to the syntactic monoid of \(u^{-1} L v^{-1}\) that sends \(\eta(x)\) to \(\eta'(x)\) for every word \(x\) over \(A\).

noncomputable def contextQuotientToSyntactic (L : Language Symbol) (left right : List Symbol) :
    MonoidHom.mrange (syntacticMorphism L) →* SyntacticMonoid (contextQuotient L left right) :=
  recognizerImageToSyntactic (syntacticMorphism L)
    (contextAccept (syntacticMorphism L) (syntacticAccept L) left right)
    ((recognizes_syntacticMorphism L).contextQuotient left right)

Uses 10 · Used by 1

Statement usesRecognition of a language by a monoid morphism · Recognizers recognize context quotients · Syntactic monoid · Accepting set for a context quotient · Context quotient · Map from a recognizer's image to the syntactic monoid · The syntactic morphism recognizes its language · Accepting set of the syntactic monoid · Syntactic congruence · Syntactic morphism

Used bySize bound for the syntactic monoid of a context quotient

TheoremSize bound for the syntactic monoid of a context quotient#✓fully proved

Let \(L\) be a language over an alphabet \(A\), let \(u, v\) be words over \(A\), and write \(u^{-1} L v^{-1} = \{x \mid uxv \in L\}\) for the context quotient. If the image of the syntactic morphism of \(L\) and the syntactic monoid of \(u^{-1} L v^{-1}\) are both finite, then the syntactic monoid of \(u^{-1} L v^{-1}\) has at most as many elements as the image of the syntactic morphism of \(L\).

theorem card_syntacticMonoid_contextQuotient_le_mrange (L : Language Symbol)
    (left right : List Symbol)
    [Fintype (MonoidHom.mrange (syntacticMorphism L))]
    [Fintype (SyntacticMonoid (contextQuotient L left right))] :
    Fintype.card (SyntacticMonoid (contextQuotient L left right)) ≤
      Fintype.card (MonoidHom.mrange (syntacticMorphism L))

Uses 10

Statement usesSyntactic monoid · Context quotient · Syntactic congruence · Syntactic morphism

Proof usesRecognizers recognize context quotients · Accepting set for a context quotient · The canonical map to the syntactic monoid of a context quotient · The image of a recognizer maps onto the syntactic monoid · The syntactic morphism recognizes its language · Accepting set of the syntactic monoid

TheoremContext quotients preserve finiteness of the syntactic monoid#✓fully proved

Let \(L\) be a language over an alphabet \(A\) whose syntactic monoid is finite. Then for all words \(u, v\) over \(A\), the syntactic monoid of the context quotient \(u^{-1} L v^{-1} = \{x \mid uxv \in L\}\) is finite.

theorem finite_syntacticMonoid_contextQuotient (L : Language Symbol) (left right : List Symbol)
    [Finite (SyntacticMonoid L)] :
    Finite (SyntacticMonoid (contextQuotient L left right))

Uses 9 · Used by 1

Statement usesSyntactic monoid · Context quotient

Proof usesRecognizers recognize context quotients · Accepting set for a context quotient · Finite recognizers give finite syntactic monoids · The syntactic morphism recognizes its language · Accepting set of the syntactic monoid · Syntactic congruence · Syntactic morphism

Used byRegular languages are closed under context quotients

TheoremRegular languages are closed under context quotients#✓fully proved

If \(L\) is a regular language over an alphabet \(A\), then for all words \(u, v\) over \(A\), the context quotient \(u^{-1} L v^{-1} = \{x \mid uxv \in L\}\) is regular.

theorem IsRegular.contextQuotient {L : Language Symbol} (hL : L.IsRegular)
    (left right : List Symbol) : (contextQuotient L left right).IsRegular

Uses 4 · Used by 1

Statement usesContext quotient

Proof usesSyntactic monoid · Context quotients preserve finiteness of the syntactic monoid · Regular languages are those with finite syntactic monoid

Used byNon-universality makes the reduction language non-regular

TheoremSyntactic equivalence via context quotients#✓fully proved

Let \(L\) be a language over an alphabet \(A\). Two words \(x, y\) over \(A\) are syntactically equivalent for \(L\) if and only if, for all words \(u, v\) over \(A\), \(x\) lies in the context quotient \(u^{-1} L v^{-1} = \{w \mid uwv \in L\}\) exactly when \(y\) does.

theorem syntacticRel_iff_mem_contextQuotient (L : Language Symbol)
    (x y : FreeMonoid Symbol) :
    syntacticRel L x y ↔
      ∀ left right,
        FreeMonoid.toList x ∈ contextQuotient L left right ↔
          FreeMonoid.toList y ∈ contextQuotient L left right

Uses 2

Statement usesContext quotient · Syntactic equivalence

DefinitionRight quotient of a language by a word#✓fully proved

For a language \(L\) over an alphabet \(\Sigma\) and a word \(w \in \Sigma^*\), the right quotient of \(L\) by \(w\) is the language \(\{x \in \Sigma^* : xw \in L\}\) of all words \(x\) whose concatenation \(xw\) with \(w\) lies in \(L\).

def rightQuotient (L : Language Symbol) (suffix : List Symbol) : Language Symbol :=
  {x | x ++ suffix ∈ L}

Used by 4

Used byRight quotients preserve finiteness of the syntactic monoid · Recognizers recognize right quotients · Regular languages are closed under right quotients by fixed words · The canonical map to the syntactic monoid of a right quotient

DefinitionAccepting set for a left quotient#✓fully proved

Let \(\varphi \colon A^* \to M\) be a monoid morphism from the free monoid on an alphabet \(A\) to a monoid \(M\), let \(P \subseteq M\), and let \(u\) be a word over \(A\). The accepting set for the left quotient by \(u\) is \(\{m \in M \mid \varphi(u)\, m \in P\}\).

def leftQuotientAccept [Monoid Carrier] (morphism : FreeMonoid Symbol →* Carrier)
    (accept : Set Carrier) (pre : List Symbol) : Set Carrier :=
  {m | morphism (FreeMonoid.ofList pre) * m ∈ accept}

Used by 3

Used byLeft quotients preserve finiteness of the syntactic monoid · Recognizers recognize left quotients · The canonical map to the syntactic monoid of a left quotient

DefinitionAccepting set for a right quotient#✓fully proved

Let \(\varphi \colon A^* \to M\) be a monoid morphism from the free monoid on an alphabet \(A\) to a monoid \(M\), let \(P \subseteq M\), and let \(u\) be a word over \(A\). The accepting set for the right quotient by \(u\) is \(\{m \in M \mid m\, \varphi(u) \in P\}\).

def rightQuotientAccept [Monoid Carrier] (morphism : FreeMonoid Symbol →* Carrier)
    (accept : Set Carrier) (suffix : List Symbol) : Set Carrier :=
  {m | m * morphism (FreeMonoid.ofList suffix) ∈ accept}

Used by 3

Used byRight quotients preserve finiteness of the syntactic monoid · Recognizers recognize right quotients · The canonical map to the syntactic monoid of a right quotient

TheoremRecognizers recognize left quotients#✓fully proved

Let \(\varphi \colon A^* \to M\) be a monoid morphism from the free monoid on an alphabet \(A\) to a monoid \(M\) that recognizes a language \(L\) over \(A\) through \(P \subseteq M\), that is, a word \(x\) lies in \(L\) exactly when \(\varphi(x) \in P\). Then for every word \(u\) over \(A\), \(\varphi\) recognizes the left quotient \(\{x \mid ux \in L\}\) through the set \(\{m \in M \mid \varphi(u)\, m \in P\}\).

theorem Recognizes.leftQuotient [Monoid Carrier] {L : Language Symbol}
    {morphism : FreeMonoid Symbol →* Carrier} {accept : Set Carrier}
    (hrec : Recognizes L morphism accept) (pre : List Symbol) :
    Recognizes (L.leftQuotient pre) morphism
      (leftQuotientAccept morphism accept pre)

Uses 2 · Used by 2

Statement usesRecognition of a language by a monoid morphism · Accepting set for a left quotient

Used byLeft quotients preserve finiteness of the syntactic monoid · The canonical map to the syntactic monoid of a left quotient

TheoremRecognizers recognize right quotients#✓fully proved

Let \(\varphi \colon A^* \to M\) be a monoid morphism from the free monoid on an alphabet \(A\) to a monoid \(M\) that recognizes a language \(L\) over \(A\) through \(P \subseteq M\), that is, a word \(x\) lies in \(L\) exactly when \(\varphi(x) \in P\). Then for every word \(u\) over \(A\), \(\varphi\) recognizes the right quotient \(\{x \mid xu \in L\}\) through the set \(\{m \in M \mid m\, \varphi(u) \in P\}\).

theorem Recognizes.rightQuotient [Monoid Carrier] {L : Language Symbol}
    {morphism : FreeMonoid Symbol →* Carrier} {accept : Set Carrier}
    (hrec : Recognizes L morphism accept) (suffix : List Symbol) :
    Recognizes (rightQuotient L suffix) morphism
      (rightQuotientAccept morphism accept suffix)

Uses 3 · Used by 2

Statement usesRecognition of a language by a monoid morphism · Right quotient of a language by a word · Accepting set for a right quotient

Used byRight quotients preserve finiteness of the syntactic monoid · The canonical map to the syntactic monoid of a right quotient

DefinitionThe canonical map to the syntactic monoid of a left quotient#✓fully proved

Let \(L\) be a language over an alphabet \(A\), let \(u\) be a word over \(A\), and write \(u^{-1} L = \{x \mid ux \in L\}\). Let \(\eta\) be the syntactic morphism of \(L\) and \(\eta'\) the syntactic morphism of \(u^{-1} L\). This is the monoid morphism from the image of \(\eta\) to the syntactic monoid of \(u^{-1} L\) that sends \(\eta(x)\) to \(\eta'(x)\) for every word \(x\) over \(A\).

noncomputable def leftQuotientToSyntactic (L : Language Symbol) (pre : List Symbol) :
    MonoidHom.mrange (syntacticMorphism L) →* SyntacticMonoid (L.leftQuotient pre) :=
  recognizerImageToSyntactic (syntacticMorphism L)
    (leftQuotientAccept (syntacticMorphism L) (syntacticAccept L) pre)
    ((recognizes_syntacticMorphism L).leftQuotient pre)

Uses 9

Statement usesRecognition of a language by a monoid morphism · Recognizers recognize left quotients · Syntactic monoid · Accepting set for a left quotient · Map from a recognizer's image to the syntactic monoid · The syntactic morphism recognizes its language · Accepting set of the syntactic monoid · Syntactic congruence · Syntactic morphism

DefinitionThe canonical map to the syntactic monoid of a right quotient#✓fully proved

Let \(L\) be a language over an alphabet \(A\), let \(u\) be a word over \(A\), and write \(L u^{-1} = \{x \mid xu \in L\}\). Let \(\eta\) be the syntactic morphism of \(L\) and \(\eta'\) the syntactic morphism of \(L u^{-1}\). This is the monoid morphism from the image of \(\eta\) to the syntactic monoid of \(L u^{-1}\) that sends \(\eta(x)\) to \(\eta'(x)\) for every word \(x\) over \(A\).

noncomputable def rightQuotientToSyntactic (L : Language Symbol) (suffix : List Symbol) :
    MonoidHom.mrange (syntacticMorphism L) →* SyntacticMonoid (rightQuotient L suffix) :=
  recognizerImageToSyntactic (syntacticMorphism L)
    (rightQuotientAccept (syntacticMorphism L) (syntacticAccept L) suffix)
    ((recognizes_syntacticMorphism L).rightQuotient suffix)

Uses 10

Statement usesRecognition of a language by a monoid morphism · Recognizers recognize right quotients · Syntactic monoid · Map from a recognizer's image to the syntactic monoid · The syntactic morphism recognizes its language · Right quotient of a language by a word · Accepting set for a right quotient · Accepting set of the syntactic monoid · Syntactic congruence · Syntactic morphism

TheoremLeft quotients preserve finiteness of the syntactic monoid#✓fully proved

Let \(L\) be a language over an alphabet \(A\) whose syntactic monoid is finite. Then for every word \(u\) over \(A\), the syntactic monoid of the left quotient \(u^{-1} L = \{x \mid ux \in L\}\) is finite.

theorem finite_syntacticMonoid_leftQuotient (L : Language Symbol) (pre : List Symbol)
    [Finite (SyntacticMonoid L)] : Finite (SyntacticMonoid (L.leftQuotient pre))

Uses 8

Statement usesSyntactic monoid

Proof usesRecognizers recognize left quotients · Finite recognizers give finite syntactic monoids · Accepting set for a left quotient · The syntactic morphism recognizes its language · Accepting set of the syntactic monoid · Syntactic congruence · Syntactic morphism

TheoremRight quotients preserve finiteness of the syntactic monoid#✓fully proved

Let \(L\) be a language over an alphabet \(A\) whose syntactic monoid is finite. Then for every word \(u\) over \(A\), the syntactic monoid of the right quotient \(L u^{-1} = \{x \mid xu \in L\}\) is finite.

theorem finite_syntacticMonoid_rightQuotient (L : Language Symbol) (suffix : List Symbol)
    [Finite (SyntacticMonoid L)] : Finite (SyntacticMonoid (rightQuotient L suffix))

Uses 9 · Used by 1

Statement usesSyntactic monoid · Right quotient of a language by a word

Proof usesRecognizers recognize right quotients · Finite recognizers give finite syntactic monoids · The syntactic morphism recognizes its language · Accepting set for a right quotient · Accepting set of the syntactic monoid · Syntactic congruence · Syntactic morphism

Used byRegular languages are closed under right quotients by fixed words

TheoremRegular languages are closed under right quotients by fixed words#✓fully proved

If \(L\) is a regular language over an alphabet \(A\), then for every word \(u\) over \(A\), the right quotient \(L u^{-1} = \{x \mid xu \in L\}\) is regular.

theorem IsRegular.rightQuotient' {L : Language Symbol} (hL : L.IsRegular)
    (suffix : List Symbol) : (rightQuotient L suffix).IsRegular

Uses 4

Statement usesRight quotient of a language by a word

Proof usesSyntactic monoid · Right quotients preserve finiteness of the syntactic monoid · Regular languages are those with finite syntactic monoid

TheoremRegular languages are closed under left quotients by fixed words#✓fully proved

If \(L\) is a regular language over an alphabet \(A\), then for every word \(u\) over \(A\), the left quotient \(u^{-1} L = \{x \mid ux \in L\}\) is regular.

The proof starts a DFA for \(L\) in the state it reaches on \(u\).

theorem IsRegular.leftQuotient {L : Language Symbol} (hL : L.IsRegular) (pre : List Symbol) :
    (L.leftQuotient pre).IsRegular

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.