Inverse homomorphic images of regular languages

DefinitionAlphabet preimage#✓fully proved

Let \(f \colon \Sigma \to \Gamma\) be a map between alphabets and \(L\) a language over \(\Gamma\). The alphabet preimage of \(L\) under \(f\) is the language over \(\Sigma\) consisting of the words \(a_1 a_2 \cdots a_n\) such that \(f(a_1) f(a_2) \cdots f(a_n) \in L\).

def alphabetPreimage (f : Source → Target) (L : Language Target) : Language Source :=
  {x | x.map f ∈ L}

Used by 10

Used byRegular languages are closed under alphabet preimages · Alphabet preimages are inverse images under word morphisms · 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 · Renaming letters by a bijection preserves and reflects regularity · The alphabet preimage morphism recognizes the alphabet preimage · Syntactic equivalence pulls back along an alphabet map · Non-universality makes the reduction language non-regular

DefinitionAlphabet preimage morphism#✓fully proved

Let \(f \colon \Sigma \to \Gamma\) be a map between alphabets and \(L\) a language over \(\Gamma\). The alphabet preimage morphism of \(f\) and \(L\) is the monoid morphism from the free monoid \(\Sigma^*\) to the syntactic monoid of \(L\) that sends a word \(w\) to the syntactic class of \(f^*(w)\), the word obtained by applying \(f\) to each letter of \(w\). It is the composite of the letterwise map \(f^* \colon \Sigma^* \to \Gamma^*\) with the syntactic morphism of \(L\).

def alphabetPreimageMorphism (f : Source → Target) (L : Language Target) :
    FreeMonoid Source →* SyntacticMonoid L :=
  (syntacticMorphism L).comp (FreeMonoid.map f)

Uses 3 · Used by 4

Statement usesSyntactic monoid · Syntactic congruence · Syntactic morphism

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 · The alphabet preimage morphism recognizes the alphabet preimage

TheoremThe alphabet preimage morphism recognizes the alphabet preimage#✓fully proved

Let \(f \colon \Sigma \to \Gamma\) be a map between alphabets and \(L\) a language over \(\Gamma\). Write \(f^*(w)\) for the word obtained by applying \(f\) to each letter of a word \(w\), \([u]_L\) for the class of a word \(u\) in the syntactic monoid \(M(L)\) of \(L\), \(A_L \subseteq M(L)\) for the accepting set of classes of words in \(L\), and \(\varphi \colon \Sigma^* \to M(L)\) for the alphabet preimage morphism \(w \mapsto [f^*(w)]_L\). Then \(\varphi\) recognizes the alphabet preimage \(\{w \in \Sigma^* \mid f^*(w) \in L\}\) through \(A_L\): for every word \(w \in \Sigma^*\), we have \(f^*(w) \in L\) if and only if \(\varphi(w) \in A_L\).

theorem recognizes_alphabetPreimageMorphism (f : Source → Target) (L : Language Target) :
    Recognizes (alphabetPreimage f L) (alphabetPreimageMorphism f L) (syntacticAccept L)

Uses 7 · Used by 3

Statement usesRecognition of a language by a monoid morphism · Syntactic monoid · Alphabet preimage · Alphabet preimage morphism · Accepting set of the syntactic monoid · Syntactic congruence

Proof usesSyntactic morphism

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

TheoremSyntactic equivalence pulls back along an alphabet map#✓fully proved

Let \(f \colon \Sigma \to \Gamma\) be a map between alphabets, \(L\) a language over \(\Gamma\), and \(K\) the alphabet preimage \(\{w \in \Sigma^* \mid f^*(w) \in L\}\), where \(f^*(w)\) is the word obtained by applying \(f\) to each letter of \(w\). If \(x, y \in \Sigma^*\) are words such that \(f^*(x)\) and \(f^*(y)\) are syntactically equivalent for \(L\), then \(x\) and \(y\) are syntactically equivalent for \(K\).

theorem syntacticRel_alphabetPreimage_of_map (f : Source → Target) (L : Language Target)
    {x y : FreeMonoid Source} (h : syntacticRel L (FreeMonoid.map f x) (FreeMonoid.map f y)) :
    syntacticRel (alphabetPreimage f L) x y

Uses 2

Statement usesAlphabet preimage · Syntactic equivalence

TheoremThe alphabet preimage morphism refines the preimage's syntactic congruence#✓fully proved

Let \(f \colon \Sigma \to \Gamma\) be a map between alphabets, \(L\) a language over \(\Gamma\) with syntactic monoid \(M(L)\), and \(\varphi \colon \Sigma^* \to M(L)\) the alphabet preimage morphism, which sends a word \(w\) to the class in \(M(L)\) of the word \(f^*(w)\) obtained by applying \(f\) to each letter of \(w\). If two words \(x, y \in \Sigma^*\) satisfy \(\varphi(x) = \varphi(y)\), then \(x\) and \(y\) are syntactically congruent for the alphabet preimage \(\{w \in \Sigma^* \mid f^*(w) \in L\}\). In other words, the kernel congruence of \(\varphi\) is contained in the syntactic congruence of the alphabet preimage.

theorem alphabetPreimageMorphism_ker_le (f : Source → Target) (L : Language Target) :
    Con.ker (alphabetPreimageMorphism f L) ≤ syntacticCon (alphabetPreimage f L)

Uses 7

Statement usesSyntactic monoid · Alphabet preimage · Alphabet preimage morphism · Syntactic congruence

Proof usesRecognizer kernels refine the syntactic congruence · The alphabet preimage morphism recognizes the alphabet preimage · Accepting set of the syntactic monoid

DefinitionDivision map for the syntactic monoid of an alphabet preimage#✓fully proved

Let \(f \colon \Sigma \to \Gamma\) be a map between alphabets and \(L\) a language over \(\Gamma\). Write \(f^*(w)\) for the word obtained by applying \(f\) to each letter of a word \(w\), \([u]_L\) for the class of a word \(u\) in the syntactic monoid \(M(L)\) of \(L\), \(K\) for the alphabet preimage \(\{w \in \Sigma^* \mid f^*(w) \in L\}\), and \(\varphi \colon \Sigma^* \to M(L)\) for the alphabet preimage morphism \(w \mapsto [f^*(w)]_L\). This is the monoid morphism from the submonoid \(\varphi(\Sigma^*)\) of \(M(L)\) to the syntactic monoid \(M(K)\) that sends \(\varphi(w)\) to \([w]_K\); it is well defined because \(\varphi(x) = \varphi(y)\) implies \([x]_K = [y]_K\).

This morphism is surjective, so \(M(K)\) is a quotient of a submonoid of \(M(L)\).

noncomputable def alphabetPreimageToSyntactic (f : Source → Target) (L : Language Target) :
    MonoidHom.mrange (alphabetPreimageMorphism f L) →*
      SyntacticMonoid (alphabetPreimage f L) :=
  recognizerImageToSyntactic (alphabetPreimageMorphism f L) (syntacticAccept L)
    (recognizes_alphabetPreimageMorphism f L)

Uses 7

Statement usesSyntactic monoid · Alphabet preimage · Alphabet preimage morphism · Map from a recognizer's image to the syntactic monoid · The alphabet preimage morphism recognizes the alphabet preimage · Accepting set of the syntactic monoid · Syntactic congruence

TheoremAlphabet preimages preserve finiteness of the syntactic monoid#✓fully proved

Let \(f \colon \Sigma \to \Gamma\) be a map between alphabets and \(L\) a language over \(\Gamma\) whose syntactic monoid is finite. Then the syntactic monoid of the alphabet preimage \(\{w \in \Sigma^* \mid f^*(w) \in L\}\) is finite, where \(f^*(w)\) is the word obtained by applying \(f\) to each letter of \(w\).

theorem finite_syntacticMonoid_alphabetPreimage (f : Source → Target) (L : Language Target)
    [Finite (SyntacticMonoid L)] : Finite (SyntacticMonoid (alphabetPreimage f L))

Uses 7 · Used by 1

Statement usesSyntactic monoid · Alphabet preimage

Proof usesAlphabet preimage morphism · Finite recognizers give finite syntactic monoids · The alphabet preimage morphism recognizes the alphabet preimage · Accepting set of the syntactic monoid · Syntactic congruence

Used byRegular languages are closed under alphabet preimages

TheoremRegular languages are closed under alphabet preimages#✓fully proved

Let \(f \colon \Sigma \to \Gamma\) be a map between alphabets. If \(L\) is a regular language over \(\Gamma\), then its alphabet preimage \(\{w \in \Sigma^* \mid f^*(w) \in L\}\) is regular, where \(f^*(w)\) is the word obtained by applying \(f\) to each letter of \(w\).

theorem IsRegular.alphabetPreimage {L : Language Target} (hL : L.IsRegular)
    (f : Source → Target) : (alphabetPreimage f L).IsRegular

Uses 4 · Used by 2

Statement usesAlphabet preimage

Proof usesSyntactic monoid · Alphabet preimages preserve finiteness of the syntactic monoid · Regular languages are those with finite syntactic monoid

Used byRenaming letters by a bijection preserves and reflects regularity · Non-universality makes the reduction language non-regular

TheoremRenaming letters by a bijection preserves and reflects regularity#✓fully proved

Let \(e \colon \Sigma \to \Gamma\) be a bijection between alphabets and \(L\) a language over \(\Gamma\). The alphabet preimage \(\{w \in \Sigma^* \mid e^*(w) \in L\}\), where \(e^*(w)\) is the word obtained by applying \(e\) to each letter of \(w\), is regular if and only if \(L\) is regular.

theorem isRegular_alphabetPreimage_equiv_iff (e : Source ≃ Target) (L : Language Target) :
    (alphabetPreimage e L).IsRegular ↔ L.IsRegular

Uses 2 · Used by 1

Statement usesAlphabet preimage

Proof usesRegular languages are closed under alphabet preimages

Used byFiniteness of the syntactic monoid is invariant under renaming letters

TheoremFiniteness of the syntactic monoid is invariant under renaming letters#✓fully proved

Let \(e \colon \Sigma \to \Gamma\) be a bijection between alphabets and \(L\) a language over \(\Gamma\). The syntactic monoid of the alphabet preimage \(\{w \in \Sigma^* \mid e^*(w) \in L\}\), where \(e^*(w)\) is the word obtained by applying \(e\) to each letter of \(w\), is finite if and only if the syntactic monoid of \(L\) is finite.

theorem finite_syntacticMonoid_alphabetPreimage_equiv_iff (e : Source ≃ Target)
    (L : Language Target) :
    Finite (SyntacticMonoid (alphabetPreimage e L)) ↔ Finite (SyntacticMonoid L)

Uses 4

Statement usesSyntactic monoid · Alphabet preimage

Proof usesRenaming letters by a bijection preserves and reflects regularity · Regular languages are those with finite syntactic monoid

DefinitionInverse image under a word morphism#✓fully proved

Let \(\Sigma\) and \(\Gamma\) be alphabets, \(h \colon \Sigma^* \to \Gamma^*\) a monoid morphism between their free monoids of words, and \(L\) a language over \(\Gamma\). The inverse image of \(L\) under \(h\) is the language \(h^{-1}(L) = \{w \in \Sigma^* \mid h(w) \in L\}\) over \(\Sigma\).

def wordMorphismPreimage (substitution : FreeMonoid Source →* FreeMonoid Target)
    (L : Language Target) : Language Source :=
  {x | FreeMonoid.toList (substitution (FreeMonoid.ofList x)) ∈ L}

Used by 7

Used byContext-free languages are closed under inverse free-monoid morphisms · Alphabet preimages are inverse images under word morphisms · Inverse images under word morphisms preserve finiteness of the syntactic monoid · Syntactic equivalence pulls back along a word morphism · Regular languages are closed under inverse word morphisms · Letterwise description of the inverse image under a word morphism · Division map for the syntactic monoid of an inverse image

TheoremWord morphisms act letter by letter#✓fully proved

Let \(h \colon \Sigma^* \to \Gamma^*\) be a monoid morphism between free monoids. For every word \(a_1 a_2 \cdots a_n \in \Sigma^*\) (including the empty word, \(n = 0\)), we have \(h(a_1 a_2 \cdots a_n) = h(a_1) h(a_2) \cdots h(a_n)\), the concatenation of the images of its letters.

theorem toList_wordMorphism_ofList (substitution : FreeMonoid Source →* FreeMonoid Target)
    (x : List Source) :
    FreeMonoid.toList (substitution (FreeMonoid.ofList x)) =
      (x.map fun a => FreeMonoid.toList (substitution (FreeMonoid.of a))).flatten

Used by 1

Used byLetterwise description of the inverse image under a word morphism

TheoremLetterwise description of the inverse image under a word morphism#✓fully proved

Let \(h \colon \Sigma^* \to \Gamma^*\) be a monoid morphism between free monoids and \(L\) a language over \(\Gamma\). The inverse image \(h^{-1}(L) = \{w \in \Sigma^* \mid h(w) \in L\}\) consists exactly of the words \(a_1 a_2 \cdots a_n \in \Sigma^*\) such that the concatenation \(h(a_1) h(a_2) \cdots h(a_n)\) of the images of their letters lies in \(L\).

theorem wordMorphismPreimage_eq_flatten (substitution : FreeMonoid Source →* FreeMonoid Target)
    (L : Language Target) :
    wordMorphismPreimage substitution L =
      {x | (x.map fun a => FreeMonoid.toList (substitution (FreeMonoid.of a))).flatten ∈ L}

Uses 2 · Used by 1

Statement usesInverse image under a word morphism

Proof usesWord morphisms act letter by letter

Used byContext-free languages are closed under inverse free-monoid morphisms

DefinitionRecognizing morphism of an inverse image#✓fully proved

Let \(h \colon \Sigma^* \to \Gamma^*\) be a monoid morphism between free monoids and \(L\) a language over \(\Gamma\) with syntactic monoid \(M(L)\). The recognizing morphism of \(h\) and \(L\) is the monoid morphism \(\Sigma^* \to M(L)\) that sends a word \(w\) to the syntactic class \([h(w)]_L\) of \(h(w)\); it is the composite of \(h\) with the syntactic morphism of \(L\).

def wordMorphismRecognizer (substitution : FreeMonoid Source →* FreeMonoid Target)
    (L : Language Target) : FreeMonoid Source →* SyntacticMonoid L :=
  (syntacticMorphism L).comp substitution

Uses 3 · Used by 2

Statement usesSyntactic monoid · Syntactic congruence · Syntactic morphism

Used byInverse images under word morphisms preserve finiteness of the syntactic monoid · Division map for the syntactic monoid of an inverse image

TheoremSyntactic equivalence pulls back along a word morphism#✓fully proved

Let \(h \colon \Sigma^* \to \Gamma^*\) be a monoid morphism between free monoids, \(L\) a language over \(\Gamma\), and \(K = h^{-1}(L) = \{w \in \Sigma^* \mid h(w) \in L\}\) its inverse image. If \(x, y \in \Sigma^*\) are words such that \(h(x)\) and \(h(y)\) are syntactically equivalent for \(L\), then \(x\) and \(y\) are syntactically equivalent for \(K\).

theorem syntacticRel_wordMorphismPreimage_of_map
    (substitution : FreeMonoid Source →* FreeMonoid Target) (L : Language Target)
    {x y : FreeMonoid Source} (h : syntacticRel L (substitution x) (substitution y)) :
    syntacticRel (wordMorphismPreimage substitution L) x y

Uses 2

Statement usesSyntactic equivalence · Inverse image under a word morphism

DefinitionDivision map for the syntactic monoid of an inverse image#✓fully proved

Let \(h \colon \Sigma^* \to \Gamma^*\) be a monoid morphism between free monoids and \(L\) a language over \(\Gamma\). Write \([u]_L\) for the class of a word \(u\) in the syntactic monoid \(M(L)\) of \(L\), \(K\) for the inverse image \(h^{-1}(L) = \{w \in \Sigma^* \mid h(w) \in L\}\), and \(\varphi \colon \Sigma^* \to M(L)\) for the recognizing morphism \(w \mapsto [h(w)]_L\). This is the monoid morphism from the submonoid \(\varphi(\Sigma^*)\) of \(M(L)\) to the syntactic monoid \(M(K)\) that sends \(\varphi(w)\) to \([w]_K\); it is well defined because \(\varphi(x) = \varphi(y)\) implies \([x]_K = [y]_K\).

This morphism is surjective, so \(M(K)\) is a quotient of a submonoid of \(M(L)\).

noncomputable def wordMorphismPreimageToSyntactic
    (substitution : FreeMonoid Source →* FreeMonoid Target) (L : Language Target) :
    MonoidHom.mrange (wordMorphismRecognizer substitution L) →*
      SyntacticMonoid (wordMorphismPreimage substitution L) :=
  recognizerImageToSyntactic (wordMorphismRecognizer substitution L) (syntacticAccept L)
    (recognizes_wordMorphismRecognizer substitution L)

Uses 8

Statement usesRecognition of a language by a monoid morphism · Syntactic monoid · Map from a recognizer's image to the syntactic monoid · Accepting set of the syntactic monoid · Syntactic congruence · Syntactic morphism · Inverse image under a word morphism · Recognizing morphism of an inverse image

TheoremInverse images under word morphisms preserve finiteness of the syntactic monoid#✓fully proved

Let \(h \colon \Sigma^* \to \Gamma^*\) be a monoid morphism between free monoids and \(L\) a language over \(\Gamma\) whose syntactic monoid is finite. Then the syntactic monoid of the inverse image \(h^{-1}(L) = \{w \in \Sigma^* \mid h(w) \in L\}\) is finite.

theorem finite_syntacticMonoid_wordMorphismPreimage
    (substitution : FreeMonoid Source →* FreeMonoid Target) (L : Language Target)
    [Finite (SyntacticMonoid L)] :
    Finite (SyntacticMonoid (wordMorphismPreimage substitution L))

Uses 8 · Used by 1

Statement usesSyntactic monoid · Inverse image under a word morphism

Proof usesRecognition of a language by a monoid morphism · Finite recognizers give finite syntactic monoids · Accepting set of the syntactic monoid · Syntactic congruence · Syntactic morphism · Recognizing morphism of an inverse image

Used byRegular languages are closed under inverse word morphisms

TheoremRegular languages are closed under inverse word morphisms#✓fully proved

Let \(h \colon \Sigma^* \to \Gamma^*\) be a monoid morphism between free monoids. If \(L\) is a regular language over \(\Gamma\), then its inverse image \(h^{-1}(L) = \{w \in \Sigma^* \mid h(w) \in L\}\) is regular.

theorem IsRegular.wordMorphismPreimage {L : Language Target} (hL : L.IsRegular)
    (substitution : FreeMonoid Source →* FreeMonoid Target) :
    (wordMorphismPreimage substitution L).IsRegular

Uses 4

Statement usesInverse image under a word morphism

Proof usesSyntactic monoid · Inverse images under word morphisms preserve finiteness of the syntactic monoid · Regular languages are those with finite syntactic monoid

TheoremAlphabet preimages are inverse images under word morphisms#✓fully proved

Let \(f \colon \Sigma \to \Gamma\) be a map between alphabets, \(f^* \colon \Sigma^* \to \Gamma^*\) the monoid morphism that applies \(f\) to each letter of a word, and \(L\) a language over \(\Gamma\). Then the alphabet preimage of \(L\) under \(f\) equals the inverse image \((f^*)^{-1}(L) = \{w \in \Sigma^* \mid f^*(w) \in L\}\) of \(L\) under \(f^*\).

theorem alphabetPreimage_eq_wordMorphismPreimage (f : Source → Target)
    (L : Language Target) :
    alphabetPreimage f L = wordMorphismPreimage (FreeMonoid.map f) L

Uses 2

Statement usesAlphabet preimage · Inverse image under a word morphism

19 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.