Inverse homomorphic images of context-free languages

13 fully proved

Right letters

DefinitionRight projection of a word#✓fully proved

For a word \(u\) over the disjoint union \(T \oplus T'\) of two alphabets, its right projection is the word over \(T'\) obtained from \(u\) by deleting every letter from \(T\) and reading each remaining letter as a letter of \(T'\), keeping their order.

def projRight (u : List (T ⊕ T')) : List T' :=
  u.filterMap Sum.getRight?

Used by 6

Used byMarker loops fill in the left letters · Language of the marker-insertion grammar · Valuation for the marker-insertion grammar · Marked form of a word · Context-free languages are closed under inverse homomorphisms · Context-free languages are closed under inserting letters

Inserting marker letters

DefinitionMarker translation of a symbol#✓fully proved

Let \(g\) be a context-free grammar over \(T'\) and let \(T\) be an alphabet. Each symbol of \(g\) is translated to a string of symbols with terminals in \(T \sqcup T'\) and nonterminals those of \(g\) together with two new nonterminals \(S\) and \(D\): a terminal \(b \in T'\) becomes the marker \(D\) followed by \(b\), and a nonterminal \(A\) of \(g\) becomes \(A\).

def insSymbol : Symbol T' g.NT → List (Symbol (T ⊕ T') (Option (Option g.NT)))
  | .terminal b => [.nonterminal none, .terminal (.inr b)]
  | .nonterminal A => [.nonterminal (some (some A))]

Used by 4

Used byMarker-insertion grammar · The marker-insertion grammar simulates the original grammar · Marker loops fill in the left letters · Language of the marker-insertion grammar

DefinitionMarked form of a word#✓fully proved

Let \(g\) be a context-free grammar over \(T'\), let \(T\) be an alphabet, and let \(u\) be a word over \(T \sqcup T'\). The marked form of \(u\) is the sentential form, with terminals in \(T \sqcup T'\) and nonterminals those of \(g\) together with two new nonterminals \(S\) and \(D\), that lists the letters of \(u\) from \(T'\) in order, each preceded by the marker \(D\), followed by one more \(D\).

def markedForm {g : ContextFreeGrammar T'} (u : List (T ⊕ T')) :
    List (Symbol (T ⊕ T') (Option (Option g.NT))) :=
  (projRight u).flatMap (fun b => [.nonterminal none, .terminal (.inr b)]) ++ [.nonterminal none]

Uses 1 · Used by 2

Statement usesRight projection of a word

Used byMarker loops fill in the left letters · Language of the marker-insertion grammar

AbbreviationMarker-insertion grammar#✓fully proved

Let \(g\) be a context-free grammar over \(T'\) with start symbol \(A_0\), and let \(T\) be a finite alphabet. The marker-insertion grammar of \(g\) is the context-free grammar over \(T \sqcup T'\) whose nonterminals are those of \(g\) together with a new start symbol \(S\) and a marker \(D\), and whose rules are: for each rule \(A \to \alpha\) of \(g\), the rule \(A \to \alpha'\), where \(\alpha'\) is \(\alpha\) with \(D\) inserted in front of each terminal; the rule \(S \to A_0 D\); the rule \(D \to \varepsilon\); and the rule \(D \to a D\) for each \(a \in T\).

noncomputable abbrev insGrammar : ContextFreeGrammar (T ⊕ T') where
  NT := Option (Option g.NT)
  initial := some none
  rules :=
    g.rules.image (fun r => ⟨some (some r.input), r.output.flatMap (insSymbol (T := T) g)⟩) ∪
      ({⟨some none, [.nonterminal (some (some g.initial)), .nonterminal none]⟩, ⟨none, []⟩} ∪
        Finset.univ.image fun a : T => ⟨none, [.terminal (.inl a), .nonterminal none]⟩)

Uses 1 · Used by 4

Statement usesMarker translation of a symbol

Used byThe marker-insertion grammar simulates the original grammar · Marker loops fill in the left letters · Language of the marker-insertion grammar · Context-free languages are closed under inserting letters

TheoremThe marker-insertion grammar simulates the original grammar#✓fully proved

Let \(g\) be a context-free grammar over \(T'\) and let \(T\) be a finite alphabet. If \(g\) derives a sentential form \(y\) from a sentential form \(x\), then the marker-insertion grammar of \(g\) over \(T \sqcup T'\) derives the translation of \(y\) from the translation of \(x\), where a sentential form is translated by replacing each of its symbols by its marker translation.

theorem insGrammar_derives_flatMap {x y : List (Symbol T' g.NT)} (h : g.Derives x y) :
    (insGrammar (T := T) g).Derives (x.flatMap (insSymbol g)) (y.flatMap (insSymbol g))

Uses 2 · Used by 1

Statement usesMarker-insertion grammar · Marker translation of a symbol

Used byLanguage of the marker-insertion grammar

TheoremMarker loops fill in the left letters#✓fully proved

Let \(g\) be a context-free grammar over \(T'\) and let \(T\) be a finite alphabet. For every word \(u\) over \(T \sqcup T'\), the marker-insertion grammar of \(g\) derives \(u\) from the marked form of \(u\), the sentential form that lists the letters of \(u\) from \(T'\) in order, each preceded by the marker nonterminal \(D\), followed by one more \(D\).

theorem insGrammar_derives_markedForm :
    ∀ u : List (T ⊕ T'), (insGrammar (T := T) g).Derives (markedForm u) (u.map .terminal)

Uses 4 · Used by 1

Statement usesMarker-insertion grammar · Marked form of a word

Proof usesMarker translation of a symbol · Right projection of a word

Used byLanguage of the marker-insertion grammar

DefinitionValuation for the marker-insertion grammar#✓fully proved

Let \(g\) be a context-free grammar over \(T'\) and let \(T\) be an alphabet. This valuation assigns a language over \(T \sqcup T'\) to each nonterminal of \(g\) and to the two new nonterminals \(S\) and \(D\) of the marker-insertion grammar of \(g\): to the marker \(D\) the words with no letter from \(T'\); to the new start symbol \(S\) the words whose letters from \(T'\) form a word of the language of \(g\); and to a nonterminal \(A\) of \(g\) the words whose letters from \(T'\) form a word that \(g\) derives from \(A\).

def insValuation (g : ContextFreeGrammar T') : Option (Option g.NT) → Language (T ⊕ T')
  | none => {u | projRight u = []}
  | some none => {u | projRight u ∈ g.language}
  | some (some A) => {u | projRight u ∈ languageFrom g A}

Uses 2 · Used by 1

Statement usesLanguage generated from a nonterminal · Right projection of a word

Used byLanguage of the marker-insertion grammar

TheoremLanguage of the marker-insertion grammar#✓fully proved

Let \(g\) be a context-free grammar over \(T'\) and let \(T\) be a finite alphabet. The marker-insertion grammar of \(g\) generates exactly the words \(u\) over \(T \sqcup T'\) whose letters from \(T'\), read in order, form a word of the language of \(g\).

theorem insGrammar_language :
    (insGrammar (T := T) g).language = {u | projRight u ∈ g.language}

Uses 14 · Used by 1

Statement usesMarker-insertion grammar · Right projection of a word

Proof usesValuation of a grammar · Interpretation of a sentential form · Interpretation of a concatenation · Interpretation of a grammar symbol · The marker-insertion grammar simulates the original grammar · Marker loops fill in the left letters · Marker translation of a symbol · Valuation for the marker-insertion grammar · The languages generated from each nonterminal form a valuation · Language generated from a nonterminal · Valuations bound the language of a grammar · Marked form of a word

Used byContext-free languages are closed under inserting letters

TheoremContext-free languages are closed under inserting letters#✓fully proved

Let \(T\) be a finite alphabet and let \(L\) be a context-free language over an alphabet \(T'\). Then the language of words \(u\) over the disjoint union \(T \oplus T'\) whose letters from \(T'\), read in order, form a word of \(L\) is context-free.

theorem IsContextFree.preimage_projRight [Finite T] {L : Language T'} (hL : L.IsContextFree) :
    Language.IsContextFree {u : List (T ⊕ T') | projRight u ∈ L}

Uses 3 · Used by 1

Statement usesRight projection of a word

Proof usesMarker-insertion grammar · Language of the marker-insertion grammar

Used byContext-free languages are closed under inverse homomorphisms

Inverse homomorphisms

DefinitionBlock of a letter#✓fully proved

For a map \(\varphi\) from \(T\) to words over \(T'\) and a letter \(a \in T\), the block of \(a\) is the word over the disjoint union \(T \sqcup T'\) that consists of \(a\), as a letter of \(T\), followed by the letters of \(\varphi(a)\), as letters of \(T'\).

def block (φ : T → List T') (a : T) : List (T ⊕ T') :=
  Sum.inl a :: (φ a).map Sum.inr

Used by 1

Used byContext-free languages are closed under inverse homomorphisms

DefinitionErasing right letters#✓fully proved

Erasing right letters is the map from letters of the disjoint union \(T \sqcup T'\) to words over \(T\) that sends a letter \(a\) of \(T\) to the one-letter word \(a\) and every letter of \(T'\) to the empty word.

def eraseRight : T ⊕ T' → List T :=
  Sum.elim (fun a => [a]) (fun _ => [])

Used by 2

Used byContext-free languages are closed under inverse homomorphisms · The right quotient of a context-free language by a regular language is context-free

TheoremContext-free languages are closed under inverse homomorphisms#✓fully proved

Context-free languages are closed under inverse homomorphisms from a finite alphabet.

theorem IsContextFree.preimage_hom [Finite T] {L : Language T'} (hL : L.IsContextFree)
    (φ : T → List T') :
    Language.IsContextFree {w : List T | (w.map φ).flatten ∈ L}

Uses 7 · Used by 2

Proof usesContext-free languages are closed under homomorphic images · Intersection of a context-free language with a regular language · Context-free languages are closed under inserting letters · Finite languages are regular · Block of a letter · Erasing right letters · Right projection of a word

Used byContext-free languages are closed under inverse free-monoid morphisms · The right quotient of a context-free language by a regular language is context-free

TheoremContext-free languages are closed under inverse free-monoid morphisms#✓fully proved

Let \(T\) be a finite alphabet, \(T'\) an alphabet, \(\sigma \colon T^* \to {T'}^*\) a morphism of free monoids and \(L\) a context-free language over \(T'\). Then the inverse image \(\sigma^{-1}(L) = \{x \in T^* \mid \sigma(x) \in L\}\) is a context-free language over \(T\).

theorem IsContextFree.preimage_wordMorphism [Finite T] {L : Language T'} (hL : L.IsContextFree)
    (σ : FreeMonoid T →* FreeMonoid T') : (wordMorphismPreimage σ L).IsContextFree

Uses 3

Statement usesInverse image under a word morphism

Proof usesContext-free languages are closed under inverse homomorphisms · Letterwise description of the inverse image under a word morphism

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.