Intersection problem for context-free languages

18 fully proved

The grammars

DefinitionThe encoded letter terminal#✓fully proved

For a letter \(a \in \alpha\), this is \(a\) as an encoded terminal over the alphabet \(\alpha \oplus \mathbb{N}\): the element \(\mathrm{inr}(\mathrm{inl}\, a)\) of \(\mathbb{N} \oplus (\alpha \oplus \mathbb{N})\), whose left summand \(\mathbb{N}\) holds the nonterminals and whose right summand holds the terminals.

def letterSym (a : α) : ℕ ⊕ (α ⊕ ℕ) := .inr (.inl a)

Used by 8

Used byLeftmost derivations from \(A\) and \(B\) follow an index sequence · The leftmost derivation along an index sequence · The ambiguity grammar is primitive recursive · The continuation production · The construction of derivations · The analysis of derivations · PCP many-one reduces to nonemptiness of the intersection of two context-free languages · The terminating production of a side grammar

DefinitionThe encoded index terminal#✓fully proved

For \(i \in \mathbb{N}\), this is the index \(i\) as an encoded terminal over the alphabet \(\alpha \oplus \mathbb{N}\): the element \(\mathrm{inr}(\mathrm{inr}\, i)\) of \(\mathbb{N} \oplus (\alpha \oplus \mathbb{N})\), whose left summand \(\mathbb{N}\) holds the nonterminals and whose right summand holds the terminals.

def indexSym (i : ℕ) : ℕ ⊕ (α ⊕ ℕ) := .inr (.inr i)

Used by 4

Used byThe ambiguity grammar is primitive recursive · The continuation production · PCP many-one reduces to nonemptiness of the intersection of two context-free languages · The terminating production of a side grammar

DefinitionEncoded nonterminal symbol#✓fully proved

For a natural number \(A\), the nonterminal \(A\) as a symbol of the right-hand side of an encoded production over the terminals \(\alpha \sqcup \mathbb{N}\): the left injection of \(A\) into \(\mathbb{N} \sqcup (\alpha \sqcup \mathbb{N})\).

def ntSym (A : ℕ) : ℕ ⊕ (α ⊕ ℕ) := .inl A

Used by 8

Used byThe ambiguity grammar of a PCP instance · Leftmost derivations in the ambiguity grammar · The productions of \(A\) and \(B\) in the ambiguity grammar · The leftmost derivation along an index sequence · Leftmost derivations from the start symbol along an index sequence · The ambiguity grammar is primitive recursive · The continuation production · PCP many-one reduces to nonemptiness of the intersection of two context-free languages

DefinitionThe \(i\)-th domino of a list#✓fully proved

For a list \(P\) of dominoes and \(i \in \mathbb{N}\), this is the \(i\)-th domino of \(P\) (counting from \(0\)) when \(i\) is less than the length of \(P\), and the domino whose top and bottom words are both empty otherwise.

def domino (P : List (Domino α)) (i : ℕ) : Domino α := P.getD i ([], [])

Uses 1 · Used by 17

Statement usesDomino (Post correspondence problem)

Used byLeftmost 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 · The ambiguity grammar is primitive recursive · The continuation production · The construction of derivations · The analysis of derivations · The letter part of an index sequence · PCP many-one reduces to nonemptiness of the intersection of two context-free languages · A PCP instance is solvable exactly when its top and bottom grammars share a word · The terminating production of a side grammar · The intended languages form a valuation of the universality grammar · The complement of PCP many-one reduces to universality of context-free grammars · Membership in the mismatch productions · Every mismatched word is derivable from the mismatch nonterminal · The mismatch productions · A PCP instance is solvable exactly when its top and bottom list languages meet

DefinitionThe continuation production#✓fully proved

For a list \(P\) of dominoes, a map \(\sigma\) assigning a word over \(\alpha\) to each domino, a nonterminal \(A \in \mathbb{N}\) and an index \(i \in \mathbb{N}\), this is the production \(A \to w_i\, A\, i\) in encoded form, where \(w_i\) is \(\sigma\) applied to the \(i\)-th domino of \(P\) (the domino with both words empty when \(i\) is past the end of \(P\)): its right-hand side is the letters of \(w_i\) as terminals, then the nonterminal \(A\), then the index terminal \(i\).

def contRule (side : Domino α → List α) (A : ℕ) (P : List (Domino α)) (i : ℕ) :
    ℕ × List (ℕ ⊕ (α ⊕ ℕ)) :=
  (A, (side (domino P i)).map letterSym ++ [ntSym A, indexSym i])

Uses 5 · Used by 10

Statement usesThe \(i\)-th domino of a list · The encoded index terminal · The encoded letter terminal · Encoded nonterminal symbol · Domino (Post correspondence problem)

Used byThe canonical rule sequence along an index sequence · Leftmost 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 leftmost derivation along an index sequence · The ambiguity grammar is primitive recursive · The construction of derivations · The analysis of derivations · PCP many-one reduces to nonemptiness of the intersection of two context-free languages · The productions of a side grammar

DefinitionThe terminating production of a side grammar#✓fully proved

Let \(P = (d_0, \dots, d_{k-1})\) be a list of dominoes over \(\alpha\), set \(d_i = (\varepsilon, \varepsilon)\) for \(i \ge k\), let \(\sigma\) assign a word over \(\alpha\) to each domino, and write \(w_i = \sigma(d_i)\). For a nonterminal \(A\) and a natural number \(i\), this is the encoded production \(A \to w_i \, i\), whose right-hand side is the letters of \(w_i\) as terminals followed by the index terminal \(i\).

def termRule (side : Domino α → List α) (A : ℕ) (P : List (Domino α)) (i : ℕ) :
    ℕ × List (ℕ ⊕ (α ⊕ ℕ)) :=
  (A, (side (domino P i)).map letterSym ++ [indexSym i])

Uses 4 · Used by 10

Statement usesThe \(i\)-th domino of a list · The encoded index terminal · The encoded letter terminal · Domino (Post correspondence problem)

Used byThe canonical rule sequence along an index sequence · Leftmost 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 leftmost derivation along an index sequence · The ambiguity grammar is primitive recursive · The construction of derivations · The analysis of derivations · PCP many-one reduces to nonemptiness of the intersection of two context-free languages · The productions of a side grammar

DefinitionThe productions of a side grammar#✓fully proved

Let \(P = (d_0, \dots, d_{k-1})\) be a list of dominoes over \(\alpha\), let \(\sigma\) assign a word over \(\alpha\) to each domino, write \(w_i = \sigma(d_i)\), and let \(A\) be a nonterminal. The side productions are the list of encoded productions \(A \to w_i \, A \, i\) and \(A \to w_i \, i\) for \(i = 0, 1, \dots, k - 1\), where the letters of \(w_i\) are terminals and \(i\) is an index terminal.

def sideRules (side : Domino α → List α) (A : ℕ) (P : List (Domino α)) :
    List (ℕ × List (ℕ ⊕ (α ⊕ ℕ))) :=
  (List.range P.length).flatMap fun i ↦ [contRule side A P i, termRule side A P i]

Uses 3 · Used by 9

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

Used byThe ambiguity grammar of a PCP instance · Leftmost derivations in the ambiguity grammar · The productions of \(A\) and \(B\) in the ambiguity grammar · The leftmost derivation along an index sequence · Leftmost derivations from the start symbol along an index sequence · The ambiguity grammar is primitive recursive · PCP many-one reduces to nonemptiness of the intersection of two context-free languages · The language of a side grammar · The side grammar of a PCP instance

DefinitionThe side grammar of a PCP instance#✓fully proved

Let \(P = (d_0, \dots, d_{k-1})\) be a list of dominoes over \(\alpha\), let \(\sigma\) assign a word over \(\alpha\) to each domino, and write \(w_i = \sigma(d_i)\). The side grammar of \(\sigma\) and \(P\) is the encoded context-free grammar whose terminals are the letters of \(\alpha\) and the index terminals \(0, 1, 2, \dots\), whose start nonterminal is \(S = 0\), and whose productions are \(S \to w_i \, S \, i\) and \(S \to w_i \, i\) for each \(i < k\). Taking for \(\sigma\) the top word of a domino gives the top grammar of \(P\), and the bottom word the bottom grammar.

def sideGrammar (side : Domino α → List α) (P : List (Domino α)) : EncodedCFG (α ⊕ ℕ) :=
  ⟨0, sideRules side 0 P⟩

Uses 3 · Used by 6

Statement usesThe productions of a side grammar · Domino (Post correspondence problem) · Encoded context-free grammars

Used byThe ambiguity grammar of \(P\) is ambiguous exactly when \(P\) has a solution · The construction of derivations · The analysis of derivations · PCP many-one reduces to nonemptiness of the intersection of two context-free languages · The language of a side grammar · A PCP instance is solvable exactly when its top and bottom grammars share a word

DefinitionThe letter part of an index sequence#✓fully proved

For a list \(P\) of dominoes, a map \(\sigma\) assigning a word over \(\alpha\) to each domino, and a sequence \(i_1, \dots, i_n\) of natural numbers, this is the word \(w_{i_1} w_{i_2} \cdots w_{i_n}\) over \(\alpha\), where \(w_i\) is \(\sigma\) applied to the \(i\)-th domino of \(P\) (the domino with both words empty when \(i\) is past the end of \(P\)).

def flat (side : Domino α → List α) (P : List (Domino α)) (is : List ℕ) : List α :=
  is.flatMap fun i ↦ side (domino P i)

Uses 2 · Used by 16

Statement usesThe \(i\)-th domino of a list · Domino (Post correspondence problem)

Used byLeftmost 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 · The construction of derivations · The analysis of derivations · A PCP instance is solvable exactly when its top and bottom grammars share a word · The side word of an index sequence · The universality grammar generates every word exactly when PCP has no solution · The intended languages form a valuation of the universality grammar · The language of the universality grammar · List word of an index sequence · The mismatch language · Every mismatched word is derivable from the mismatch nonterminal · Malformed words are in no list language · Mismatched words are not in the list language · A PCP instance is solvable exactly when its top and bottom list languages meet

DefinitionThe side word of an index sequence#✓fully proved

Let \(P = (d_0, \dots, d_{k-1})\) be a list of dominoes over \(\alpha\), set \(d_i = (\varepsilon, \varepsilon)\) for \(i \ge k\), let \(\sigma\) assign a word over \(\alpha\) to each domino, and write \(w_i = \sigma(d_i)\). The side word of a sequence \(i_1, \dots, i_n\) of natural numbers is the word \(w_{i_1} \cdots w_{i_n} \, i_n \cdots i_1\) over the letters of \(\alpha\) and the index terminals \(0, 1, 2, \dots\): the letters of \(w_{i_1}, \dots, w_{i_n}\) followed by the indices in reverse order.

def sideWord (side : Domino α → List α) (P : List (Domino α)) (is : List ℕ) : List (α ⊕ ℕ) :=
  (flat side P is).map Sum.inl ++ is.reverse.map Sum.inr

Uses 2 · Used by 9

Statement usesThe letter part of an index sequence · Domino (Post correspondence problem)

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 · The construction of derivations · The analysis of derivations · The language of a side grammar · A PCP instance is solvable exactly when its top and bottom grammars share a word

Derivations

TheoremA terminal word derives only itself#✓fully proved

Let \(g\) be a context-free grammar with terminal alphabet \(\alpha \oplus \mathbb{N}\) and let \(u\) be a word over \(\alpha \oplus \mathbb{N}\). If \(g\) derives a sentential form \(v\) from \(u\), read as a string of terminals, then \(v = u\).

theorem eq_of_derives_terminal {g : ContextFreeGrammar (α ⊕ ℕ)} {u : List (α ⊕ ℕ)}
    {v : List (Symbol (α ⊕ ℕ) g.NT)} (h : g.Derives (u.map Symbol.terminal) v) :
    v = u.map Symbol.terminal

Used by 1

Used byThe analysis of derivations

TheoremSplitting a sentential form at its single nonterminal#✓fully proved

Let \(N\) be a type of nonterminals, \(u, v\) words over \(\alpha \oplus \mathbb{N}\), \(A, B \in N\), and \(p, q\) strings of terminals in \(\alpha \oplus \mathbb{N}\) and nonterminals in \(N\). If \(u\, A\, v = p\, B\, q\), where \(u\) and \(v\) are read as strings of terminals, then \(p = u\), \(B = A\) and \(q = v\).

theorem eq_of_terminal_append_nonterminal {N : Type*} {pre suf : List (α ⊕ ℕ)} {A B : N}
    {p q : List (Symbol (α ⊕ ℕ) N)}
    (h : pre.map Symbol.terminal ++ Symbol.nonterminal A :: suf.map Symbol.terminal =
      p ++ [Symbol.nonterminal B] ++ q) :
    p = pre.map Symbol.terminal ∧ B = A ∧ q = suf.map Symbol.terminal

Used by 1

Used byThe analysis of derivations

TheoremThe analysis of derivations#✓fully proved

Let \(P\) be a list of dominoes, \(\sigma\) a map assigning a word over \(\alpha\) to each domino, and \(G\) the context-free grammar of the side grammar of \(P\) for \(\sigma\), with start nonterminal \(S\) and terminals \(\alpha \oplus \mathbb{N}\) (letters and indices). Let \(u, v, x\) be words over \(\alpha \oplus \mathbb{N}\). If \(G\) derives the terminal word \(x\) from the sentential form \(u\, S\, v\), then there is a nonempty sequence \(i_1, \dots, i_n\) of indices, each less than the length of \(P\), such that \(x = u\, w_{i_1} \cdots w_{i_n}\, i_n \cdots i_1\, v\), where \(w_i\) is \(\sigma\) applied to the \(i\)-th domino of \(P\).

Such a derivation applies \(S \to w_i\, S\, i\) for each index but the last and then \(S \to w_i\, i\).

theorem eq_sideWord_of_derives {s : List (Symbol (α ⊕ ℕ) ℕ)} {w : List (α ⊕ ℕ)}
    (h : (sideGrammar side P).toCFG.Derives s (w.map Symbol.terminal)) :
    ∀ pre suf : List (α ⊕ ℕ),
      s = pre.map Symbol.terminal ++ Symbol.nonterminal 0 :: suf.map Symbol.terminal →
      ∃ is : List ℕ, is ≠ [] ∧ (∀ i ∈ is, i < P.length) ∧ w = pre ++ sideWord side P is ++ suf

Uses 14 · Used by 1

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

Proof usesThe continuation production · The \(i\)-th domino of a list · A terminal word derives only itself · Splitting a sentential form at its single nonterminal · The letter part of an index sequence · The encoded letter terminal · The terminating production of a side grammar · Encoded context-free grammars · Decoding a production · Decoding a grammar symbol

Used byThe language of a side grammar

TheoremThe construction of derivations#✓fully proved

Let \(P\) be a list of dominoes, \(\sigma\) a map assigning a word over \(\alpha\) to each domino, and \(G\) the context-free grammar of the side grammar of \(P\) for \(\sigma\), with start nonterminal \(S\) and terminals \(\alpha \oplus \mathbb{N}\) (letters and indices). For every nonempty sequence \(i_1, \dots, i_n\) of indices, each less than the length of \(P\), and all words \(u, v\) over \(\alpha \oplus \mathbb{N}\), \(G\) derives the terminal word \(u\, w_{i_1} \cdots w_{i_n}\, i_n \cdots i_1\, v\) from the sentential form \(u\, S\, v\), where \(w_i\) is \(\sigma\) applied to the \(i\)-th domino of \(P\).

theorem derives_sideWord : ∀ (is : List ℕ), is ≠ [] → (∀ i ∈ is, i < P.length) →
    ∀ pre suf : List (α ⊕ ℕ), (sideGrammar side P).toCFG.Derives
      (pre.map Symbol.terminal ++ Symbol.nonterminal 0 :: suf.map Symbol.terminal)
      ((pre ++ sideWord side P is ++ suf).map Symbol.terminal)

Uses 12 · Used by 1

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

Proof usesThe 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 · Encoded context-free grammars · Decoding a production · Decoding a grammar symbol

Used byThe language of a side grammar

TheoremThe language of a side grammar#✓fully proved

Let \(\alpha\) be an alphabet with decidable equality, let \(P = (d_0, \dots, d_{k-1})\) be a list of dominoes over \(\alpha\), let \(\sigma\) assign a word over \(\alpha\) to each domino, and write \(w_i = \sigma(d_i)\). A word \(u\) over the letters of \(\alpha\) and the index terminals \(0, 1, 2, \dots\) lies in the language of the side grammar of \(\sigma\) and \(P\) if and only if there is a nonempty sequence of indices \(i_1, \dots, i_n\), each less than \(k\), with \(u = w_{i_1} \cdots w_{i_n} \, i_n \cdots i_1\).

theorem mem_language_sideGrammar {w : List (α ⊕ ℕ)} :
    w ∈ (sideGrammar side P).language ↔
      ∃ is : List ℕ, is ≠ [] ∧ (∀ i ∈ is, i < P.length) ∧ w = sideWord side P is

Uses 9 · Used by 2

Statement usesThe side grammar of a PCP instance · The side word of an index sequence · Domino (Post correspondence problem) · Language of an encoded grammar

Proof usesThe construction of derivations · The analysis of derivations · The productions of a side grammar · Encoded context-free grammars · Grammar denoted by an encoding

Used byThe ambiguity grammar of \(P\) is ambiguous exactly when \(P\) has a solution · A PCP instance is solvable exactly when its top and bottom grammars share a word

Common words are PCP solutions

TheoremUnique splitting of letters followed by markers#✓fully proved

Let \(A, C\) be words over \(\alpha\) and \(B, D\) words over \(\beta\), all viewed as words over the disjoint union \(\alpha \oplus \beta\). If \(AB = CD\) as words over \(\alpha \oplus \beta\), then \(A = C\) and \(B = D\).

theorem eq_of_map_inl_append_map_inr {β : Type*} {A C : List α} {B D : List β}
    (h : A.map Sum.inl ++ B.map Sum.inr = C.map Sum.inl ++ D.map Sum.inr) : A = C ∧ B = D

Used by 5

Used byThe ambiguity grammar of \(P\) is ambiguous exactly when \(P\) has a solution · A PCP instance is solvable exactly when its top and bottom grammars share a word · Malformed words are in no list language · Mismatched words are not in the list language · A PCP instance is solvable exactly when its top and bottom list languages meet

TheoremA PCP instance is solvable exactly when its top and bottom grammars share a word#✓fully proved

Let \(P\) be a list of dominoes over an alphabet \(\alpha\) with decidable equality. Then \(P\) has a PCP solution if and only if some word lies both in the language of the side grammar of \(P\) for the top words and in the language of the side grammar of \(P\) for the bottom words.

theorem pcp_iff_exists_mem_inter [DecidableEq α] (P : List (Domino α)) :
    PCP P ↔ ∃ w, w ∈ (sideGrammar Prod.fst P).language ∧ w ∈ (sideGrammar Prod.snd P).language

Uses 12 · Used by 2

Statement usesThe side grammar of a PCP instance · Domino (Post correspondence problem) · The Post correspondence problem · Language of an encoded grammar

Proof usesThe \(i\)-th domino of a list · Unique splitting of letters followed by markers · The letter part of an index sequence · The language of a side grammar · The side word of an index sequence · PCP solution · Bottom word of a domino sequence · Top word of a sequence of dominoes

Used byThe ambiguity grammar of \(P\) is ambiguous exactly when \(P\) has a solution · PCP many-one reduces to nonemptiness of the intersection of two context-free languages

The many-one reduction

TheoremPCP many-one reduces to nonemptiness of the intersection of two context-free languages#✓fully proved

PCP many-one reduces to nonemptiness of the intersection of two context-free languages. Let \(\alpha\) be an alphabet with a primitive recursive encoding and decidable equality. The Post correspondence problem over \(\alpha\) is many-one reducible to the problem of deciding, for a pair \((G_1, G_2)\) of encoded context-free grammars whose terminals are the letters of \(\alpha\) together with the natural numbers, whether some word lies in both the language of \(G_1\) and the language of \(G_2\): there is a computable map sending each list \(P\) of dominoes over \(\alpha\) to such a pair, with \(P\) having a PCP solution if and only if the two languages share a word.

theorem manyOneReducible_pcp_inter [DecidableEq α] :
    ManyOneReducible (PCP (α := α)) fun g : EncodedCFG (α ⊕ ℕ) × EncodedCFG (α ⊕ ℕ) ↦
      ∃ w, w ∈ g.1.language ∧ w ∈ g.2.language

Uses 14 · Used by 1

Statement usesDomino (Post correspondence problem) · The Post correspondence problem · Encoded context-free grammars · Encoded grammars as pairs · Language of an encoded grammar

Proof usesThe continuation production · The \(i\)-th domino of a list · The encoded index terminal · The encoded letter terminal · Encoded nonterminal symbol · A PCP instance is solvable exactly when its top and bottom grammars share a word · The side grammar of a PCP instance · The productions of a side grammar · The terminating production of a side grammar

Used byWhether two context-free languages intersect is undecidable

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.