Ambiguity of context-free grammars

InductiveLeftmost derivation#✓fully proved

Let \(g\) be a context-free grammar, \(u\) a sentential form of \(g\), \(w\) a word of terminals and \(r_1, \dots, r_n\) a list of rules over the terminals and nonterminals of \(g\). The list \(r_1, \dots, r_n\) is a leftmost derivation of \(w\) from \(u\) in \(g\) when every \(r_i\) is a production of \(g\), and, starting from \(u\) and for \(i = 1, \dots, n\) in turn, the leftmost nonterminal of the current sentential form is the left-hand side of \(r_i\) and is replaced by the right-hand side of \(r_i\), and the sentential form reached after these \(n\) steps is \(w\), read as a string of terminals. In particular the empty list is a leftmost derivation of \(w\) from \(u\) exactly when \(u\) is \(w\) read as a string of terminals.

inductive LeftDerivation (g : ContextFreeGrammar T) :
    List (Symbol T g.NT) → List T → List (ContextFreeRule T g.NT) → Prop
  /-- A word of terminals has the empty leftmost derivation. -/
  | done (w : List T) : LeftDerivation g (w.map Symbol.terminal) w []
  /-- Rewrite the leftmost nonterminal `r.input`, after the terminal prefix `p`. -/
  | step {p : List T} {v : List (Symbol T g.NT)} {w : List T} {r : ContextFreeRule T g.NT}
      {rs : List (ContextFreeRule T g.NT)} :
      r ∈ g.rules → LeftDerivation g (p.map Symbol.terminal ++ r.output ++ v) w rs →
      LeftDerivation g (p.map Symbol.terminal ++ Symbol.nonterminal r.input :: v) w (r :: rs)

Used by 9

Used byLeftmost derivations are derivations · Leftmost derivations from a word of terminals are empty · Ambiguous grammar · Words with a leftmost derivation lie in the language · Leftmost derivations in the ambiguity grammar · Leftmost derivations from \(A\) and \(B\) follow an index sequence · The ambiguity grammar of \(P\) is ambiguous exactly when \(P\) has a solution · The leftmost derivation along an index sequence · Leftmost derivations from the start symbol along an index sequence

DefinitionAmbiguous grammar#✓fully proved

A context-free grammar \(g\) is ambiguous if some word of terminals \(w\) has two leftmost derivations from the start symbol of \(g\) that use different lists of rules.

def IsAmbiguous (g : ContextFreeGrammar T) : Prop :=
  ∃ w rs₁ rs₂, rs₁ ≠ rs₂ ∧ LeftDerivation g [Symbol.nonterminal g.initial] w rs₁ ∧
    LeftDerivation g [Symbol.nonterminal g.initial] w rs₂

Uses 1 · Used by 4

Statement usesLeftmost derivation

Used byInherently ambiguous language · The ambiguity grammar of \(P\) is ambiguous exactly when \(P\) has a solution · PCP many-one reduces to ambiguity of context-free grammars · Whether a context-free grammar is ambiguous is undecidable

TheoremLeftmost derivations are derivations#✓fully proved

Let \(g\) be a context-free grammar. If a sentential form \(u\) has a leftmost derivation in \(g\) to a word of terminals \(w\), then \(u\) derives \(w\) in \(g\) (by zero or more rewriting steps).

theorem derives {u : List (Symbol T g.NT)} {w : List T} {rs : List (ContextFreeRule T g.NT)}
    (h : LeftDerivation g u w rs) : g.Derives u (w.map Symbol.terminal)

Uses 1 · Used by 1

Statement usesLeftmost derivation

Used byWords with a leftmost derivation lie in the language

TheoremWords with a leftmost derivation lie in the language#✓fully proved

Let \(g\) be a context-free grammar. If a word of terminals \(w\) has a leftmost derivation in \(g\) from the start symbol of \(g\), then \(w\) belongs to the language of \(g\).

theorem mem_language {w : List T} {rs : List (ContextFreeRule T g.NT)}
    (h : LeftDerivation g [Symbol.nonterminal g.initial] w rs) : w ∈ g.language

Uses 2

Statement usesLeftmost derivation

Proof usesLeftmost derivations are derivations

TheoremLeftmost derivations from a word of terminals are empty#✓fully proved

Let \(g\) be a context-free grammar and \(u\) a word of terminals. If \(u\) has a leftmost derivation in \(g\) with list of rules \(\rho\) to a word of terminals \(w\), then \(\rho\) is the empty list and \(w = u\).

theorem eq_of_terminal {u w : List T} {rs : List (ContextFreeRule T g.NT)}
    (h : LeftDerivation g (u.map Symbol.terminal) w rs) : rs = [] ∧ w = u

Uses 1 · Used by 1

Statement usesLeftmost derivation

Used byLeftmost derivations from \(A\) and \(B\) follow an index sequence

DefinitionCanonical inherently ambiguous context-free language#✓fully proved

The language {a ^ i b ^ j c ^ k | i = j or j = k} over the alphabet Fin 3 (0, 1, 2 for a, b, c): the standard inherently ambiguous context-free language.

def inherentlyAmbiguousLang : Language (Fin 3) :=
  {w | ∃ i j k, (i = j ∨ j = k) ∧
    w = List.replicate i 0 ++ List.replicate j 1 ++ List.replicate k 2}

Sources

• S. Ginsburg, The Mathematical Theory of Context-Free Languages, McGraw-Hill, 1966; J. E. Hopcroft and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, 1979, Chapter 7.

Used by 2

Used byInherently ambiguous example as a union of two languages · The example language is context-free

DefinitionInherently ambiguous language#✓fully proved

A language is inherently ambiguous when it is context-free and every grammar generating it is ambiguous.

def IsInherentlyAmbiguous (L : Language T) : Prop :=
  L.IsContextFree ∧ ∀ g : ContextFreeGrammar T, g.language = L → IsAmbiguous g

Uses 1

Statement usesAmbiguous grammar

TheoremInherently ambiguous example as a union of two languages#✓fully proved

The example language is the union of a ^ n b ^ n c ^ * and a ^ * b ^ n c ^ n.

theorem inherentlyAmbiguousLang_eq :
    inherentlyAmbiguousLang =
      eqPowLang (0 : Fin 3) 1 * KStar.kstar ({[(2 : Fin 3)]} : Language (Fin 3)) +
        (KStar.kstar ({[(0 : Fin 3)]} : Language (Fin 3)) * eqPowLang (1 : Fin 3) 2)

Uses 3 · Used by 1

Statement usesThe language \(a^n b^n\) · Canonical inherently ambiguous context-free language

Proof usesThe Kleene star of a one-letter word

Used byThe example language is context-free

TheoremThe example language is context-free#✓fully proved

The example language is context-free.

theorem inherentlyAmbiguousLang_isContextFree : inherentlyAmbiguousLang.IsContextFree

Uses 8

Statement usesCanonical inherently ambiguous context-free language

Proof usesClosure of context-free languages under union · Closure of context-free languages under Kleene star · Closure of context-free languages under concatenation · Singleton languages are context-free · The language \(a^n b^n\) · The language \(a^n b^n\) is context-free · Inherently ambiguous example as a union of two languages

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.