Skip to content

Universality problem for context-free grammars

36 fully proved

Index codes and list languages

DefinitionUnary code of an index#✓fully proved

The code of an index \(i \in \mathbb{N}\) is the bit word \(\mathbf{t}\,\mathbf{f}^i\) of length \(i + 1\): the bit \(\mathbf{t}\) (true) followed by \(i\) copies of the bit \(\mathbf{f}\) (false); with \(|\) for true and \(1\) for false, it is the word \(|\,1^i\).

def bitCode (i : ℕ) : List Bool := true :: List.replicate i false
Used by 12
Used byDomino-independent productions of the universality grammar · Concatenated code of an index sequence · Codes of indices below \(k\) contain no code of \(k\) · The intended languages form a valuation of the universality grammar · The language of the universality grammar · Malformed words · Every word is malformed or well formed · 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 · Malformed words are in no list language

DefinitionConcatenated code of an index sequence#✓fully proved

For a finite sequence \(I = (i_1, \dots, i_n)\) of natural numbers, its code is the bit word \(c(i_1)\,c(i_2) \cdots c(i_n)\), the concatenation of the unary codes \(c(i) = \mathbf{t}\,\mathbf{f}^i\) of its entries; the empty sequence has the empty code.

def bitCodes (I : List ℕ) : List Bool := I.flatMap bitCode
Uses 1 · Used by 13
Statement usesUnary code of an index
Used byConcatenated index codes are uniquely decodable · Codes of indices below \(k\) contain no code of \(k\) · Codes of index sequences below \(k\) · 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 · Every word is malformed or well formed · 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

DefinitionList word of an index sequence#✓fully proved

Let \(P = (d_0, \dots, d_{m-1})\) be a list of dominoes over \(\alpha\), let \(s\) be a function sending each domino to a word over \(\alpha\), and set \(w_i = s(d_i)\) for \(i < m\) and \(w_i = s(\varepsilon, \varepsilon)\) for \(i \ge m\), where \((\varepsilon, \varepsilon)\) is the domino with empty top and bottom. The list word of an index sequence \(i_1, \dots, i_n\) is the word \(w_{i_1} \cdots w_{i_n}\, c(i_n) \cdots c(i_1)\) over \(\alpha \oplus \mathrm{Bool}\), where \(c(i)\) is the unary code of \(i\): the bit \(\mathrm{true}\) followed by \(i\) bits \(\mathrm{false}\).

def listWord (side : Domino α → List α) (P : List (Domino α)) (I : List ℕ) : List (α ⊕ Bool) :=
  (flat side P I).map Sum.inl ++ (bitCodes I.reverse).map Sum.inr
Uses 3 · Used by 5
Statement usesConcatenated code of an index sequence · The letter part of an index sequence · Domino (Post correspondence problem)
Used byThe universality grammar generates every word exactly when PCP has no solution · List language of a PCP instance · 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

DefinitionList language of a PCP instance#✓fully proved

Let \(P = (d_0, \dots, d_{m-1})\) be a list of dominoes over \(\alpha\), let \(s\) be a function sending each domino to a word over \(\alpha\) (for instance its top word), and write \(w_i = s(d_i)\). The list language of \(s\) and \(P\) is the language over \(\alpha \oplus \mathrm{Bool}\) of all words \(w_{i_1} \cdots w_{i_n}\, c(i_n) \cdots c(i_1)\) with \(n \ge 1\) and \(i_1, \dots, i_n < m\), where \(c(i)\) is the unary code of \(i\): the bit \(\mathrm{true}\) followed by \(i\) bits \(\mathrm{false}\).

def listLang (side : Domino α → List α) (P : List (Domino α)) : Language (α ⊕ Bool) :=
  {w | ∃ I : List ℕ, I ≠ [] ∧ (∀ i ∈ I, i < P.length) ∧ w = listWord side P I}
Uses 2 · Used by 4
Statement usesList word of an index sequence · Domino (Post correspondence problem)
Used byThe universality grammar generates every word exactly when PCP has no solution · 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

TheoremConcatenated index codes are uniquely decodable#✓fully proved

For a finite sequence \(I = (i_1, \dots, i_n)\) of natural numbers write \(c(I) = c(i_1) \cdots c(i_n)\), where \(c(i) = \mathbf{t}\,\mathbf{f}^i\) is the unary code of \(i\). If \(I\) and \(J\) are finite sequences of natural numbers with \(c(I) = c(J)\), then \(I = J\).

theorem bitCodes_injective : Function.Injective bitCodes
Uses 1 · Used by 2
Statement usesConcatenated code of an index sequence
Used byMismatched 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 list languages meet#✓fully proved

A list \(P\) of dominoes has a PCP solution if and only if some word belongs both to the list language of the top words of \(P\) and to the list language of the bottom words of \(P\).

theorem pcp_iff_exists_mem_listLang (P : List (Domino α)) :
    PCP P ↔ ∃ w, w ∈ listLang Prod.fst P ∧ w ∈ listLang Prod.snd P
Uses 12 · Used by 1
Statement usesList language of a PCP instance · Domino (Post correspondence problem) · The Post correspondence problem
Proof usesConcatenated code of an index sequence · Concatenated index codes are uniquely decodable · The \(i\)-th domino of a list · Unique splitting of letters followed by markers · The letter part of an index sequence · List word of an index sequence · PCP solution · Bottom word of a domino sequence · Top word of a sequence of dominoes
Used byThe universality grammar generates every word exactly when PCP has no solution

The grammar

DefinitionEncoded nonterminal#✓fully proved

For a type \(\alpha\) and a natural number \(A\), the nonterminal \(A\) as a symbol of an encoded grammar over the alphabet \(\alpha \oplus \mathrm{Bool}\), that is, the element \(\mathrm{inl}\, A\) of \(\mathbb{N} \oplus (\alpha \oplus \mathrm{Bool})\).

def uNt (A : ℕ) : ℕ ⊕ (α ⊕ Bool) := .inl A
Used by 7
Used byDomino-independent productions of the universality grammar · The intended languages form a valuation of the universality grammar · The language 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

DefinitionEncoded letter terminal#✓fully proved

For a letter \(a \in \alpha\), the terminal \(a\) of the alphabet \(\alpha \oplus \mathrm{Bool}\) as a symbol of an encoded grammar, that is, the element \(\mathrm{inr}(\mathrm{inl}\, a)\) of \(\mathbb{N} \oplus (\alpha \oplus \mathrm{Bool})\).

def uLetter (a : α) : ℕ ⊕ (α ⊕ Bool) := .inr (.inl a)
Used by 7
Used byDomino-independent productions of the universality grammar · The intended languages form a valuation of the universality grammar · The language 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

DefinitionEncoded bit terminal#✓fully proved

For a type \(\alpha\) and a bit \(b\), the terminal \(b\) of the alphabet \(\alpha \oplus \mathrm{Bool}\) as a symbol of an encoded grammar, that is, the element \(\mathrm{inr}(\mathrm{inr}\, b)\) of \(\mathbb{N} \oplus (\alpha \oplus \mathrm{Bool})\).

def uBit (b : Bool) : ℕ ⊕ (α ⊕ Bool) := .inr (.inr b)
Used by 7
Used byDomino-independent productions of the universality grammar · The intended languages form a valuation of the universality grammar · The language 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

DefinitionList of all letters#✓fully proved

For a finite alphabet \(\alpha\), the list of all letters of \(\alpha\), each appearing exactly once, in some fixed but unspecified order.

noncomputable def allLetters : List α := Finset.univ.toList
Used by 6
Used byDomino-independent productions of the universality grammar · The intended languages form a valuation of the universality grammar · The language of the universality grammar · The complement of PCP many-one reduces to universality of context-free grammars · Every mismatched word is derivable from the mismatch nonterminal · The letters other than a given letter

DefinitionThe letters other than a given letter#✓fully proved

For a letter \(a\) of a finite alphabet with decidable equality, the list of all letters \(b\) of the alphabet with \(b \ne a\), in the order of a fixed enumeration of the alphabet.

noncomputable def others (a : α) : List α := allLetters.filter fun b ↦ b ≠ a
Uses 1 · Used by 5
Statement usesList of all letters
Used byThe 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

DefinitionDomino-independent productions of the universality grammar#✓fully proved

For a finite alphabet \(\alpha\) and \(k \in \mathbb{N}\), this is a list of productions whose nonterminals \(N_0, N_1, \dots\) are encoded as natural numbers and whose terminals are the letters \(a \in \alpha\) and the two bits \(\mathbf{t}\) (true) and \(\mathbf{f}\) (false). Writing \(c(i) = \mathbf{t}\,\mathbf{f}^i\) for the unary code of an index \(i\), the list consists of the productions \(N_3 \to \varepsilon\), \(N_5 \to \varepsilon\), \(N_6 \to \varepsilon\), \(N_7 \to \varepsilon\); \(N_5 \to \mathbf{t}\,N_5\), \(N_5 \to \mathbf{f}\,N_5\), \(N_6 \to \mathbf{t}\,N_6\), \(N_6 \to \mathbf{f}\,N_6\); \(N_0 \to N_3\), \(N_0 \to N_3\,\mathbf{f}\,N_5\), \(N_0 \to N_6\,c(k)\,N_6\), \(N_0 \to N_1\), \(N_0 \to N_2\); for each letter \(a \in \alpha\), the productions \(N_3 \to a\,N_3\), \(N_4 \to a\,N_3\), \(N_6 \to a\,N_6\), \(N_0 \to N_6\,\mathbf{t}\,a\,N_6\) and \(N_0 \to N_6\,\mathbf{f}\,a\,N_6\); and for each \(i < k\), the production \(N_7 \to c(i)\,N_7\).

The nonterminal \(N_0\) is the start symbol. The intended languages are: for \(N_3\) the words of letters, for \(N_4\) the nonempty words of letters, for \(N_5\) the words of bits, for \(N_6\) all words, and for \(N_7\) the concatenated codes of indices below \(k\). The start productions (those with left side \(N_0\)) generate the malformed words and the two mismatch nonterminals \(N_1\) and \(N_2\).

noncomputable def baseRules (k : ℕ) : List (ℕ × List (ℕ ⊕ (α ⊕ Bool))) :=
  [(3, []), (5, []), (6, []), (7, []),
    (5, [uBit true, uNt 5]), (5, [uBit false, uNt 5]),
    (6, [uBit true, uNt 6]), (6, [uBit false, uNt 6]),
    (0, [uNt 3]), (0, [uNt 3, uBit false, uNt 5]), (0, uNt 6 :: (bitCode k).map uBit ++ [uNt 6]),
    (0, [uNt 1]), (0, [uNt 2])] ++
  allLetters.flatMap (fun a ↦ [(3, [uLetter a, uNt 3]), (4, [uLetter a, uNt 3]),
    (6, [uLetter a, uNt 6]), (0, [uNt 6, uBit true, uLetter a, uNt 6]),
    (0, [uNt 6, uBit false, uLetter a, uNt 6])]) ++
  (List.range k).map fun i ↦ (7, (bitCode i).map uBit ++ [uNt 7])
Uses 5 · Used by 5
Statement usesList of all letters · Unary code of an index · Encoded bit terminal · Encoded letter terminal · Encoded nonterminal
Used byThe intended languages form a valuation of the universality grammar · The language of the universality grammar · The complement of PCP many-one reduces to universality of context-free grammars · Every mismatched word is derivable from the mismatch nonterminal · The universality grammar

DefinitionThe mismatch productions#✓fully proved

The mismatch productions of a nonterminal \(A\) for one side of a list \(P\) of dominoes over a finite alphabet. Let \(s\) be a map from dominoes to words (in use, the top or the bottom). For each index \(i < |P|\) write \(w = s(d_i)\) for the \(i\)-th domino \(d_i\) of \(P\) and \(\mathrm{code}(i)\) for the unary code of \(i\) as bits. With letters and bits as terminals and \(N_3\), \(N_4\), \(N_7\) the nonterminals \(3\), \(4\), \(7\) (meant to generate words of letters, nonempty words of letters and codes of indices), the productions are \(A \to w\,A\,\mathrm{code}(i)\) and \(A \to w\,N_4\,\mathrm{code}(i)\), which peel \(w\) off, and, for each proper prefix \(u\) of \(w\), \(A \to u\,N_7\,\mathrm{code}(i)\) and \(A \to u\,a\,N_3\,N_7\,\mathrm{code}(i)\) for every letter \(a\) other than the letter of \(w\) following \(u\), which stop matching.

noncomputable def mismatchRules (side : Domino α → List α) (A : ℕ) (P : List (Domino α)) :
    List (ℕ × List (ℕ ⊕ (α ⊕ Bool))) :=
  (List.range P.length).flatMap fun i ↦
    (A, (side (domino P i)).map uLetter ++ uNt A :: (bitCode i).map uBit) ::
    (A, (side (domino P i)).map uLetter ++ uNt 4 :: (bitCode i).map uBit) ::
    (List.range (side (domino P i)).length).flatMap fun m ↦
      (A, ((side (domino P i)).take m).map uLetter ++ uNt 7 :: (bitCode i).map uBit) ::
      (((side (domino P i)).drop m).take 1).flatMap fun c ↦ (others c).map fun a ↦
        (A, ((side (domino P i)).take m).map uLetter ++
          uLetter a :: uNt 3 :: uNt 7 :: (bitCode i).map uBit)
Uses 7 · Used by 6
Statement usesUnary code of an index · The \(i\)-th domino of a list · The letters other than a given letter · Encoded bit terminal · Encoded letter terminal · Encoded nonterminal · Domino (Post correspondence problem)
Used byThe intended languages form a valuation of the universality grammar · The language 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 universality grammar

DefinitionThe universality grammar#✓fully proved

For a finite alphabet \(\alpha\) with decidable equality and a list \(P\) of dominoes over \(\alpha\), the encoded context-free grammar over \(\alpha \oplus \mathrm{Bool}\) with start nonterminal \(0\) whose productions are the base productions for \(k = |P|\), followed by the mismatch productions of the top words of \(P\) with nonterminal \(1\), followed by the mismatch productions of the bottom words of \(P\) with nonterminal \(2\).

Its language is the union of the complements of the top and bottom list languages of \(P\).

noncomputable def univGrammar (P : List (Domino α)) : EncodedCFG (α ⊕ Bool) :=
  ⟨0, baseRules P.length ++ mismatchRules Prod.fst 1 P ++ mismatchRules Prod.snd 2 P⟩
Uses 4 · Used by 5
Statement usesDomino-independent productions of the universality grammar · The mismatch productions · Domino (Post correspondence problem) · Encoded context-free grammars
Used byThe 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 · The complement of PCP many-one reduces to universality of context-free grammars · Every mismatched word is derivable from the mismatch nonterminal

The languages of the nonterminals

DefinitionWords of letters#✓fully proved

For an alphabet \(\alpha\), the language of words of letters is the set of all words over \(\alpha \oplus \mathrm{Bool}\) whose symbols all lie in \(\alpha\), that is, the words over \(\alpha\) (including the empty word) viewed as words over \(\alpha \oplus \mathrm{Bool}\).

def lettersLang : Language (α ⊕ Bool) := {w | ∃ x : List α, w = x.map Sum.inl}
Used by 1
Used byIntended languages of the nonterminals of the universality grammar

DefinitionNonempty words of letters#✓fully proved

For an alphabet \(\alpha\), the language of nonempty words of letters is the set of all nonempty words over \(\alpha \oplus \mathrm{Bool}\) whose symbols all lie in \(\alpha\), that is, the nonempty words over \(\alpha\) viewed as words over \(\alpha \oplus \mathrm{Bool}\).

def letters1Lang : Language (α ⊕ Bool) := {w | ∃ x : List α, x ≠ [] ∧ w = x.map Sum.inl}
Used by 1
Used byIntended languages of the nonterminals of the universality grammar

DefinitionWords of bits#✓fully proved

For an alphabet \(\alpha\), the language over the disjoint union of \(\alpha\) and the bits \(\{\mathbf{t}, \mathbf{f}\}\) consisting of the words in which every symbol is a bit, including the empty word.

def bitsLang : Language (α ⊕ Bool) := {w | ∃ y : List Bool, w = y.map Sum.inr}
Used by 1
Used byIntended languages of the nonterminals of the universality grammar

DefinitionCodes of index sequences below \(k\)#✓fully proved

For an alphabet \(\alpha\) and \(k \in \mathbb{N}\), the language over the disjoint union of \(\alpha\) and the bits \(\{\mathbf{t}, \mathbf{f}\}\) consisting of the bit words \(c(j_1) \cdots c(j_n)\) with \(n \ge 0\) and \(j_1, \dots, j_n < k\), where \(c(j) = \mathbf{t}\,\mathbf{f}^j\) is the unary code of \(j\). In particular it contains the empty word.

def codesLang (k : ℕ) : Language (α ⊕ Bool) :=
  {w | ∃ J : List ℕ, (∀ j ∈ J, j < k) ∧ w = (bitCodes J).map Sum.inr}
Uses 1 · Used by 1
Statement usesConcatenated code of an index sequence
Used byIntended languages of the nonterminals of the universality grammar

DefinitionThe mismatch language#✓fully proved

The mismatch language of one side of a list \(P\) of dominoes. Let \(s\) be a map from dominoes to words (in use, the top or the bottom), write \(w_i = s(d_i)\) for the \(i\)-th domino \(d_i\) of \(P\) and \(\mathrm{code}(i)\) for the unary code of \(i\) as bits. The language, over letters and bits, consists of the words \(x\,\mathrm{code}(i_n) \cdots \mathrm{code}(i_1)\) where \(x\) is a word of letters and \(i_1, \dots, i_n\) with \(n \ge 1\) are indices below \(|P|\) such that \(x \ne w_{i_1} \cdots w_{i_n}\).

def mismatchLang (side : Domino α → List α) (P : List (Domino α)) : Language (α ⊕ Bool) :=
  {w | ∃ (x : List α) (I : List ℕ), I ≠ [] ∧ (∀ i ∈ I, i < P.length) ∧ x ≠ flat side P I ∧
    w = x.map Sum.inl ++ (bitCodes I.reverse).map Sum.inr}
Uses 3 · Used by 5
Statement usesConcatenated code of an index sequence · The letter part of an index sequence · Domino (Post correspondence problem)
Used byThe 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 · Mismatched words are not in the list language · Intended languages of the nonterminals of the universality grammar

DefinitionMalformed words#✓fully proved

Consider words over \(\alpha \oplus \mathrm{Bool}\), whose symbols are letters from \(\alpha\) and bits, and read the bit \(\mathrm{true}\) as the separator \(|\) and the bit \(\mathrm{false}\) as \(1\). For \(k \in \mathbb{N}\), a word is malformed with bound \(k\) when at least one of the following holds: it consists of letters only (possibly none); it is a word of letters followed by a nonempty word of bits whose first bit is \(1\); some bit is immediately followed by a letter; or it contains the block \(|\,1^k\) (the bit \(|\) followed by \(k\) bits \(1\)) as a contiguous factor.

def malformedLang (k : ℕ) : Language (α ⊕ Bool) :=
  {w | (∃ x : List α, w = x.map Sum.inl) ∨
    (∃ (x : List α) (y : List Bool), w = x.map Sum.inl ++ Sum.inr false :: y.map Sum.inr) ∨
    (∃ (u v : List (α ⊕ Bool)) (b : Bool) (a : α), w = u ++ Sum.inr b :: Sum.inl a :: v) ∨
    (∃ u v : List (α ⊕ Bool), w = u ++ (bitCode k).map Sum.inr ++ v)}
Uses 1 · Used by 6
Statement usesUnary code of an index
Used byThe 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 · Every word is malformed or well formed · Malformed words are in no list language · Intended languages of the nonterminals of the universality grammar

DefinitionIntended languages of the nonterminals of the universality grammar#✓fully proved

For a list \(P\) of dominoes over \(\alpha\), the assignment of a language over \(\alpha \oplus \mathrm{Bool}\) to each natural number that sends \(0\) to the union of the malformed language for \(k = |P|\) and the mismatch languages of the top words and of the bottom words of \(P\); \(1\) to the mismatch language of the top words of \(P\); \(2\) to the mismatch language of the bottom words of \(P\); \(3\) to the words of letters; \(4\) to the nonempty words of letters; \(5\) to the words of bits; \(6\) to the set of all words; \(7\) to the codes of index sequences with all indices below \(|P|\); and every other number to the empty language.

def univVal (P : List (Domino α)) : ℕ → Language (α ⊕ Bool)
  | 0 => {w | w ∈ malformedLang P.length ∨ w ∈ mismatchLang Prod.fst P ∨
      w ∈ mismatchLang Prod.snd P}
  | 1 => mismatchLang Prod.fst P
  | 2 => mismatchLang Prod.snd P
  | 3 => lettersLang
  | 4 => letters1Lang
  | 5 => bitsLang
  | 6 => {_w | True}
  | 7 => codesLang P.length
  | _ => {_w | False}
Uses 7 · Used by 3
Statement usesWords of bits · Codes of index sequences below \(k\) · Nonempty words of letters · Words of letters · Malformed words · The mismatch language · Domino (Post correspondence problem)
Used byThe 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

TheoremEvaluating a form with one nonterminal#✓fully proved

Let \(V\) assign a language over \(T\) to each nonterminal. For terminal words \(u\) and \(v\), a nonterminal \(A\) and a word \(w\), the word \(w\) lies in the language that \(V\) assigns to the sentential form \(u\,A\,v\) if and only if \(w = u z v\) for some \(z \in V(A)\).

theorem mem_evalForm_one {T N : Type*} {V : N → Language T} {u v w : List T} {A : N} :
    w ∈ evalForm V (u.map Symbol.terminal ++ Symbol.nonterminal A :: v.map Symbol.terminal) ↔
      ∃ z ∈ V A, w = u ++ z ++ v
Uses 3 · Used by 3
Statement usesInterpretation of a sentential form
Proof usesInterpretation of a concatenation · A terminal word denotes its singleton
Used byThe intended languages form a valuation of the universality grammar · The language of the universality grammar · Every mismatched word is derivable from the mismatch nonterminal

TheoremEvaluating a form with two nonterminals#✓fully proved

Let \(V\) assign a language over \(T\) to each nonterminal. For terminal words \(u\), \(v\) and \(x\), nonterminals \(A\) and \(B\) and a word \(w\), the word \(w\) lies in the language that \(V\) assigns to the sentential form \(u\,A\,v\,B\,x\) if and only if \(w = u z_1 v z_2 x\) for some \(z_1 \in V(A)\) and \(z_2 \in V(B)\).

theorem mem_evalForm_two {T N : Type*} {V : N → Language T} {u v x w : List T} {A B : N} :
    w ∈ evalForm V (u.map Symbol.terminal ++ Symbol.nonterminal A ::
      (v.map Symbol.terminal ++ Symbol.nonterminal B :: x.map Symbol.terminal)) ↔
      ∃ z₁ ∈ V A, ∃ z₂ ∈ V B, w = u ++ z₁ ++ v ++ z₂ ++ x
Uses 3 · Used by 3
Statement usesInterpretation of a sentential form
Proof usesInterpretation of a concatenation · A terminal word denotes its singleton
Used byThe intended languages form a valuation of the universality grammar · The language of the universality grammar · Every mismatched word is derivable from the mismatch nonterminal

Upper bounds: every production is sound for the intended valuation

TheoremThe intended languages form a valuation of the universality grammar#✓fully proved

Let \(\alpha\) be a finite alphabet with decidable equality and let \(P\) be a list of dominoes over \(\alpha\). The assignment of intended languages to the nonterminals of the universality grammar of \(P\) is a valuation of that grammar: for every production \(A \to \gamma\), the language that \(\gamma\) denotes under the assignment is contained in the language assigned to \(A\).

theorem isValuation_univVal (P : List (Domino α)) :
    IsValuation (univGrammar P).toCFG (univVal P)
Uses 24 · Used by 1
Statement usesThe universality grammar · Intended languages of the nonterminals of the universality grammar · Domino (Post correspondence problem) · Grammar denoted by an encoding · Valuation of a grammar
Proof usesList of all letters · Domino-independent productions of the universality grammar · Unary code of an index · Concatenated code of an index sequence · The \(i\)-th domino of a list · The letter part of an index sequence · Malformed words · Evaluating a form with one nonterminal · Evaluating a form with two nonterminals · The mismatch language · The mismatch productions · The letters other than a given letter · Encoded bit terminal · Encoded letter terminal · Encoded nonterminal · Encoded context-free grammars · Decoding a production · Decoding a grammar symbol · Interpretation of a sentential form
Used byThe language of the universality grammar

Lower bounds: the intended words are derivable

TheoremA word that does not start with \(w\) leaves \(w\) at some position#✓fully proved

Let \(w\) and \(x\) be words over an alphabet \(\alpha\) such that \(w\) is not a prefix of \(x\). Then there is a position \(m < |w|\) with the following property: writing \(w = u\,c\,r\) with \(|u| = m\) and \(c \in \alpha\), either \(x = u\), or \(x = u\,a\,y\) for some letter \(a \ne c\) and some word \(y\).

theorem exists_mismatch_of_not_prefix {w x : List α} (h : ¬w <+: x) :
    ∃ m < w.length, ∃ c rest, w.drop m = c :: rest ∧
      (x = w.take m ∨ ∃ a y, a ≠ c ∧ x = w.take m ++ a :: y)
Used by 1
Used byEvery mismatched word is derivable from the mismatch nonterminal

TheoremMembership in the mismatch productions#✓fully proved

Let \(P\) be a list of dominoes over a finite alphabet with decidable equality, \(A\) a nonterminal, \(s\) a map from dominoes to words (in use, the top or the bottom), \(i < |P|\) an index, \(w = s(d_i)\) for the \(i\)-th domino \(d_i\) of \(P\), and \(\mathrm{code}(i)\) the unary code of \(i\) as bits. Write letters and bits as terminals and \(N_3\), \(N_4\), \(N_7\) for the nonterminals \(3\), \(4\) and \(7\). Each of the following encoded productions belongs to the mismatch productions of \(A\) for \(s\) and \(P\): \(A \to w\,A\,\mathrm{code}(i)\); \(A \to w\,N_4\,\mathrm{code}(i)\); for each \(m < |w|\), with \(u\) the prefix of \(w\) of length \(m\), \(A \to u\,N_7\,\mathrm{code}(i)\); and, for each such \(m\) and each letter \(a\) different from the letter of \(w\) following \(u\), \(A \to u\,a\,N_3\,N_7\,\mathrm{code}(i)\).

theorem mem_mismatchRules {side : Domino α → List α} {A i : ℕ} (hi : i < P.length)
    {e : ℕ × List (ℕ ⊕ (α ⊕ Bool))}
    (he : e = (A, (side (domino P i)).map uLetter ++ uNt A :: (bitCode i).map uBit) ∨
      e = (A, (side (domino P i)).map uLetter ++ uNt 4 :: (bitCode i).map uBit) ∨
      (∃ m < (side (domino P i)).length,
        e = (A, ((side (domino P i)).take m).map uLetter ++ uNt 7 :: (bitCode i).map uBit) ∨
        ∃ c ∈ ((side (domino P i)).drop m).take 1, ∃ a ∈ others c,
          e = (A, ((side (domino P i)).take m).map uLetter ++
            uLetter a :: uNt 3 :: uNt 7 :: (bitCode i).map uBit))) :
    e ∈ mismatchRules side A P
Uses 8 · Used by 1
Statement usesUnary code of an index · The \(i\)-th domino of a list · The mismatch productions · The letters other than a given letter · Encoded bit terminal · Encoded letter terminal · Encoded nonterminal · Domino (Post correspondence problem)
Used byEvery mismatched word is derivable from the mismatch nonterminal

TheoremEvery mismatched word is derivable from the mismatch nonterminal#✓fully proved

Let \(P\) be a list of dominoes over a finite alphabet, \(s\) a map from dominoes to words (in use, the top or the bottom), \(w_i = s(d_i)\) for the \(i\)-th domino \(d_i\) of \(P\), and \(\mathrm{code}(i)\) the unary code of \(i\) as bits. Let \(A\) be a nonterminal such that every mismatch production of \(A\) for \(s\) and \(P\) is a production of the universality grammar of \(P\). Then for every nonempty sequence \(i_1, \dots, i_n\) of indices below \(|P|\) and every word \(x\) of letters with \(x \ne w_{i_1} \cdots w_{i_n}\), the word \(x\,\mathrm{code}(i_n) \cdots \mathrm{code}(i_1)\) is derivable from \(A\) in the universality grammar of \(P\).

theorem mismatch_mem {side : Domino α → List α} {A : ℕ}
    (hrules : ∀ e ∈ mismatchRules side A P, e ∈ (univGrammar P).rules) :
    ∀ I : List ℕ, I ≠ [] → (∀ i ∈ I, i < P.length) → ∀ x : List α, x ≠ flat side P I →
      x.map Sum.inl ++ (bitCodes I.reverse).map Sum.inr ∈ languageFrom (univGrammar P).toCFG A
Uses 24 · Used by 1
Statement usesConcatenated code of an index sequence · The letter part of an index sequence · The mismatch productions · The universality grammar · Domino (Post correspondence problem) · Encoded context-free grammars · Grammar denoted by an encoding · Language generated from a nonterminal
Proof usesList of all letters · Domino-independent productions of the universality grammar · Unary code of an index · The \(i\)-th domino of a list · A word that does not start with \(w\) leaves \(w\) at some position · Evaluating a form with one nonterminal · Evaluating a form with two nonterminals · Membership in the mismatch productions · The letters other than a given letter · Encoded bit terminal · Encoded letter terminal · Encoded nonterminal · Decoding a production · Decoding a grammar symbol · Interpretation of a sentential form · The languages generated from each nonterminal form a valuation
Used byThe language of the universality grammar

TheoremThe language of the universality grammar#✓fully proved

Let \(\alpha\) be a finite alphabet with decidable equality, let \(P\) be a list of dominoes over \(\alpha\) of length \(m\), and for \(i < m\) let \(t_i\) and \(b_i\) be the top and bottom words of the domino of \(P\) at position \(i\), counting from \(0\). Read the bit \(\mathrm{true}\) as the separator \(|\) and the bit \(\mathrm{false}\) as \(1\), and let \(c(i)\) be the unary code of \(i\): the bit \(|\) followed by \(i\) bits \(1\). The language of the universality grammar of \(P\) equals the intended language of its start nonterminal \(0\): a word over \(\alpha \oplus \mathrm{Bool}\) belongs to it exactly when at least one of the following holds: it consists of letters from \(\alpha\) only (possibly none); it is a word of letters followed by a nonempty word of bits whose first bit is \(1\); some bit is immediately followed by a letter; it contains \(c(m)\) as a contiguous factor; or it equals \(x\, c(i_n) \cdots c(i_1)\) for a word \(x\) over \(\alpha\) and indices \(i_1, \dots, i_n < m\) with \(n \ge 1\) such that \(x \ne t_{i_1} \cdots t_{i_n}\) or \(x \ne b_{i_1} \cdots b_{i_n}\).

theorem language_univGrammar (P : List (Domino α)) :
    (univGrammar P).language = univVal P 0
Uses 27 · Used by 1
Statement usesThe universality grammar · Intended languages of the nonterminals of the universality grammar · Domino (Post correspondence problem) · Language of an encoded grammar
Proof usesList of all letters · Domino-independent productions of the universality grammar · Unary code of an index · Concatenated code of an index sequence · The letter part of an index sequence · The intended languages form a valuation of the universality grammar · Malformed words · Evaluating a form with one nonterminal · Evaluating a form with two nonterminals · The mismatch language · The mismatch productions · Every mismatched word is derivable from the mismatch nonterminal · Encoded bit terminal · Encoded letter terminal · Encoded nonterminal · Encoded context-free grammars · Decoding a production · Decoding a grammar symbol · Grammar denoted by an encoding · Interpretation of a sentential form · The languages generated from each nonterminal form a valuation · Language generated from a nonterminal · Valuations bound the language of a grammar
Used byThe universality grammar generates every word exactly when PCP has no solution

The language is the complement of the intersection of the list languages

TheoremNo right symbol directly precedes a left symbol in a left-then-right word#✓fully proved

Let \(\alpha\) and \(\beta\) be types and consider words over the disjoint union \(\alpha \sqcup \beta\). For all words \(u, v\) over \(\alpha \sqcup \beta\), all \(b \in \beta\) and \(a \in \alpha\), all words \(X\) over \(\alpha\) and all words \(Y\) over \(\beta\), we have \(u\,b\,a\,v \ne X\,Y\): a word over \(\alpha\) followed by a word over \(\beta\) never has a symbol of \(\beta\) immediately followed by a symbol of \(\alpha\).

theorem append_inr_inl_ne {β : Type*} (u v : List (α ⊕ β)) (b : β) (a : α) :
    ∀ (X : List α) (Y : List β),
      u ++ Sum.inr b :: Sum.inl a :: v ≠ X.map Sum.inl ++ Y.map Sum.inr
Used by 1
Used byMalformed words are in no list language

TheoremA bit inside a word of letters followed by bits starts a suffix of the bits#✓fully proved

Let \(\alpha\) and \(\beta\) be types, call the elements of \(\alpha\) letters and those of \(\beta\) bits, and regard words over \(\alpha\) and over \(\beta\) as words over the disjoint union \(\alpha \oplus \beta\). If \(u\,b\,z = X\,Y\) for words \(u, z\) over \(\alpha \oplus \beta\), a bit \(b\), a word \(X\) of letters and a word \(Y\) of bits, then there are words \(Y_1, Y_2\) of bits with \(Y = Y_1 Y_2\) and \(b\,z = Y_2\).

theorem exists_suffix_of_inr {β : Type*} {u z : List (α ⊕ β)} {b : β} :
    ∀ {X : List α} {Y : List β}, u ++ Sum.inr b :: z = X.map Sum.inl ++ Y.map Sum.inr →
      ∃ Y₁ Y₂, Y = Y₁ ++ Y₂ ∧ Sum.inr b :: z = Y₂.map Sum.inr
Used by 1
Used byMalformed words are in no list language

TheoremCodes of indices below \(k\) contain no code of \(k\)#✓fully proved

Let \(k \in \mathbb{N}\) and let \(J = (j_1, \dots, j_n)\) be a finite sequence of natural numbers with \(j_1, \dots, j_n < k\). Write \(c(i) = \mathbf{t}\,\mathbf{f}^i\) for the unary code of \(i\) and \(c(J) = c(j_1) \cdots c(j_n)\). Then there are no bit words \(Y\) and \(Z\) with \(c(J) = Y\,c(k)\,Z\).

theorem bitCodes_ne_append_bitCode {k : ℕ} :
    ∀ {J : List ℕ}, (∀ j ∈ J, j < k) → ∀ Y Z : List Bool, bitCodes J ≠ Y ++ bitCode k ++ Z
Uses 2 · Used by 1
Statement usesUnary code of an index · Concatenated code of an index sequence
Used byMalformed words are in no list language

TheoremMalformed words are in no list language#✓fully proved

Let \(P\) be a list of dominoes and \(s\) a map from dominoes to words (in use, the top or the bottom). Write the code of an index \(i\) as the bits \(|\,1^i\), where \(|\) stands for the bit true and \(1\) for the bit false. A word over letters and bits that is malformed with respect to \(|P|\) (it has no bits, its first bit is a \(1\), a bit is followed by a letter, or it contains the factor \(|\,1^{|P|}\)) does not belong to the list language of \(s\) for \(P\).

theorem not_mem_listLang_of_malformed {side : Domino α → List α} {P : List (Domino α)}
    {w : List (α ⊕ Bool)} (hw : w ∈ malformedLang P.length) : w ∉ listLang side P
Uses 11 · Used by 1
Statement usesList language of a PCP instance · Malformed words · Domino (Post correspondence problem)
Proof usesNo right symbol directly precedes a left symbol in a left-then-right word · Unary code of an index · Concatenated code of an index sequence · Codes of indices below \(k\) contain no code of \(k\) · Unique splitting of letters followed by markers · A bit inside a word of letters followed by bits starts a suffix of the bits · The letter part of an index sequence · List word of an index sequence
Used byThe universality grammar generates every word exactly when PCP has no solution

TheoremMismatched words are not in the list language#✓fully proved

Let \(P\) be a list of dominoes and \(s\) a map from dominoes to words (in use, the top or the bottom). No word of the mismatch language of \(s\) for \(P\) belongs to the list language of \(s\) for \(P\).

theorem not_mem_listLang_of_mismatch {side : Domino α → List α} {P : List (Domino α)}
    {w : List (α ⊕ Bool)} (hw : w ∈ mismatchLang side P) : w ∉ listLang side P
Uses 8 · Used by 1
Statement usesList language of a PCP instance · The mismatch language · Domino (Post correspondence problem)
Proof usesConcatenated code of an index sequence · Concatenated index codes are uniquely decodable · Unique splitting of letters followed by markers · The letter part of an index sequence · List word of an index sequence
Used byThe universality grammar generates every word exactly when PCP has no solution

TheoremEvery word is malformed or well formed#✓fully proved

Let \(k \in \mathbb{N}\) and let \(w\) be a word over \(\alpha \oplus \mathrm{Bool}\). Then \(w\) is malformed with bound \(k\), or \(w = x\, c(j_1) \cdots c(j_n)\) for a word \(x\) over \(\alpha\) and a nonempty sequence of indices \(j_1, \dots, j_n < k\), where \(c(j)\) is the unary code of \(j\): the bit \(\mathrm{true}\) followed by \(j\) bits \(\mathrm{false}\).

theorem malformed_or_wellFormed (k : ℕ) (w : List (α ⊕ Bool)) :
    w ∈ malformedLang k ∨ ∃ (x : List α) (J : List ℕ), J ≠ [] ∧ (∀ j ∈ J, j < k) ∧
      w = x.map Sum.inl ++ (bitCodes J).map Sum.inr
Uses 3 · Used by 1
Statement usesConcatenated code of an index sequence · Malformed words
Proof usesUnary code of an index
Used byThe universality grammar generates every word exactly when PCP has no solution

TheoremThe universality grammar generates every word exactly when PCP has no solution#✓fully proved

Let \(\alpha\) be a finite alphabet with decidable equality and let \(P\) be a list of dominoes over \(\alpha\). The universality grammar of \(P\) generates every word over \(\alpha \oplus \mathrm{Bool}\) if and only if the Post correspondence problem \(P\) has no solution.

theorem forall_mem_language_univGrammar_iff [Fintype α] [DecidableEq α] (P : List (Domino α)) :
    (∀ w, w ∈ (univGrammar P).language) ↔ ¬PCP P
Uses 16 · Used by 1
Statement usesThe universality grammar · Domino (Post correspondence problem) · The Post correspondence problem · Language of an encoded grammar
Proof usesConcatenated code of an index sequence · The letter part of an index sequence · The language of the universality grammar · List language of a PCP instance · List word of an index sequence · Malformed words · Every word is malformed or well formed · The mismatch language · 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 · Intended languages of the nonterminals of the universality grammar
Used byThe complement of PCP many-one reduces to universality of context-free grammars

The many-one reduction

TheoremThe complement of PCP many-one reduces to universality of context-free grammars#✓fully proved

Let \(\alpha\) be a finite alphabet with decidable equality and a primitive recursive encoding. There is a computable map sending each PCP instance \(P\) (a list of dominoes over \(\alpha\)) to an encoded context-free grammar \(G_P\) over the alphabet \(\alpha \oplus \mathrm{Bool}\) (the letters of \(\alpha\) together with two bits) such that \(P\) has no PCP solution if and only if \(G_P\) generates every word over \(\alpha \oplus \mathrm{Bool}\).

theorem manyOneReducible_not_pcp_univ [Finite α] :
    ManyOneReducible (fun P : List (Domino α) ↦ ¬PCP P) fun g : EncodedCFG (α ⊕ Bool) ↦
      ∀ w, w ∈ g.language
Uses 16 · Used by 2
Statement usesDomino (Post correspondence problem) · The Post correspondence problem · Encoded context-free grammars · Encoded grammars as pairs · Language of an encoded grammar
Proof usesList of all letters · Domino-independent productions of the universality grammar · Unary code of an index · The \(i\)-th domino of a list · The universality grammar generates every word exactly when PCP has no solution · The mismatch productions · The letters other than a given letter · Encoded bit terminal · Encoded letter terminal · Encoded nonterminal · The universality grammar
Used byWhether a context-free grammar generates every word is undecidable · Universality of context-free grammars is not recognizable

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.