Ambiguity problem for context-free grammars

DefinitionThe ambiguity grammar of a PCP instance#✓fully proved

Let \(P = [(t_0, b_0), \dots, (t_{m-1}, b_{m-1})]\) be a list of dominoes over an alphabet \(\alpha\), with top words \(t_i\) and bottom words \(b_i\). The ambiguity grammar of \(P\) is the encoded context-free grammar over the terminals \(\alpha \sqcup \mathbb{N}\) (letters and indices) with nonterminals \(S = 0\), \(A = 1\), \(B = 2\), start symbol \(S\), and the productions \(S \to A\) and \(S \to B\) together with, for every \(i < m\), the productions \(A \to t_i\, A\, i\), \(A \to t_i\, i\), \(B \to b_i\, B\, i\) and \(B \to b_i\, i\), in which the index \(i\) is a terminal.

def ambGrammar (P : List (Domino α)) : EncodedCFG (α ⊕ ℕ) :=
  ⟨0, (0, [ntSym 1]) :: (0, [ntSym 2]) :: (sideRules Prod.fst 1 P ++ sideRules Prod.snd 2 P)⟩

Uses 4 · Used by 8

Statement usesEncoded nonterminal symbol · The productions of a side grammar · Domino (Post correspondence problem) · Encoded context-free grammars

Used byLeftmost derivations in the ambiguity grammar · The productions of \(A\) and \(B\) 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 · PCP many-one reduces to ambiguity of context-free grammars · The ambiguity grammar is primitive recursive

DefinitionThe canonical rule sequence along an index sequence#✓fully proved

Let \(P\) be a list of dominoes over \(\alpha\), let \(\sigma\) assign a word over \(\alpha\) to each domino, let \(A\) be a natural number, and for \(i \in \mathbb{N}\) write \(w_i\) for \(\sigma\) applied to the \(i\)-th domino of \(P\) (the domino with both words empty when \(i\) is past the end of \(P\)). For a sequence \(i_1, \dots, i_n\) of natural numbers, this is the list of productions, with terminals \(\alpha \sqcup \mathbb{N}\) and nonterminals \(\mathbb{N}\), consisting of \(A \to w_{i_k}\, A\, i_k\) for \(k = 1, \dots, n - 1\) in order, followed by \(A \to w_{i_n}\, i_n\), where the letters of \(w_{i_k}\) and the index \(i_k\) are terminals and \(A\) is a nonterminal; the empty sequence gives the empty list.

def canon (side : Domino α → List α) (A : ℕ) (P : List (Domino α)) :
    List ℕ → List (ContextFreeRule (α ⊕ ℕ) ℕ)
  | [] => []
  | [i] => [EncodedCFG.decodeRule (termRule side A P i)]
  | i :: j :: is => EncodedCFG.decodeRule (contRule side A P i) :: canon side A P (j :: is)

Uses 4 · Used by 5

Statement usesThe continuation production · The terminating production of a side grammar · Domino (Post correspondence problem) · Decoding a production

Used byLeftmost 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

TheoremThe productions of \(A\) and \(B\) in the ambiguity grammar#✓fully proved

Let \(P = [(t_0, b_0), \dots, (t_{m-1}, b_{m-1})]\) be a list of dominoes, and let \(A\), \(B\) be the nonterminals of the ambiguity grammar of \(P\) for its top and bottom words. Every production of that grammar with left-hand side \(A\) is \(A \to t_i\, A\, i\) or \(A \to t_i\, i\) for some \(i < m\), and every production with left-hand side \(B\) is \(B \to b_i\, B\, i\) or \(B \to b_i\, i\) for some \(i < m\).

theorem cases_of_mem_ambGrammar_of_input {side : Domino α → List α} {A : ℕ}
    (hA : (A = 1 ∧ side = Prod.fst) ∨ (A = 2 ∧ side = Prod.snd))
    {r : ContextFreeRule (α ⊕ ℕ) ℕ} (hr : r ∈ (ambGrammar P).toCFG.rules) (hin : r.input = A) :
    ∃ i < P.length, r = EncodedCFG.decodeRule (contRule side A P i) ∨
      r = EncodedCFG.decodeRule (termRule side A P i)

Uses 9 · Used by 1

Statement usesThe ambiguity grammar of a PCP instance · The continuation production · The terminating production of a side grammar · Domino (Post correspondence problem) · Decoding a production · Grammar denoted by an encoding

Proof usesEncoded nonterminal symbol · The productions of a side grammar · Encoded context-free grammars

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

TheoremLeftmost derivations from \(A\) and \(B\) follow an index sequence#✓fully proved

Let \(P = [(t_0, b_0), \dots, (t_{m-1}, b_{m-1})]\) be a list of dominoes, let \(A\), \(B\) be the nonterminals of the ambiguity grammar of \(P\) for its top and bottom words, and let \(u\), \(v\) be words of terminals. Every leftmost derivation of a word \(w\) from the sentential form \(u\,A\,v\) is the canonical rule sequence from \(A\) for the words \(t_i\) along some nonempty sequence \(i_1, \dots, i_n\) of indices less than \(m\), and \(w = u\, t_{i_1} \cdots t_{i_n}\, i_n \cdots i_1\, v\). Likewise, every leftmost derivation of \(w\) from \(u\,B\,v\) is the canonical rule sequence from \(B\) for the words \(b_i\) along such a sequence, and \(w = u\, b_{i_1} \cdots b_{i_n}\, i_n \cdots i_1\, v\).

theorem eq_canon_of_leftDerivation {side : Domino α → List α} {A : ℕ}
    (hA : (A = 1 ∧ side = Prod.fst) ∨ (A = 2 ∧ side = Prod.snd))
    {s : List (Symbol (α ⊕ ℕ) (ambGrammar P).toCFG.NT)} {w : List (α ⊕ ℕ)}
    {rs : List (ContextFreeRule (α ⊕ ℕ) (ambGrammar P).toCFG.NT)}
    (h : LeftDerivation (ambGrammar P).toCFG s w rs) :
    ∀ pre suf : List (α ⊕ ℕ),
      s = pre.map Symbol.terminal ++ Symbol.nonterminal A :: suf.map Symbol.terminal →
      ∃ is : List ℕ, is ≠ [] ∧ (∀ i ∈ is, i < P.length) ∧ rs = canon side A P is ∧
        w = pre ++ sideWord side P is ++ suf

Uses 15 · Used by 1

Statement usesThe ambiguity grammar of a PCP instance · The canonical rule sequence along an index sequence · The side word of an index sequence · Domino (Post correspondence problem) · Grammar denoted by an encoding · Leftmost derivation

Proof usesThe productions of \(A\) and \(B\) in the ambiguity grammar · The continuation production · The \(i\)-th domino of a list · The letter part of an index sequence · The encoded letter terminal · The terminating production of a side grammar · Decoding a production · Decoding a grammar symbol · Leftmost derivations from a word of terminals are empty

Used byLeftmost derivations in the ambiguity grammar

TheoremThe leftmost derivation along an index sequence#✓fully proved

Let \(P = [(t_0, b_0), \dots, (t_{m-1}, b_{m-1})]\) be a list of dominoes, and let \(A\), \(B\) be the nonterminals of the ambiguity grammar of \(P\) for its top and bottom words. For every nonempty sequence \(i_1, \dots, i_n\) of indices less than \(m\) and all words of terminals \(u\), \(v\), the canonical rule sequence from \(A\) for the words \(t_i\) along \(i_1, \dots, i_n\) is a leftmost derivation of \(u\, t_{i_1} \cdots t_{i_n}\, i_n \cdots i_1\, v\) from \(u\,A\,v\), and the canonical rule sequence from \(B\) for the words \(b_i\) along \(i_1, \dots, i_n\) is a leftmost derivation of \(u\, b_{i_1} \cdots b_{i_n}\, i_n \cdots i_1\, v\) from \(u\,B\,v\).

theorem leftDerivation_canon {side : Domino α → List α} {A : ℕ}
    (hA : (A = 1 ∧ side = Prod.fst) ∨ (A = 2 ∧ side = Prod.snd)) :
    ∀ is : List ℕ, is ≠ [] → (∀ i ∈ is, i < P.length) → ∀ pre suf : List (α ⊕ ℕ),
      LeftDerivation (ambGrammar P).toCFG
        (pre.map Symbol.terminal ++ Symbol.nonterminal A :: suf.map Symbol.terminal)
        (pre ++ sideWord side P is ++ suf) (canon side A P is)

Uses 16 · Used by 1

Statement usesThe ambiguity grammar of a PCP instance · The canonical rule sequence along an index sequence · The side word of an index sequence · Domino (Post correspondence problem) · Grammar denoted by an encoding · Leftmost derivation

Proof usesThe continuation production · The \(i\)-th domino of a list · The letter part of an index sequence · The encoded letter terminal · Encoded nonterminal symbol · The productions of a side grammar · The terminating production of a side grammar · Encoded context-free grammars · Decoding a production · Decoding a grammar symbol

Used byLeftmost derivations from the start symbol along an index sequence

DefinitionThe start production \(S \to A\)#✓fully proved

For an alphabet \(\alpha\) and a natural number \(A\), this is the production with terminals \(\alpha \sqcup \mathbb{N}\) and nonterminals \(\mathbb{N}\) whose left-hand side is the nonterminal \(S = 0\) and whose right-hand side is the single nonterminal \(A\).

In the ambiguity grammar of a PCP instance it is used with \(A = 1\) and \(A = 2\).

def startRule (A : ℕ) : ContextFreeRule (α ⊕ ℕ) ℕ := ⟨0, [Symbol.nonterminal A]⟩

Used by 3

Used byLeftmost derivations in the ambiguity grammar · The ambiguity grammar of \(P\) is ambiguous exactly when \(P\) has a solution · Leftmost derivations from the start symbol along an index sequence

TheoremLeftmost derivations in the ambiguity grammar#✓fully proved

Let \(P = [(t_0, b_0), \dots, (t_{m-1}, b_{m-1})]\) be a list of dominoes, and let \(S\), \(A\), \(B\) be the nonterminals of the ambiguity grammar of \(P\). Every leftmost derivation of a word \(w\) from \(S\) in that grammar has one of two forms, for some nonempty sequence \(i_1, \dots, i_n\) of indices less than \(m\): either it is \(S \to A\) followed by the canonical rule sequence from \(A\) for the words \(t_i\) along \(i_1, \dots, i_n\), and \(w = t_{i_1} \cdots t_{i_n}\, i_n \cdots i_1\); or it is \(S \to B\) followed by the canonical rule sequence from \(B\) for the words \(b_i\) along \(i_1, \dots, i_n\), and \(w = b_{i_1} \cdots b_{i_n}\, i_n \cdots i_1\).

theorem cases_of_leftDerivation_start {w : List (α ⊕ ℕ)}
    {rs : List (ContextFreeRule (α ⊕ ℕ) (ambGrammar P).toCFG.NT)}
    (h : LeftDerivation (ambGrammar P).toCFG [Symbol.nonterminal 0] w rs) :
    ∃ A side, ((A = 1 ∧ side = Prod.fst) ∨ (A = 2 ∧ side = Prod.snd)) ∧
      ∃ is : List ℕ, is ≠ [] ∧ (∀ i ∈ is, i < P.length) ∧
        rs = startRule A :: canon side A P is ∧ w = sideWord side P is

Uses 14 · Used by 1

Statement usesThe ambiguity grammar of a PCP instance · The canonical rule sequence along an index sequence · The side word of an index sequence · The start production \(S \to A\) · Domino (Post correspondence problem) · Grammar denoted by an encoding · Leftmost derivation

Proof usesThe continuation production · Leftmost derivations from \(A\) and \(B\) follow an index sequence · Encoded nonterminal symbol · The productions of a side grammar · The terminating production of a side grammar · Encoded context-free grammars · Decoding a production

Used byThe ambiguity grammar of \(P\) is ambiguous exactly when \(P\) has a solution

TheoremLeftmost derivations from the start symbol along an index sequence#✓fully proved

Let \(P = [(t_0, b_0), \dots, (t_{m-1}, b_{m-1})]\) be a list of dominoes, and let \(S\), \(A\), \(B\) be the nonterminals of the ambiguity grammar of \(P\). For every nonempty sequence \(i_1, \dots, i_n\) of indices less than \(m\), the production \(S \to A\) followed by the canonical rule sequence from \(A\) for the words \(t_i\) along \(i_1, \dots, i_n\) is a leftmost derivation of \(t_{i_1} \cdots t_{i_n}\, i_n \cdots i_1\) from \(S\), and the production \(S \to B\) followed by the canonical rule sequence from \(B\) for the words \(b_i\) along \(i_1, \dots, i_n\) is a leftmost derivation of \(b_{i_1} \cdots b_{i_n}\, i_n \cdots i_1\) from \(S\).

theorem leftDerivation_start {A : ℕ} {side : Domino α → List α}
    (hA : (A = 1 ∧ side = Prod.fst) ∨ (A = 2 ∧ side = Prod.snd)) {is : List ℕ} (hne : is ≠ [])
    (hlt : ∀ i ∈ is, i < P.length) :
    LeftDerivation (ambGrammar P).toCFG [Symbol.nonterminal 0] (sideWord side P is)
      (startRule A :: canon side A P is)

Uses 12 · Used by 1

Statement usesThe ambiguity grammar of a PCP instance · The canonical rule sequence along an index sequence · The side word of an index sequence · The start production \(S \to A\) · Domino (Post correspondence problem) · Grammar denoted by an encoding · Leftmost derivation

Proof usesThe leftmost derivation along an index sequence · Encoded nonterminal symbol · The productions of a side grammar · Encoded context-free grammars · Decoding a production

Used byThe ambiguity grammar of \(P\) is ambiguous exactly when \(P\) has a solution

TheoremThe ambiguity grammar of \(P\) is ambiguous exactly when \(P\) has a solution#✓fully proved

For every list \(P\) of dominoes, the ambiguity grammar of \(P\) is ambiguous, that is, some word has two different leftmost derivations from its start symbol, if and only if \(P\) has a PCP solution.

theorem isAmbiguous_iff_pcp (P : List (Domino α)) : IsAmbiguous (ambGrammar P).toCFG ↔ PCP P

Uses 18 · Used by 1

Statement usesThe ambiguity grammar of a PCP instance · Domino (Post correspondence problem) · The Post correspondence problem · Grammar denoted by an encoding · Ambiguous grammar

Proof usesThe canonical rule sequence along an index sequence · Leftmost derivations in the ambiguity grammar · The \(i\)-th domino of a list · Unique splitting of letters followed by markers · The letter part of an index sequence · Leftmost derivations from the start symbol along an index sequence · The language of a side grammar · A PCP instance is solvable exactly when its top and bottom grammars share a word · The side grammar of a PCP instance · The side word of an index sequence · The start production \(S \to A\) · Language of an encoded grammar · Leftmost derivation

Used byPCP many-one reduces to ambiguity of context-free grammars

TheoremThe ambiguity grammar is primitive recursive#✓fully proved

For every alphabet \(\alpha\) with a primitive recursive encoding by natural numbers, the map sending a list \(P\) of dominoes over \(\alpha\) to the ambiguity grammar of \(P\) is primitive recursive, where encoded grammars are encoded as pairs of a start nonterminal and a list of productions.

theorem primrec_ambGrammar [Primcodable α] : Primrec (ambGrammar (α := α))

Uses 11 · Used by 1

Statement usesThe ambiguity grammar of a PCP instance · Domino (Post correspondence problem) · Encoded context-free grammars · Encoded grammars as pairs

Proof usesThe continuation production · The \(i\)-th domino of a list · The encoded index terminal · The encoded letter terminal · Encoded nonterminal symbol · The productions of a side grammar · The terminating production of a side grammar

Used byPCP many-one reduces to ambiguity of context-free grammars

TheoremPCP many-one reduces to ambiguity of context-free grammars#✓fully proved

For every alphabet \(\alpha\) with a primitive recursive encoding by natural numbers and decidable equality, the Post correspondence problem over \(\alpha\) many-one reduces to ambiguity of encoded context-free grammars over the terminals \(\alpha \sqcup \mathbb{N}\): there is a computable function sending each list \(P\) of dominoes over \(\alpha\) to such a grammar, which is ambiguous if and only if \(P\) has a PCP solution.

theorem manyOneReducible_pcp_isAmbiguous [Primcodable α] [DecidableEq α] :
    ManyOneReducible (PCP (α := α)) fun g : EncodedCFG (α ⊕ ℕ) ↦ IsAmbiguous g.toCFG

Uses 9 · Used by 1

Statement usesDomino (Post correspondence problem) · The Post correspondence problem · Encoded context-free grammars · Encoded grammars as pairs · Grammar denoted by an encoding · Ambiguous grammar

Proof usesThe ambiguity grammar of a PCP instance · The ambiguity grammar of \(P\) is ambiguous exactly when \(P\) has a solution · The ambiguity grammar is primitive recursive

Used byWhether a context-free grammar is ambiguous is undecidable

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.