Quotients of context-free languages

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

For languages \(L\) and \(R\) over an alphabet \(T\), the right quotient of \(L\) by \(R\) is the language of all words \(x\) over \(T\) such that the concatenation \(xy\) lies in \(L\) for some word \(y \in R\).

def rightQuotientLang (L R : Language T) : Language T :=
  {x | ∃ y ∈ R, x ++ y ∈ L}

Used by 2

Used byThe left quotient of a context-free language by a regular language is context-free · The right quotient of a context-free language by a regular language is context-free

DefinitionWords over the left copy of a doubled alphabet#✓fully proved

For an alphabet \(T\), write \(T \sqcup T\) for the disjoint union of a left and a right copy of \(T\). This is the language over \(T \sqcup T\) of the words obtained from a word \(x\) over \(T\) by replacing each letter with its left copy.

def leftWords : Language (T ⊕ T) :=
  {u | ∃ x : List T, u = x.map Sum.inl}

Used by 1

Used byThe right quotient of a context-free language by a regular language is context-free

DefinitionWords of a language marked by the right copy#✓fully proved

For a language \(R\) over an alphabet \(T\), write \(T \sqcup T\) for the disjoint union of a left and a right copy of \(T\). This is the language over \(T \sqcup T\) of the words obtained from a word \(y \in R\) by replacing each letter with its right copy.

def rightWords (R : Language T) : Language (T ⊕ T) :=
  {u | ∃ y ∈ R, u = y.map Sum.inr}

Used by 1

Used byThe right quotient of a context-free language by a regular language is context-free

DefinitionAutomaton for words over the left copy#✓fully proved

For an alphabet \(T\), write \(T \sqcup T\) for the disjoint union of a left and a right copy of \(T\). This is the deterministic automaton over \(T \sqcup T\) with the two states true and false, whose start state and only accepting state are true, and which moves from state \(b\) on a letter \(c\) to true exactly when \(b\) is true and \(c\) lies in the left copy, and to false otherwise.

def leftDFA : DFA (T ⊕ T) Bool :=
  ⟨fun b c => b && c.isLeft, true, {true}⟩

Used by 1

Used byThe right quotient of a context-free language by a regular language is context-free

DefinitionAutomaton running a deterministic automaton on the right copy#✓fully proved

Let \(D\) be a deterministic automaton over an alphabet \(T\), and write \(T \sqcup T\) for the disjoint union of a left and a right copy of \(T\). This is the deterministic automaton over \(T \sqcup T\) whose states are the states of \(D\) together with one extra dead state \(\bot\). From a state \(p\) of \(D\), on the right copy of a letter \(a\) it moves to the state that \(D\) reaches from \(p\) on \(a\); on a letter of the left copy, and from \(\bot\) on any letter, it moves to \(\bot\). Its start state is the start state of \(D\), and its accepting states are the accepting states of \(D\).

def rightDFA : DFA (T ⊕ T) (Option σ) where
  step o c := match o, c with
    | some p, .inr a => some (D.step p a)
    | _, _ => none
  start := some D.start
  accept := {o | ∃ p ∈ D.accept, o = some p}

Used by 1

Used byThe right quotient of a context-free language by a regular language is context-free

DefinitionForgetting the copy of a letter#✓fully proved

For an alphabet \(T\), write \(T \sqcup T\) for the disjoint union of a left and a right copy of \(T\). This map sends the left copy and the right copy of a letter \(a \in T\) to the one-letter word \(a\) over \(T\).

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

Used by 1

Used byThe right quotient of a context-free language by a regular language is context-free

TheoremThe right quotient of a context-free language by a regular language is context-free#✓fully proved

The right quotient of a context-free language by a regular language is context-free, over a finite alphabet.

theorem IsContextFree.rightQuotientLang [Finite T] {L R : Language T} (hL : L.IsContextFree)
    (hR : R.IsRegular) : (Cslib.Language.rightQuotientLang L R).IsContextFree

Uses 10 · Used by 1

Statement usesRight quotient of a language by a language

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 inverse homomorphisms · Automaton for words over the left copy · Words over the left copy of a doubled alphabet · Automaton running a deterministic automaton on the right copy · Words of a language marked by the right copy · Forgetting the copy of a letter · Erasing right letters

Used byThe left quotient of a context-free language by a regular language is context-free

TheoremThe left quotient of a context-free language by a regular language is context-free#✓fully proved

The left quotient of a context-free language by a regular language is context-free, over a finite alphabet.

theorem IsContextFree.leftQuotientLang [Finite T] {L R : Language T} (hL : L.IsContextFree)
    (hR : R.IsRegular) : Language.IsContextFree {y | ∃ x ∈ R, x ++ y ∈ L}

Uses 2

Proof usesThe right quotient of a context-free language by a regular language is context-free · Right quotient of a language by a language

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.