Post correspondence problem

AbbreviationDomino (Post correspondence problem)#✓fully proved

A domino over an alphabet \(\alpha\) is a pair \((t, b)\) of words over \(\alpha\): its top word \(t\) and its bottom word \(b\).

abbrev Domino (α : Type*) := List α × List α
Used by 101
Used byDomino named by a one-letter block · Alphabet for the PCP encoding · Bottom morphism of the PCP encoding · Domino as an index letter · Regular language of domino index words · Bottom morphism applied to an index word · Top morphism applied to an index word · Flattening a list of one-letter blocks · Membership in the domino index-word language · PCP encoding as a one-variable string constraint · PCP is characterized by string-constraint satisfiability: · Membership atom of the PCP encoding checks index words · Top morphism of the PCP encoding · The ambiguity grammar of a PCP instance · The 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 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 · The continuation production · The construction of derivations · The \(i\)-th domino of a list · 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 · 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 productions of a side grammar · The side word of an index sequence · The terminating production of a side grammar · Bottom word of a domino sequence · PCP over a one-letter alphabet is decidable · End domino of the MPCP-to-PCP reduction · MPCP is undecidable · The Post correspondence problem is undecidable · PCP solution · Boolean check for PCP solutions · Total length of dominoes that are at least as long on top · Total length of dominoes that are strictly longer on top · MPCP many-one reduces to PCP · PCP over a finite alphabet many-one reduces to PCP over the binary alphabet · Starred image of a domino · Image of a PCP instance under a word map · The modified Post correspondence problem · MPCP reduces to PCP on instances with nonempty words · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · Instances with nonempty words · Boolean test for nonempty words · The Post correspondence problem is undecidable over the binary alphabet · The Post correspondence problem · The unary PCP criterion · An injective word homomorphism preserves and reflects PCP solvability · An MPCP solution gives a PCP solution of the reduced instance · The nonempty-words test is primitive recursive · PCP is recursively enumerable · The total reduction from MPCP to PCP · The start domino of the MPCP-to-PCP reduction · Swapping top and bottom · Unary PCP is decidable by a multi-stack machine · PCP is Turing-recognizable · The reduction from MPCP to PCP · Top word of a sequence of dominoes · The unary PCP test · Erasing the markers from a domino · Copy domino · The backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Final domino · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability for rules with nonempty sides many-one reduces to PCP · The total reduction of reachability with nonempty sides to MPCP · The domino of a rewriting rule · The separator domino · Reachability reduces to MPCP · The start domino of the reduction from reachability to MPCP · The MPCP instance of a reachability instance · Whether a context-free grammar is ambiguous is undecidable · Whether two context-free languages intersect is undecidable · Whether a context-free grammar generates every word is undecidable · The complement of PCP is not recognizable · Universality of context-free grammars is not recognizable · 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 language of a PCP instance · List word of an index sequence · The complement of PCP many-one reduces to universality of context-free grammars · Membership in the mismatch productions · The mismatch language · Every mismatched word is derivable from the mismatch nonterminal · The mismatch productions · 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 · The universality grammar · Intended languages of the nonterminals of the universality grammar

DefinitionTop word of a sequence of dominoes#✓fully proved

For a sequence of dominoes \((t_1, b_1), \ldots, (t_n, b_n)\), its top word is the concatenation \(t_1 t_2 \cdots t_n\) of their top words; the empty sequence has the empty top word.

def top (s : List (Domino α)) : List α := s.flatMap Prod.fst
Uses 1 · Used by 17
Statement usesDomino (Post correspondence problem)
Used byTop morphism applied to an index word · PCP is characterized by string-constraint satisfiability: · A PCP instance is solvable exactly when its top and bottom grammars share a word · PCP solution · Boolean check for PCP solutions · Total length of dominoes that are at least as long on top · Total length of dominoes that are strictly longer on top · MPCP many-one reduces to PCP · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · The unary PCP criterion · An injective word homomorphism preserves and reflects PCP solvability · An MPCP solution gives a PCP solution of the reduced instance · PCP is recursively enumerable · The backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Reachability reduces to MPCP · A PCP instance is solvable exactly when its top and bottom list languages meet

DefinitionBottom word of a domino sequence#✓fully proved

For a sequence \(s = d_1, \dots, d_k\) of dominoes, the bottom word of \(s\) is the concatenation \(b_1 b_2 \cdots b_k\), where \(b_i\) is the bottom word of \(d_i\).

def bottom (s : List (Domino α)) : List α := s.flatMap Prod.snd
Uses 1 · Used by 17
Statement usesDomino (Post correspondence problem)
Used byBottom morphism applied to an index word · PCP is characterized by string-constraint satisfiability: · A PCP instance is solvable exactly when its top and bottom grammars share a word · PCP solution · Boolean check for PCP solutions · Total length of dominoes that are at least as long on top · Total length of dominoes that are strictly longer on top · MPCP many-one reduces to PCP · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · The unary PCP criterion · An injective word homomorphism preserves and reflects PCP solvability · An MPCP solution gives a PCP solution of the reduced instance · PCP is recursively enumerable · The backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Reachability reduces to MPCP · A PCP instance is solvable exactly when its top and bottom list languages meet

DefinitionPCP solution#✓fully proved

Let \(P\) be a finite list of dominoes. A solution of \(P\) is a nonempty sequence \(d_1, \dots, d_k\) of dominoes, each occurring in \(P\) (repetitions allowed), such that the concatenation of the top words of \(d_1, \dots, d_k\) equals the concatenation of their bottom words.

def IsSolution (P : List (Domino α)) (s : List (Domino α)) : Prop :=
  s ≠ [] ∧ (∀ d ∈ s, d ∈ P) ∧ top s = bottom s
Uses 3 · Used by 13
Statement usesDomino (Post correspondence problem) · Bottom word of a domino sequence · Top word of a sequence of dominoes
Used byPCP is characterized by string-constraint satisfiability: · A PCP instance is solvable exactly when its top and bottom grammars share a word · MPCP many-one reduces to PCP · The modified Post correspondence problem · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · The Post correspondence problem · The unary PCP criterion · An injective word homomorphism preserves and reflects PCP solvability · An MPCP solution gives a PCP solution of the reduced instance · PCP is recursively enumerable · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability reduces to MPCP · A PCP instance is solvable exactly when its top and bottom list languages meet

DefinitionThe Post correspondence problem#✓fully proved

A list \(P\) of dominoes is a solvable instance of the Post correspondence problem when it has a PCP solution: a nonempty sequence of dominoes from \(P\), repetitions allowed, whose top words and bottom words concatenate to the same word.

def PCP (P : List (Domino α)) : Prop := ∃ s, IsSolution P s
Uses 2 · Used by 27
Statement usesDomino (Post correspondence problem) · PCP solution
Used byPCP is characterized by string-constraint satisfiability: · The ambiguity grammar of \(P\) is ambiguous exactly when \(P\) has a solution · PCP many-one reduces to ambiguity of context-free grammars · 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 · PCP over a one-letter alphabet is decidable · The Post correspondence problem is undecidable · MPCP many-one reduces to PCP · PCP over a finite alphabet many-one reduces to PCP over the binary alphabet · MPCP reduces to PCP on instances with nonempty words · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · The Post correspondence problem is undecidable over the binary alphabet · The unary PCP criterion · An injective word homomorphism preserves and reflects PCP solvability · An MPCP solution gives a PCP solution of the reduced instance · PCP is recursively enumerable · Unary PCP is decidable by a multi-stack machine · PCP is Turing-recognizable · Reachability for rules with nonempty sides many-one reduces to PCP · Whether a context-free grammar is ambiguous is undecidable · Whether two context-free languages intersect is undecidable · Whether a context-free grammar generates every word is undecidable · The complement of PCP is not recognizable · Universality of context-free grammars is not recognizable · The universality grammar generates every word exactly when PCP has no solution · The complement of PCP many-one reduces to universality of context-free grammars · A PCP instance is solvable exactly when its top and bottom list languages meet

DefinitionThe modified Post correspondence problem#✓fully proved

A list \(P\) of dominoes has an MPCP solution when \(P\) is nonempty and some PCP solution of \(P\) starts with the first domino of \(P\).

def MPCP (P : List (Domino α)) : Prop :=
  ∃ d₀ s, P.head? = some d₀ ∧ IsSolution P (d₀ :: s)
Uses 2 · Used by 8
Statement usesDomino (Post correspondence problem) · PCP solution
Used byMPCP is undecidable · MPCP many-one reduces to PCP · MPCP reduces to PCP on instances with nonempty words · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · An MPCP solution gives a PCP solution of the reduced instance · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability for rules with nonempty sides many-one reduces to PCP · Reachability reduces to MPCP

DefinitionInstances with nonempty words#✓fully proved

A list \(P\) of dominoes has nonempty words when every domino of \(P\) has a nonempty top word and a nonempty bottom word.

def NonemptyWords (P : List (Domino α)) : Prop := ∀ d ∈ P, d.1 ≠ [] ∧ d.2 ≠ []
Uses 1 · Used by 6
Statement usesDomino (Post correspondence problem)
Used byMPCP is undecidable · MPCP many-one reduces to PCP · MPCP reduces to PCP on instances with nonempty words · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability for rules with nonempty sides many-one reduces to PCP

AbbreviationThe extended alphabet of the MPCP-to-PCP reduction#✓fully proved

For an alphabet \(\alpha\), the extended alphabet consists of the letters of \(\alpha\) together with two new symbols: the star \(\star\) and the end marker \(\diamond\).

It is represented so that it has a primitive recursive encoding whenever \(\alpha\) has one.

abbrev Sym (α : Type*) := Option (Option α)
Used by 33
Used byEnd domino of the MPCP-to-PCP reduction · End marker · MPCP is undecidable · The Post correspondence problem is undecidable · The alphabet inside the extended alphabet · Erasing stars and end markers · MPCP many-one reduces to PCP · Starred image of a domino · MPCP reduces to PCP on instances with nonempty words · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · An MPCP solution gives a PCP solution of the reduced instance · The total reduction from MPCP to PCP · The star symbol · A star after every letter · A star before every letter · The start domino of the MPCP-to-PCP reduction · The reduction from MPCP to PCP · Erasing the markers from a domino · Copy domino · The backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Comparing words of letters before a separator · Final domino · Letters differ from the star · Lifting a word to the extended alphabet · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability for rules with nonempty sides many-one reduces to PCP · The total reduction of reachability with nonempty sides to MPCP · The domino of a rewriting rule · The separator domino · Reachability reduces to MPCP · The start domino of the reduction from reachability to MPCP · The MPCP instance of a reachability instance

AbbreviationThe alphabet inside the extended alphabet#✓fully proved

Each letter \(a\) of the alphabet \(\alpha\) is regarded as a symbol of the extended alphabet of the MPCP-to-PCP reduction, which consists of the letters of \(\alpha\), the star \(\star\) and the end marker \(\diamond\).

abbrev letter (a : α) : Sym α := some (some a)
Uses 1 · Used by 13
Statement usesThe extended alphabet of the MPCP-to-PCP reduction
Used byMPCP many-one reduces to PCP · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · An MPCP solution gives a PCP solution of the reduced instance · A star after every letter · A star before every letter · Copy domino · The backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Comparing words of letters before a separator · Letters differ from the star · Lifting a word to the extended alphabet · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability reduces to MPCP

AbbreviationThe star symbol#✓fully proved

The star \(\star\) is the new symbol of the extended alphabet that is neither a letter of \(\alpha\) nor the end marker \(\diamond\).

abbrev star : Sym α := some none
Uses 1 · Used by 16
Statement usesThe extended alphabet of the MPCP-to-PCP reduction
Used byEnd domino of the MPCP-to-PCP reduction · MPCP many-one reduces to PCP · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · An MPCP solution gives a PCP solution of the reduced instance · A star after every letter · A star before every letter · The start domino of the MPCP-to-PCP reduction · The backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Comparing words of letters before a separator · Final domino · Letters differ from the star · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · The separator domino · Reachability reduces to MPCP · The start domino of the reduction from reachability to MPCP

AbbreviationEnd marker#✓fully proved

The end marker \(\diamond\) is the symbol of the extended alphabet of the MPCP-to-PCP reduction that is neither a letter of \(\alpha\) nor the star \(\star\).

abbrev endMark : Sym α := none
Uses 1 · Used by 9
Statement usesThe extended alphabet of the MPCP-to-PCP reduction
Used byEnd domino of the MPCP-to-PCP reduction · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · An MPCP solution gives a PCP solution of the reduced instance · The backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Final domino · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability reduces to MPCP · The start domino of the reduction from reachability to MPCP

DefinitionA star before every letter#✓fully proved

Let \(\star\) be the star of the extended alphabet. For a word \(u = a_1 a_2 \cdots a_n\) over \(\alpha\), the word \(\star u\) over the extended alphabet is \(\star a_1 \star a_2 \cdots \star a_n\), obtained by putting a star before every letter of \(u\); the empty word gives the empty word.

def starBefore (u : List α) : List (Sym α) := u.flatMap fun a ↦ [star, letter a]
Uses 3 · Used by 5
Statement usesThe extended alphabet of the MPCP-to-PCP reduction · The alphabet inside the extended alphabet · The star symbol
Used byMPCP many-one reduces to PCP · Starred image of a domino · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · An MPCP solution gives a PCP solution of the reduced instance · The start domino of the MPCP-to-PCP reduction

DefinitionA star after every letter#✓fully proved

Let \(\star\) be the star of the extended alphabet. For a word \(u = a_1 a_2 \cdots a_n\) over \(\alpha\), the word \(u\star\) over the extended alphabet is \(a_1 \star a_2 \star \cdots a_n \star\), obtained by putting a star after every letter of \(u\); the empty word gives the empty word.

def starAfter (u : List α) : List (Sym α) := u.flatMap fun a ↦ [letter a, star]
Uses 3 · Used by 5
Statement usesThe extended alphabet of the MPCP-to-PCP reduction · The alphabet inside the extended alphabet · The star symbol
Used byMPCP many-one reduces to PCP · Starred image of a domino · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · An MPCP solution gives a PCP solution of the reduced instance · The start domino of the MPCP-to-PCP reduction

DefinitionErasing stars and end markers#✓fully proved

For a word \(w\) over the extended alphabet of the MPCP-to-PCP reduction, this is the word over \(\alpha\) obtained from \(w\) by deleting every star \(\star\) and every end marker \(\diamond\), keeping the letters of \(\alpha\) in their order.

def letters (w : List (Sym α)) : List α := w.filterMap fun x ↦ x.bind id
Uses 1 · Used by 2
Statement usesThe extended alphabet of the MPCP-to-PCP reduction
Used byOn instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · Erasing the markers from a domino

DefinitionStarred image of a domino#✓fully proved

For a word \(u\) over \(\alpha\), write \(\star u\) for the word over the extended alphabet obtained by putting a star \(\star\) before every letter of \(u\), and \(u\star\) for the word obtained by putting a star after every letter. A domino \((t, b)\) over \(\alpha\) is sent to the domino \((\star t, b\star)\) over the extended alphabet.

def mapDomino (d : Domino α) : Domino (Sym α) := (starBefore d.1, starAfter d.2)
Uses 4 · Used by 4
Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · A star after every letter · A star before every letter
Used byMPCP many-one reduces to PCP · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · An MPCP solution gives a PCP solution of the reduced instance · The reduction from MPCP to PCP

DefinitionThe start domino of the MPCP-to-PCP reduction#✓fully proved

For a domino \((t, b)\) over an alphabet \(\alpha\), its start domino is the domino \((\star t, \star b \star)\) over the extended alphabet, where \(\star t\) puts the star \(\star\) before every letter of \(t\) and \(b \star\) puts a star after every letter of \(b\), so that the bottom word gets one extra star in front.

def startDomino (d : Domino α) : Domino (Sym α) := (starBefore d.1, star :: starAfter d.2)
Uses 5 · Used by 4
Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · The star symbol · A star after every letter · A star before every letter
Used byMPCP many-one reduces to PCP · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · An MPCP solution gives a PCP solution of the reduced instance · The reduction from MPCP to PCP

DefinitionEnd domino of the MPCP-to-PCP reduction#✓fully proved

Over the alphabet \(\alpha\) extended with the star \(\star\) and the end marker \(\diamond\), the end domino is \((\star\diamond, \diamond)\): its top word is \(\star\) followed by \(\diamond\), and its bottom word is \(\diamond\).

def endDomino : Domino (Sym α) := ([star, endMark], [endMark])
Uses 4 · Used by 4
Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · End marker · The star symbol
Used byMPCP many-one reduces to PCP · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · An MPCP solution gives a PCP solution of the reduced instance · The reduction from MPCP to PCP

DefinitionThe reduction from MPCP to PCP#✓fully proved

Write \(\star\) for the star and \(\diamond\) for the end marker of the extended alphabet; for a word \(u\) over \(\alpha\), \(\star u\) puts a star before every letter of \(u\) and \(u \star\) puts a star after every letter of \(u\). The empty list of dominoes is sent to the empty list. A list \(P = [d_0, d_1, \ldots, d_n]\) of dominoes over \(\alpha\), with \(d_0 = (t_0, b_0)\), is sent to the following list of dominoes over the extended alphabet: first the start domino \((\star t_0, \star b_0 \star)\), then the domino \((\star t, b \star)\) for each domino \((t, b)\) of \(P\) in order (including \(d_0\)), and last the end domino \((\star \diamond, \diamond)\), whose top word is a star followed by the end marker.

def toPCP : List (Domino α) → List (Domino (Sym α))
  | [] => []
  | d₀ :: P => startDomino d₀ :: ((d₀ :: P).map mapDomino ++ [endDomino])
Uses 5 · Used by 5
Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · End domino of the MPCP-to-PCP reduction · Starred image of a domino · The start domino of the MPCP-to-PCP reduction
Used byMPCP many-one reduces to PCP · MPCP reduces to PCP on instances with nonempty words · On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · An MPCP solution gives a PCP solution of the reduced instance · The total reduction from MPCP to PCP

DefinitionErasing the markers from a domino#✓fully proved

For a domino \((t, b)\) over the extended alphabet, its unmapping is the domino over \(\alpha\) obtained by deleting every star \(\star\) and every end marker \(\diamond\) from both \(t\) and \(b\), keeping the letters of \(\alpha\) in order.

It reads a domino of the reduced PCP instance back as a domino over \(\alpha\).

def unmap (d : Domino (Sym α)) : Domino α := (letters d.1, letters d.2)
Uses 3 · Used by 1
Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · Erasing stars and end markers
Used byOn instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution

TheoremAn MPCP solution gives a PCP solution of the reduced instance#✓fully proved

If a list \(P\) of dominoes has an MPCP solution, then the image of \(P\) under the reduction from MPCP to PCP has a PCP solution.

theorem pcp_toPCP_of_mpcp {P : List (Domino α)} (h : MPCP P) : PCP (toPCP P)
Uses 16 · Used by 1
Statement usesDomino (Post correspondence problem) · The modified Post correspondence problem · The Post correspondence problem · The extended alphabet of the MPCP-to-PCP reduction · The reduction from MPCP to PCP
Proof usesPCP solution · Bottom word of a domino sequence · End domino of the MPCP-to-PCP reduction · End marker · The alphabet inside the extended alphabet · Starred image of a domino · The star symbol · A star after every letter · A star before every letter · The start domino of the MPCP-to-PCP reduction · Top word of a sequence of dominoes
Used byMPCP reduces to PCP on instances with nonempty words

TheoremOn instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution#✓fully proved

On instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution. Let \(P\) be a list of dominoes in which every domino has a nonempty top and a nonempty bottom. If the image of \(P\) under the reduction from MPCP to PCP has a PCP solution, then \(P\) has an MPCP solution.

theorem mpcp_of_pcp_toPCP {P : List (Domino α)} (hP : NonemptyWords P) (h : PCP (toPCP P)) :
    MPCP P
Uses 19 · Used by 1
Statement usesDomino (Post correspondence problem) · The modified Post correspondence problem · Instances with nonempty words · The Post correspondence problem · The extended alphabet of the MPCP-to-PCP reduction · The reduction from MPCP to PCP
Proof usesPCP solution · Bottom word of a domino sequence · End domino of the MPCP-to-PCP reduction · End marker · The alphabet inside the extended alphabet · Erasing stars and end markers · Starred image of a domino · The star symbol · A star after every letter · A star before every letter · The start domino of the MPCP-to-PCP reduction · Top word of a sequence of dominoes · Erasing the markers from a domino
Used byMPCP reduces to PCP on instances with nonempty words

TheoremMPCP reduces to PCP on instances with nonempty words#✓fully proved

Let \(P\) be a list of dominoes over an alphabet \(\alpha\) in which every domino has a nonempty top and a nonempty bottom. Then \(P\) has an MPCP solution if and only if the image of \(P\) under the reduction from MPCP to PCP, an instance over \(\alpha\) extended with a star and an end marker, has a PCP solution.

theorem mpcp_iff_pcp_toPCP {P : List (Domino α)} (hP : NonemptyWords P) :
    MPCP P ↔ PCP (toPCP P)
Uses 8 · Used by 1
Statement usesDomino (Post correspondence problem) · The modified Post correspondence problem · Instances with nonempty words · The Post correspondence problem · The extended alphabet of the MPCP-to-PCP reduction · The reduction from MPCP to PCP
Proof usesOn instances with nonempty words, a PCP solution of the reduced instance gives an MPCP solution · An MPCP solution gives a PCP solution of the reduced instance
Used byMPCP many-one reduces to PCP

DefinitionBoolean test for nonempty words#✓fully proved

For a list \(P\) of dominoes, this Boolean test returns true exactly when every domino of \(P\) has a nonempty top and a nonempty bottom.

def nonemptyWordsB (P : List (Domino α)) : Bool := P.all fun d ↦ !d.1.isEmpty && !d.2.isEmpty
Uses 1 · Used by 5
Statement usesDomino (Post correspondence problem)
Used byMPCP many-one reduces to PCP · The nonempty-words test is primitive recursive · The total reduction from MPCP to PCP · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · The total reduction of reachability with nonempty sides to MPCP

DefinitionThe total reduction from MPCP to PCP#✓fully proved

For a list \(P\) of dominoes, the total reduction sends \(P\) to its image under the reduction from MPCP to PCP when every domino of \(P\) has a nonempty top and a nonempty bottom, and to the empty instance, which has no PCP solution, otherwise.

def reduce (P : List (Domino α)) : List (Domino (Sym α)) :=
  cond (nonemptyWordsB P) (toPCP P) []
Uses 4 · Used by 1
Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · Boolean test for nonempty words · The reduction from MPCP to PCP
Used byMPCP many-one reduces to PCP

TheoremThe nonempty-words test is primitive recursive#✓fully proved

For an alphabet \(\alpha\) with a primitive recursive coding, the Boolean test of whether every domino of a list over \(\alpha\) has a nonempty top and a nonempty bottom is a primitive recursive function of the list.

theorem primrec_nonemptyWordsB : Primrec (nonemptyWordsB (α := α))
Uses 2 · Used by 2
Statement usesDomino (Post correspondence problem) · Boolean test for nonempty words
Used byMPCP many-one reduces to PCP · Reachability with nonempty sides many-one reduces to MPCP with nonempty words

TheoremMPCP many-one reduces to PCP#✓fully proved

Let \(\alpha\) be an alphabet with a primitive recursive coding, and let \(\alpha'\) be \(\alpha\) extended with two new symbols, the star and the end marker. There is a computable function \(f\) from finite lists of dominoes over \(\alpha\) to finite lists of dominoes over \(\alpha'\) such that, for every list \(P\) of dominoes over \(\alpha\), \(f(P)\) has a PCP solution if and only if both every domino of \(P\) has a nonempty top word and a nonempty bottom word, and \(P\) has an MPCP solution.

theorem manyOneReducible_mpcp_pcp :
    ManyOneReducible (fun P : List (Domino α) ↦ NonemptyWords P ∧ MPCP P)
      (PCP (α := Sym α))
Uses 20 · Used by 1
Statement usesDomino (Post correspondence problem) · The modified Post correspondence problem · Instances with nonempty words · The Post correspondence problem · The extended alphabet of the MPCP-to-PCP reduction
Proof usesPCP solution · Bottom word of a domino sequence · End domino of the MPCP-to-PCP reduction · The alphabet inside the extended alphabet · Starred image of a domino · MPCP reduces to PCP on instances with nonempty words · Boolean test for nonempty words · The nonempty-words test is primitive recursive · The total reduction from MPCP to PCP · The star symbol · A star after every letter · A star before every letter · The start domino of the MPCP-to-PCP reduction · The reduction from MPCP to PCP · Top word of a sequence of dominoes
Used byReachability for rules with nonempty sides many-one reduces to PCP

DefinitionBoolean check for PCP solutions#✓fully proved

Let \(\alpha\) be an alphabet with a primitive recursive coding and decidable equality, and let \(P\) and \(s\) be lists of dominoes over \(\alpha\). The Boolean solution check of \(s\) for \(P\) is true exactly when \(s\) is nonempty, every domino of \(s\) occurs in \(P\), and the top word of \(s\) equals the bottom word of \(s\), and it is false otherwise.

def isSolutionB [DecidableEq α] (P s : List (Domino α)) : Bool :=
  !s.isEmpty && s.all (fun d ↦ decide (d ∈ P)) && decide (top s = bottom s)
Uses 3 · Used by 1
Statement usesDomino (Post correspondence problem) · Bottom word of a domino sequence · Top word of a sequence of dominoes
Used byPCP is recursively enumerable

TheoremPCP is recursively enumerable#✓fully proved

For an alphabet \(\alpha\) with a primitive recursive coding, the set of lists of dominoes over \(\alpha\) that have a PCP solution is recursively enumerable.

The proof searches all candidate sequences.

theorem rePred_pcp : REPred (PCP (α := α))
Uses 6 · Used by 1
Statement usesDomino (Post correspondence problem) · The Post correspondence problem
Proof usesPCP solution · Bottom word of a domino sequence · Boolean check for PCP solutions · Top word of a sequence of dominoes
Used byPCP is Turing-recognizable

TheoremPCP is Turing-recognizable#✓fully proved

For every alphabet \(\alpha\) with a primitive recursive encoding, there is a multi-stack Turing machine that, started on the binary encoding of a list \(P\) of dominoes over \(\alpha\), halts exactly when \(P\) has a PCP solution.

theorem tm2Recognizable_pcp : TM2Recognizable (PCP (α := α))
Uses 5 · Used by 1
Statement usesDomino (Post correspondence problem) · The Post correspondence problem · Recognizability by multi-stack machines
Proof usesPCP is recursively enumerable · Multi-stack recognizable predicates are exactly the r.e. predicates
Used byThe complement of PCP is not recognizable

TheoremTotal length of dominoes that are at least as long on top#✓fully proved

Write \(|w|\) for the length of a word \(w\). Let \(s\) be a finite sequence of dominoes over an alphabet. If every domino \((t, b)\) in \(s\) satisfies \(|b| \le |t|\), then the concatenation of the bottom words of \(s\) is no longer than the concatenation of the top words of \(s\).

theorem length_bottom_le_length_top {s : List (Domino α)}
    (h : ∀ d ∈ s, d.2.length ≤ d.1.length) : (bottom s).length ≤ (top s).length
Uses 3 · Used by 1
Statement usesDomino (Post correspondence problem) · Bottom word of a domino sequence · Top word of a sequence of dominoes
Used byTotal length of dominoes that are strictly longer on top

TheoremTotal length of dominoes that are strictly longer on top#✓fully proved

Write \(|w|\) for the length of a word \(w\). Let \(s\) be a nonempty finite sequence of dominoes over an alphabet. If every domino \((t, b)\) in \(s\) satisfies \(|b| < |t|\), then the concatenation of the bottom words of \(s\) is strictly shorter than the concatenation of the top words of \(s\).

theorem length_bottom_lt_length_top {s : List (Domino α)} (hs : s ≠ [])
    (h : ∀ d ∈ s, d.2.length < d.1.length) : (bottom s).length < (top s).length
Uses 4 · Used by 1
Statement usesDomino (Post correspondence problem) · Bottom word of a domino sequence · Top word of a sequence of dominoes
Proof usesTotal length of dominoes that are at least as long on top
Used byThe unary PCP criterion

DefinitionSwapping top and bottom#✓fully proved

For a finite sequence \(s\) of dominoes, the swapped sequence is obtained from \(s\) by exchanging the top and bottom word of every domino: each \((t, b)\) becomes \((b, t)\), and the order of the dominoes is unchanged.

def swap (s : List (Domino α)) : List (Domino α) := s.map Prod.swap
Uses 1 · Used by 1
Statement usesDomino (Post correspondence problem)
Used byThe unary PCP criterion

TheoremThe unary PCP criterion#✓fully proved

Let \(\alpha\) be an alphabet with at most one letter, and write \(|w|\) for the length of a word \(w\). A finite list \(P\) of dominoes over \(\alpha\) has a PCP solution if and only if either some domino \((t, b)\) in \(P\) has \(|t| = |b|\), or some domino \((t, b)\) in \(P\) has \(|t| < |b|\) and some domino \((t', b')\) in \(P\) has \(|b'| < |t'|\).

theorem pcp_iff_of_subsingleton (P : List (Domino α)) :
    PCP P ↔ (∃ d ∈ P, d.1.length = d.2.length) ∨
      ((∃ d ∈ P, d.1.length < d.2.length) ∧ ∃ e ∈ P, e.2.length < e.1.length)
Uses 7 · Used by 1
Statement usesDomino (Post correspondence problem) · The Post correspondence problem
Proof usesPCP solution · Bottom word of a domino sequence · Total length of dominoes that are strictly longer on top · Swapping top and bottom · Top word of a sequence of dominoes
Used byPCP over a one-letter alphabet is decidable

DefinitionThe unary PCP test#✓fully proved

Let \(\alpha\) be an alphabet with at most one letter, and write \(|w|\) for the length of a word \(w\). For a finite list \(P\) of dominoes over \(\alpha\), the unary test of \(P\) is the Boolean value that is true exactly when some domino \((t, b)\) in \(P\) has \(|t| = |b|\), or some domino \((t, b)\) in \(P\) has \(|t| < |b|\) and some domino \((t', b')\) in \(P\) has \(|b'| < |t'|\).

def unaryTest (P : List (Domino α)) : Bool :=
  P.any (fun d ↦ d.1.length == d.2.length) ||
    (P.any (fun d ↦ decide (d.1.length < d.2.length)) &&
      P.any fun e ↦ decide (e.2.length < e.1.length))
Uses 1 · Used by 1
Statement usesDomino (Post correspondence problem)
Used byPCP over a one-letter alphabet is decidable

TheoremPCP over a one-letter alphabet is decidable#✓fully proved

Let \(\alpha\) be an alphabet with at most one letter whose elements have a computable encoding. Then the Post correspondence problem over \(\alpha\) is a computable predicate: some computable function decides, for every finite list \(P\) of dominoes over \(\alpha\), whether \(P\) has a PCP solution.

theorem computablePred_pcp_of_subsingleton : ComputablePred (PCP (α := α))
Uses 4 · Used by 1
Statement usesDomino (Post correspondence problem) · The Post correspondence problem
Proof usesThe unary PCP criterion · The unary PCP test
Used byUnary PCP is decidable by a multi-stack machine

TheoremUnary PCP is decidable by a multi-stack machine#✓fully proved

Let \(\alpha\) be an alphabet with at most one letter whose elements have a computable encoding. Then the Post correspondence problem over \(\alpha\) is decidable by a multi-stack machine: some multi-stack Turing machine decides, for every finite list \(P\) of dominoes over \(\alpha\), whether \(P\) has a PCP solution.

theorem tm2Decidable_pcp_of_subsingleton : TM2Decidable (PCP (α := α))
Uses 5
Statement usesDomino (Post correspondence problem) · The Post correspondence problem · Decidability by multi-stack machines
Proof usesPCP over a one-letter alphabet is decidable · Multi-stack decidable predicates are exactly the computable predicates

InductiveSymbols of the rewriting system of a single-tape machine#✓fully proved

For a tape alphabet \(\Gamma\) and a set of states \(\Lambda\), the symbols of the rewriting system simulating a single-tape machine are a tape symbol \(a\) for each \(a \in \Gamma\), a state symbol \(q\) for each \(q \in \Lambda\), the left end marker \(\vdash\), the right end marker \(\dashv\) and the halting symbol \(H\).

inductive TMSym (Γ Λ : Type*) where
  /-- A tape symbol. -/
  | tape (a : Γ)
  /-- A state, written just left of the head symbol. -/
  | state (q : Λ)
  /-- The left end marker `⊢`. -/
  | lend
  /-- The right end marker `⊣`. -/
  | rend
  /-- The halting symbol `H`. -/
  | halt
  deriving DecidableEq, Fintype
Used by 32
Used byThe eight kinds of rules of the machine-simulating rewriting system · The rewrites from words with one control symbol are confluent · Number of control symbols · Rewriting preserves the number of control symbols · Rewrites from words with one control symbol · The halting symbol erases the tape · A halted configuration rewrites to the halting word · Thue equivalence from a word with one control symbol uses only controlled steps · Erasing rules · Some finite Thue system has an undecidable word problem · Reachability for string rewriting is undecidable · A word with one control symbol splits at it · One machine step is one rewrite · The halting word · The start word · Invariant of the rewriting simulation of a single-tape machine · Control symbols · Boolean test for control symbols · Single-tape halting many-one reduces to the word problem of a fixed Thue system · Single-tape halting many-one reduces to string rewriting reachability · Rewriting at a state symbol · The halting word is irreducible · The rewriting system simulating a Turing machine · The rules for one transition · The word of a configuration · Words spelling a configuration · Splitting a rewrite site at its control symbol · Every rewrite preserves the invariant of reachable words · Local confluence on words with one control symbol · A rewrite at the control symbol · A single-tape machine halts iff its start word rewrites to the halting word · A single-tape machine halts iff its start word is Thue equivalent to the halting word

DefinitionControl symbols#✓fully proved

A symbol of the rewriting system simulating a single-tape Turing machine is a control symbol if it is a state symbol or the halting symbol \(H\); tape symbols and the end markers \(\vdash\) and \(\dashv\) are not control symbols.

def IsCtl : TMSym Γ Λ → Prop
  | state _ => True
  | halt => True
  | _ => False
Uses 1 · Used by 5
Statement usesSymbols of the rewriting system of a single-tape machine
Used byA word with one control symbol splits at it · Splitting a rewrite site at its control symbol · Every rewrite preserves the invariant of reachable words · Local confluence on words with one control symbol · A rewrite at the control symbol

TheoremUnique splitting at a marked letter#✓fully proved

Let \(P\) be a property of the elements of a type \(\alpha\), let \(A\) and \(B\) be lists over \(\alpha\) none of whose elements satisfy \(P\), and let \(y \in \alpha\). If \(C\) and \(D\) are lists over \(\alpha\) and \(x \in \alpha\) satisfies \(P\) with \(C\,x\,D = A\,y\,B\) (concatenation), then \(C = A\), \(x = y\) and \(D = B\).

theorem eq_of_append_cons_eq {α : Type*} {P : α → Prop} {A B : List α} {y : α}
    (hA : ∀ s ∈ A, ¬P s) (hB : ∀ s ∈ B, ¬P s) :
    ∀ {C D : List α} {x : α}, P x → C ++ x :: D = A ++ y :: B → C = A ∧ x = y ∧ D = B
Used by 1
Used bySplitting a rewrite site at its control symbol

TheoremSplitting a rewrite site at its control symbol#✓fully proved

Let \(A\), \(B\), \(u\), \(v\), \(p\), \(s\) be words over the symbols of the rewriting system simulating a single-tape machine, and let \(x\) and \(y\) be symbols. If no symbol of \(A\) or of \(B\) is a control symbol (a state symbol or the halting symbol), \(x\) is a control symbol, and \(u\,p\,x\,s\,v = A\,y\,B\), then \(u\,p = A\), \(x = y\) and \(s\,v = B\).

theorem split_site {A B u v p s : List (TMSym Γ Λ)} {x y : TMSym Γ Λ}
    (hA : ∀ s ∈ A, ¬IsCtl s) (hB : ∀ s ∈ B, ¬IsCtl s) (hx : IsCtl x)
    (h : u ++ (p ++ x :: s) ++ v = A ++ y :: B) : u ++ p = A ∧ x = y ∧ s ++ v = B
Uses 3 · Used by 2
Statement usesControl symbols · Symbols of the rewriting system of a single-tape machine
Proof usesUnique splitting at a marked letter
Used byEvery rewrite preserves the invariant of reachable words · A rewrite at the control symbol

DefinitionThe word of a configuration#✓fully proved

For a state \(q\), a tape symbol \(h\) and words \(L\), \(R\) of tape symbols, the word of the configuration in state \(q\) with head symbol \(h\), left part \(L\) (in reading order, from left to right) and right part \(R\) is \(\vdash L\,q\,h\,R \dashv\), where \(\vdash\) and \(\dashv\) are the end markers.

def spell (q : Λ) (Lw : List Γ) (h : Γ) (R : List Γ) : List (TMSym Γ Λ) :=
  lend :: (Lw.map tape ++ state q :: tape h :: (R.map tape ++ [rend]))
Uses 1 · Used by 6
Statement usesSymbols of the rewriting system of a single-tape machine
Used byA halted configuration rewrites to the halting word · One machine step is one rewrite · The start word · Words spelling a configuration · Every rewrite preserves the invariant of reachable words · A single-tape machine halts iff its start word rewrites to the halting word

DefinitionThe halting word#✓fully proved

The halting word is the word \(\vdash H \dashv\) made of the left end marker, the halting symbol and the right end marker. It is the target word of the rewriting simulation of a single-tape machine.

def haltWord : List (TMSym Γ Λ) := [lend, halt, rend]
Uses 1 · Used by 7
Statement usesSymbols of the rewriting system of a single-tape machine
Used byThe halting symbol erases the tape · A halted configuration rewrites to the halting word · Single-tape halting many-one reduces to the word problem of a fixed Thue system · Single-tape halting many-one reduces to string rewriting reachability · The halting word is irreducible · A single-tape machine halts iff its start word rewrites to the halting word · A single-tape machine halts iff its start word is Thue equivalent to the halting word

DefinitionWords spelling a configuration#✓fully proved

A word \(w\) spells a configuration \(c\) of a single-tape Turing machine if there are a state \(q\), a tape symbol \(h\) and words \(L\), \(R\) of tape symbols such that \(c\) is in state \(q\), its head reads \(h\), its tape reads \(L\) immediately to the left of the head and \(R\) immediately to the right of it, with blanks beyond, and \(w = \vdash L\,q\,h\,R \dashv\).

def Spells (w : List (TMSym Γ Λ)) (c : TM0.Cfg Γ Λ) : Prop :=
  ∃ q h Lw R, c = ⟨q, ⟨h, ListBlank.mk Lw.reverse, ListBlank.mk R⟩⟩ ∧ w = spell q Lw h R
Uses 2 · Used by 5
Statement usesSymbols of the rewriting system of a single-tape machine · The word of a configuration
Used byA halted configuration rewrites to the halting word · One machine step is one rewrite · Invariant of the rewriting simulation of a single-tape machine · Every rewrite preserves the invariant of reachable words · A single-tape machine halts iff its start word rewrites to the halting word

DefinitionThe start word#✓fully proved

For an input \(l\) of tape symbols, the start word is \(\vdash q_0\, h\, R \dashv\), where \(\vdash\) and \(\dashv\) are the left and right end markers, \(q_0\) is the default state, \(h\) is the first symbol of \(l\) (the default tape symbol if \(l\) is empty) and \(R\) is the rest of \(l\). It spells the configuration in state \(q_0\) with head symbol \(h\), empty left part and right part \(R\).

def initWord (l : List Γ) : List (TMSym Γ Λ) := spell default [] l.headI l.tail
Uses 2 · Used by 4
Statement usesSymbols of the rewriting system of a single-tape machine · The word of a configuration
Used bySingle-tape halting many-one reduces to the word problem of a fixed Thue system · Single-tape halting many-one reduces to string rewriting reachability · A single-tape machine halts iff its start word rewrites to the halting word · A single-tape machine halts iff its start word is Thue equivalent to the halting word

DefinitionThe rules for one transition#✓fully proved

Let \(M\) be a single-tape Turing machine with finitely many states and tape symbols, let \(\sqcup\) be its blank symbol, and write \(\vdash\), \(\dashv\) for the end markers and \(H\) for the halting symbol. The rules for a state \(q\) reading a tape symbol \(a\) are: the rule \(q\,a \to H\) if \(M\) has no transition from \(q\) reading \(a\); the rule \(q\,a \to q'\,b\) if \(M\) writes \(b\) and enters \(q'\); the rules \(q\,a \dashv \to a\,q'\,\sqcup \dashv\) and, for every tape symbol \(c\), \(q\,a\,c \to a\,q'\,c\) if \(M\) moves right and enters \(q'\); and the rules \({\vdash}\,q\,a \to {\vdash}\,q'\,\sqcup\,a\) and, for every tape symbol \(c\), \(c\,q\,a \to q'\,c\,a\) if \(M\) moves left and enters \(q'\).

noncomputable def rulesFor (q : Λ) (a : Γ) : List (Rule (TMSym Γ Λ)) :=
  match M q a with
  | none => [([state q, tape a], [halt])]
  | some (q', .write b) => [([state q, tape a], [state q', tape b])]
  | some (q', .move .right) => ([state q, tape a, rend], [tape a, state q', tape default, rend]) ::
      (Finset.univ : Finset Γ).toList.map fun c ↦
        ([state q, tape a, tape c], [tape a, state q', tape c])
  | some (q', .move .left) => ([lend, state q, tape a], [lend, state q', tape default, tape a]) ::
      (Finset.univ : Finset Γ).toList.map fun c ↦
        ([tape c, state q, tape a], [state q', tape c, tape a])
Uses 2 · Used by 6
Statement usesRewriting rules · Symbols of the rewriting system of a single-tape machine
Used byThe eight kinds of rules of the machine-simulating rewriting system · The halting symbol erases the tape · A halted configuration rewrites to the halting word · One machine step is one rewrite · The rewriting system simulating a Turing machine · Local confluence on words with one control symbol

DefinitionErasing rules#✓fully proved

For a finite tape alphabet \(\Gamma\), let \(H\) be the halting symbol of the rewriting system simulating a single-tape machine with tape alphabet \(\Gamma\). The erasing rules are the rewriting rules \(c\,H \to H\) and \(H\,c \to H\) for every tape symbol \(c \in \Gamma\): the halting symbol deletes the tape symbol on either side of it.

noncomputable def eraseRules : List (Rule (TMSym Γ Λ)) :=
  (Finset.univ : Finset Γ).toList.flatMap fun c ↦
    [([tape c, halt], [halt]), ([halt, tape c], [halt])]
Uses 2 · Used by 3
Statement usesRewriting rules · Symbols of the rewriting system of a single-tape machine
Used byA halted configuration rewrites to the halting word · One machine step is one rewrite · The rewriting system simulating a Turing machine

DefinitionThe rewriting system simulating a Turing machine#✓fully proved

Let \(M\) be a single-tape Turing machine with finitely many states and tape symbols, and write \(H\) for the halting symbol. The rewriting system simulating \(M\) is the finite list of rules consisting of the rules for every state \(q\) reading every tape symbol \(a\), followed by the erasing rules \(c\,H \to H\) and \(H\,c \to H\) for every tape symbol \(c\).

noncomputable def rules : List (Rule (TMSym Γ Λ)) :=
  ((Finset.univ : Finset Λ).toList.flatMap fun q ↦
    (Finset.univ : Finset Γ).toList.flatMap fun a ↦ rulesFor M q a) ++ eraseRules
Uses 4 · Used by 17
Statement usesRewriting rules · Symbols of the rewriting system of a single-tape machine · Erasing rules · The rules for one transition
Used byThe eight kinds of rules of the machine-simulating rewriting system · The rewrites from words with one control symbol are confluent · Rewriting preserves the number of control symbols · Rewrites from words with one control symbol · The halting symbol erases the tape · A halted configuration rewrites to the halting word · Thue equivalence from a word with one control symbol uses only controlled steps · Some finite Thue system has an undecidable word problem · One machine step is one rewrite · Single-tape halting many-one reduces to the word problem of a fixed Thue system · Single-tape halting many-one reduces to string rewriting reachability · The halting word is irreducible · Every rewrite preserves the invariant of reachable words · Local confluence on words with one control symbol · A rewrite at the control symbol · A single-tape machine halts iff its start word rewrites to the halting word · A single-tape machine halts iff its start word is Thue equivalent to the halting word

TheoremThe eight kinds of rules of the machine-simulating rewriting system#✓fully proved

Let \(M\) be a single-tape Turing machine with a finite tape alphabet \(\Gamma\), a default (blank) symbol \(\beta \in \Gamma\) and finitely many states. The symbols are the tape symbols, the states, the end markers \(\vdash\) and \(\dashv\), and the halting symbol \(H\). Every rule \(l \to r\) of the rewriting system simulating \(M\) has one of the following eight forms, where \(q, q'\) are states and \(a, b, c\) are tape symbols. Either \(M\) has no transition in state \(q\) reading \(a\), and \(l = q\,a\), \(r = H\); or in state \(q\) reading \(a\) the machine \(M\) goes to state \(q'\) and writes \(b\), and \(l = q\,a\), \(r = q'\,b\); or in state \(q\) reading \(a\) it goes to \(q'\) and moves the head right, and either \(l = q\,a \dashv\), \(r = a\,q'\,\beta \dashv\) or \(l = q\,a\,c\), \(r = a\,q'\,c\); or in state \(q\) reading \(a\) it goes to \(q'\) and moves the head left, and either \(l = \vdash q\,a\), \(r = \vdash q'\,\beta\,a\) or \(l = c\,q\,a\), \(r = q'\,c\,a\); or \(l = c\,H\), \(r = H\); or \(l = H\,c\), \(r = H\).

theorem cases_of_mem_rules {l r : List (TMSym Γ Λ)} (h : (l, r) ∈ rules M) :
    (∃ q a, M q a = none ∧ l = [state q, tape a] ∧ r = [halt]) ∨
    (∃ q a q' b, M q a = some (q', .write b) ∧ l = [state q, tape a] ∧
      r = [state q', tape b]) ∨
    (∃ q a q', M q a = some (q', .move .right) ∧ l = [state q, tape a, rend] ∧
      r = [tape a, state q', tape default, rend]) ∨
    (∃ q a q' c, M q a = some (q', .move .right) ∧ l = [state q, tape a, tape c] ∧
      r = [tape a, state q', tape c]) ∨
    (∃ q a q', M q a = some (q', .move .left) ∧ l = [lend, state q, tape a] ∧
      r = [lend, state q', tape default, tape a]) ∨
    (∃ q a q' c, M q a = some (q', .move .left) ∧ l = [tape c, state q, tape a] ∧
      r = [state q', tape c, tape a]) ∨
    (∃ c, l = [tape c, halt] ∧ r = [halt]) ∨
    (∃ c, l = [halt, tape c] ∧ r = [halt])
Uses 4 · Used by 4
Statement usesRewriting rules · Symbols of the rewriting system of a single-tape machine · The rewriting system simulating a Turing machine
Proof usesThe rules for one transition
Used byRewriting preserves the number of control symbols · Single-tape halting many-one reduces to string rewriting reachability · Every rewrite preserves the invariant of reachable words · A rewrite at the control symbol

TheoremOne machine step is one rewrite#✓fully proved

Let \(M\) be a single-tape Turing machine with finitely many tape symbols and states. If the word \(w\) spells the configuration \(c\) and \(M\) steps from \(c\) to \(c'\), then \(w\) rewrites in one step of the rewriting system simulating \(M\) to a word \(w'\) that spells \(c'\).

theorem exists_step_of_spells {w : List (TMSym Γ Λ)} {c c' : TM0.Cfg Γ Λ} (hw : Spells w c)
    (hc : c' ∈ TM0.step M c) : ∃ w', Step (rules M) w w' ∧ Spells w' c'
Uses 8 · Used by 1
Statement usesOne-step rewriting · Words spelling a configuration · Symbols of the rewriting system of a single-tape machine · The rewriting system simulating a Turing machine
Proof usesRewriting rules · Erasing rules · The rules for one transition · The word of a configuration
Used byA single-tape machine halts iff its start word rewrites to the halting word

TheoremThe halting symbol erases the tape#✓fully proved

Let \(M\) be a single-tape Turing machine with finitely many states and tape symbols, and let \(\vdash\), \(\dashv\) be the end markers and \(H\) the halting symbol of the rewriting system simulating \(M\). For all words \(X\) and \(Y\) of tape symbols, the word \(\vdash X\,H\,Y \dashv\) rewrites in zero or more steps of this rewriting system to the halting word \(\vdash H \dashv\).

theorem derives_erase (X Y : List Γ) :
    Derives (rules M) (lend :: (X.map tape ++ halt :: (Y.map tape ++ [rend]))) haltWord
Uses 7 · Used by 1
Statement usesDerivations in a string rewriting system · Symbols of the rewriting system of a single-tape machine · The halting word · The rewriting system simulating a Turing machine
Proof usesRewriting rules · One-step rewriting · The rules for one transition
Used byA halted configuration rewrites to the halting word

TheoremA halted configuration rewrites to the halting word#✓fully proved

Let \(M\) be a single-tape Turing machine with finitely many states and tape symbols, and let \(\vdash\), \(\dashv\) be the end markers and \(H\) the halting symbol of the rewriting system simulating \(M\). Let \(c\) be a configuration of \(M\) at which \(M\) has no next step, and let \(w\) be a word that spells \(c\): for some state \(q\), tape symbol \(h\) and lists \(L\), \(R\) of tape symbols, \(c\) is in state \(q\) with \(h\) under the head, the tape left of the head reads \(L\) from left to right and the tape right of the head reads \(R\), up to blanks at the far ends, and \(w = \vdash L\,q\,h\,R \dashv\). Then \(w\) rewrites in zero or more steps of this rewriting system to the halting word \(\vdash H \dashv\).

theorem derives_of_spells_of_step_eq_none {w : List (TMSym Γ Λ)} {c : TM0.Cfg Γ Λ}
    (hw : Spells w c) (hc : TM0.step M c = none) : Derives (rules M) w haltWord
Uses 11 · Used by 1
Statement usesDerivations in a string rewriting system · Words spelling a configuration · Symbols of the rewriting system of a single-tape machine · The halting word · The rewriting system simulating a Turing machine
Proof usesRewriting rules · One-step rewriting · The halting symbol erases the tape · Erasing rules · The rules for one transition · The word of a configuration
Used byA single-tape machine halts iff its start word rewrites to the halting word

DefinitionInvariant of the rewriting simulation of a single-tape machine#✓fully proved

Let \(M\) be a single-tape machine with finitely many tape symbols and states, and \(l\) an input. A word \(w\) satisfies the invariant for \(l\) when either \(w\) spells a configuration that \(M\) reaches from its initial configuration on \(l\), or \(M\) halts on \(l\) and \(w = \vdash X\, H\, Y \dashv\) for some words \(X\) and \(Y\) of tape symbols, where \(\vdash\) and \(\dashv\) are the left and right end markers and \(H\) is the halting symbol. It serves as the invariant of the words reachable from the start word of \(l\).

def Inv (l : List Γ) (w : List (TMSym Γ Λ)) : Prop :=
  (∃ c, StateTransition.Reaches (TM0.step M) (TM0.init l) c ∧ Spells w c) ∨
    (TM0HaltsOn M l ∧ ∃ X Y : List Γ, w = lend :: (X.map tape ++ halt :: (Y.map tape ++ [rend])))
Uses 3 · Used by 2
Statement usesHalting of a single-tape machine · Words spelling a configuration · Symbols of the rewriting system of a single-tape machine
Used byEvery rewrite preserves the invariant of reachable words · A single-tape machine halts iff its start word rewrites to the halting word

TheoremEvery rewrite preserves the invariant of reachable words#✓fully proved

Let \(M\) be a single-tape machine with finite tape alphabet and finite set of states, and let \(l\) be an input word. Write \(\vdash\) and \(\dashv\) for the left and right end markers and \(H\) for the halting symbol. A word \(w\) satisfies the invariant for \(M\) and \(l\) when either \(w\) spells a configuration that \(M\) reaches from its initial configuration on \(l\) (the configuration with state \(q\), head symbol \(h\), left part \(L\) and right part \(R\), finite words of tape symbols read from left to right beyond which the tape is blank, is spelled \({\vdash}\,L\,q\,h\,R\,{\dashv}\)), or \(M\) halts on \(l\) and \(w = {\vdash}\,X\,H\,Y\,{\dashv}\) for words \(X\) and \(Y\) of tape symbols. If \(w\) satisfies the invariant and rewrites in one step to \(w'\) under the rules of \(M\), then \(w'\) satisfies the invariant.

theorem Inv.step {l : List Γ} {w w' : List (TMSym Γ Λ)} (hw : Inv M l w)
    (hs : Step (rules M) w w') : Inv M l w'
Uses 11 · Used by 1
Statement usesOne-step rewriting · Invariant of the rewriting simulation of a single-tape machine · Symbols of the rewriting system of a single-tape machine · The rewriting system simulating a Turing machine
Proof usesRewriting rules · Halting of a single-tape machine · Control symbols · Words spelling a configuration · The eight kinds of rules of the machine-simulating rewriting system · The word of a configuration · Splitting a rewrite site at its control symbol
Used byA single-tape machine halts iff its start word rewrites to the halting word

TheoremA single-tape machine halts iff its start word rewrites to the halting word#✓fully proved

Let \(M\) be a single-tape machine with finite tape alphabet and finite set of states, and write \(\vdash\) and \(\dashv\) for the left and right end markers and \(H\) for the halting symbol. For every input word \(l\), \(M\) halts on \(l\) if and only if the start word \({\vdash}\,q_0\,h\,R\,{\dashv}\) of \(l\) rewrites to the halting word \({\vdash}\,H\,{\dashv}\) in zero or more steps under the rules of \(M\), where \(q_0\) is the default state, \(h\) is the first letter of \(l\) (the blank if \(l\) is empty) and \(R\) is the rest of \(l\).

theorem tm0HaltsOn_iff_derives (l : List Γ) :
    TM0HaltsOn M l ↔ Derives (rules M) (initWord l) haltWord
Uses 14 · Used by 2
Statement usesDerivations in a string rewriting system · Halting of a single-tape machine · Symbols of the rewriting system of a single-tape machine · The halting word · The start word · The rewriting system simulating a Turing machine
Proof usesRewriting rules · One-step rewriting · Invariant of the rewriting simulation of a single-tape machine · Every rewrite preserves the invariant of reachable words · Words spelling a configuration · A halted configuration rewrites to the halting word · One machine step is one rewrite · The word of a configuration
Used bySingle-tape halting many-one reduces to string rewriting reachability · A single-tape machine halts iff its start word is Thue equivalent to the halting word

TheoremSingle-tape halting many-one reduces to string rewriting reachability#✓fully proved

Let \(M\) be a single-tape Turing machine with finitely many states and tape symbols. Then the set of inputs on which \(M\) halts is many-one reducible to the set of instances \((R, x, y)\), where \(R\) is a list of rules and \(x\), \(y\) are words over the symbols of the rewriting system simulating \(M\), such that every rule of \(R\) has a nonempty left side and a nonempty right side and \(x\) rewrites to \(y\) in zero or more steps of \(R\).

theorem manyOneReducible_tm0HaltsOn_sr [Finite Γ] [Finite Λ] [Primcodable Γ]
    [Primcodable (TMSym Γ Λ)] :
    ManyOneReducible (TM0HaltsOn M) fun I : List (Rule (TMSym Γ Λ)) × List (TMSym Γ Λ) ×
      List (TMSym Γ Λ) ↦ NonemptyRules I.1 ∧ SR I
Uses 11 · Used by 1
Statement usesRewriting systems with nonempty sides · Rewriting rules · The reachability problem for string rewriting · Halting of a single-tape machine · Symbols of the rewriting system of a single-tape machine
Proof usesDerivations in a string rewriting system · The eight kinds of rules of the machine-simulating rewriting system · The halting word · The start word · The rewriting system simulating a Turing machine · A single-tape machine halts iff its start word rewrites to the halting word
Used byReachability for string rewriting is undecidable

TheoremReachability for string rewriting is undecidable#✓fully proved

There is a finite alphabet \(\alpha\), with a primitive recursive coding of its letters by natural numbers, such that no multi-stack Turing machine decides, for a finite list \(R\) of rewriting rules over \(\alpha\) and words \(x\) and \(y\) over \(\alpha\), whether every rule of \(R\) has a nonempty left side and a nonempty right side and \(x\) rewrites to \(y\) in zero or more steps of \(R\).

theorem exists_not_tm2Decidable_sr :
    ∃ (α : Type) (_ : Fintype α) (_ : Primcodable α),
      ¬TM2Decidable fun I : List (Rule α) × List α × List α ↦ NonemptyRules I.1 ∧ SR I
Uses 12 · Used by 2
Statement usesRewriting systems with nonempty sides · Rewriting rules · The reachability problem for string rewriting · Decidability by multi-stack machines
Proof usesHalting of a single-tape machine · Symbols of the rewriting system of a single-tape machine · Single-tape halting many-one reduces to string rewriting reachability · The halting problem for single-tape machines is undecidable · Primitive recursive coding of a finite type · Decidability transfers along mapping reductions · The restricted machine evaluates like the original · Restriction of a single-tape machine to a supporting set of states
Used byMPCP is undecidable · The Post correspondence problem is undecidable

TheoremMPCP is undecidable#✓fully proved

There is a finite alphabet \(\alpha\), with a primitive recursive coding of its letters by natural numbers, such that no multi-stack Turing machine decides, for a finite list \(P\) of dominoes over \(\alpha\), whether every domino of \(P\) has a nonempty top and a nonempty bottom and \(P\) has a solution of the modified Post correspondence problem, that is, a nonempty sequence of dominoes of \(P\), repetitions allowed, that starts with the first domino of \(P\) and whose tops and bottoms concatenate to the same word.

theorem exists_not_tm2Decidable_mpcp :
    ∃ (α : Type) (_ : Fintype α) (_ : Primcodable α),
      ¬TM2Decidable fun P : List (Post.Domino α) ↦ Post.NonemptyWords P ∧ Post.MPCP P
Uses 11
Statement usesDomino (Post correspondence problem) · The modified Post correspondence problem · Instances with nonempty words · Decidability by multi-stack machines
Proof usesThe extended alphabet of the MPCP-to-PCP reduction · Rewriting systems with nonempty sides · Rewriting rules · The reachability problem for string rewriting · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability for string rewriting is undecidable · Decidability transfers along mapping reductions

TheoremThe Post correspondence problem is undecidable#✓fully proved

There is a finite alphabet \(\alpha\), with a primitive recursive coding of its letters by natural numbers, such that no multi-stack Turing machine decides whether a finite list of dominoes over \(\alpha\) has a solution, that is, a nonempty sequence of dominoes of the list, repetitions allowed, whose tops and bottoms concatenate to the same word.

theorem exists_not_tm2Decidable_pcp :
    ∃ (α : Type) (_ : Fintype α) (_ : Primcodable α), ¬TM2Decidable (Post.PCP (α := α))
Uses 10 · Used by 5
Statement usesDomino (Post correspondence problem) · The Post correspondence problem · Decidability by multi-stack machines
Proof usesThe extended alphabet of the MPCP-to-PCP reduction · Rewriting systems with nonempty sides · Rewriting rules · The reachability problem for string rewriting · Reachability for rules with nonempty sides many-one reduces to PCP · Reachability for string rewriting is undecidable · Decidability transfers along mapping reductions
Used byThe Post correspondence problem is undecidable over the binary alphabet · Whether a context-free grammar is ambiguous is undecidable · Whether two context-free languages intersect is undecidable · Whether a context-free grammar generates every word is undecidable · The complement of PCP is not recognizable

DefinitionBoolean test for control symbols#✓fully proved

The Boolean function on the symbols of the rewriting system simulating a single-tape Turing machine that is true on every state symbol and on the halting symbol \(H\), and false on every tape symbol and on the end markers \(\vdash\) and \(\dashv\).

def isCtlB : TMSym Γ Λ → Bool
  | state _ => true
  | halt => true
  | _ => false
Uses 1 · Used by 4
Statement usesSymbols of the rewriting system of a single-tape machine
Used byNumber of control symbols · Rewriting preserves the number of control symbols · A word with one control symbol splits at it · A single-tape machine halts iff its start word is Thue equivalent to the halting word

DefinitionNumber of control symbols#✓fully proved

The number of control symbols of a word \(w\) over the symbols of the rewriting system simulating a single-tape machine is the number of letters of \(w\) that are states or the halting symbol \(H\).

def ctlCount (w : List (TMSym Γ Λ)) : ℕ := w.countP isCtlB
Uses 2 · Used by 7
Statement usesSymbols of the rewriting system of a single-tape machine · Boolean test for control symbols
Used byThe rewrites from words with one control symbol are confluent · Rewriting preserves the number of control symbols · Rewrites from words with one control symbol · Thue equivalence from a word with one control symbol uses only controlled steps · A word with one control symbol splits at it · Local confluence on words with one control symbol · A single-tape machine halts iff its start word is Thue equivalent to the halting word

TheoremA word with one control symbol splits at it#✓fully proved

If a word \(w\) over the symbols of the rewriting system simulating a single-tape machine contains exactly one control symbol (a state symbol or the halting symbol), then \(w = p\,x\,s\) for a control symbol \(x\) and words \(p\) and \(s\) that contain no control symbol.

theorem exists_split_of_ctlCount_eq_one :
    ∀ {w : List (TMSym Γ Λ)}, ctlCount w = 1 → ∃ pre x post, w = pre ++ x :: post ∧ IsCtl x ∧
      (∀ y ∈ pre, ¬IsCtl y) ∧ (∀ y ∈ post, ¬IsCtl y)
Uses 4 · Used by 1
Statement usesControl symbols · Symbols of the rewriting system of a single-tape machine · Number of control symbols
Proof usesBoolean test for control symbols
Used byLocal confluence on words with one control symbol

DefinitionRewriting at a state symbol#✓fully proved

Let \(M\) be a single-tape Turing machine with finitely many states and tape symbols, and let \(\sqcup\) be its blank symbol. For words \(u\), \(v\) and a state \(q\), the successor of \(u\,q\,v\) is defined as follows. If \(v\) does not begin with a tape symbol, there is none. If \(v = a\,v'\) for a tape symbol \(a\): when \(M\) has no transition from \(q\) reading \(a\), it is \(u\,H\,v'\), where \(H\) is the halting symbol; when \(M\) writes \(b\) and enters \(q'\), it is \(u\,q'\,b\,v'\); when \(M\) moves right and enters \(q'\), it is \(u\,a\,q'\,\sqcup \dashv v''\) if \(v' = {\dashv}\,v''\) for the right end marker \(\dashv\), it is \(u\,a\,q'\,c\,v''\) if \(v' = c\,v''\) for a tape symbol \(c\), and there is none otherwise; when \(M\) moves left and enters \(q'\), it is \(u' \vdash q'\,\sqcup\,a\,v'\) if \(u = u' \vdash\) for the left end marker \(\vdash\), it is \(u'\,q'\,c\,a\,v'\) if \(u = u'\,c\) for a tape symbol \(c\), and there is none otherwise.

Cslib.Decidability.TMRewriting.nextState · 16 lines 
def nextState (pre : List (TMSym Γ Λ)) (q : Λ) : List (TMSym Γ Λ) → Option (List (TMSym Γ Λ))
  | tape a :: post' =>
    match M q a with
    | none => some (pre ++ halt :: post')
    | some (q', .write b) => some (pre ++ state q' :: tape b :: post')
    | some (q', .move .right) =>
      match post' with
      | rend :: post'' => some (pre ++ tape a :: state q' :: tape default :: rend :: post'')
      | tape c :: post'' => some (pre ++ tape a :: state q' :: tape c :: post'')
      | _ => none
    | some (q', .move .left) =>
      match pre.getLast? with
      | some lend => some (pre.dropLast ++ lend :: state q' :: tape default :: tape a :: post')
      | some (tape c) => some (pre.dropLast ++ state q' :: tape c :: tape a :: post')
      | _ => none
  | _ => none
Uses 1 · Used by 3
Statement usesSymbols of the rewriting system of a single-tape machine
Used byThe halting word is irreducible · Local confluence on words with one control symbol · A rewrite at the control symbol

TheoremA rewrite at the control symbol#✓fully proved

Let \(M\) be a single-tape machine with finite tape alphabet and finite set of states. Let \(x\) be a control symbol (a state symbol or the halting symbol \(H\)) and let \(u\) and \(v\) be words that contain no control symbol. If \(u\,x\,v\) rewrites in one step to \(w'\) under the rules of \(M\), then either \(x\) is a state symbol \(q\) and the successor of \(u\,q\,v\) under the rules for \(q\) is defined and equals \(w'\), or \(x = H\) and either \(u = u'\,c\) for a word \(u'\) and a tape symbol \(c\) with \(w' = u'\,H\,v\), or \(v = c\,v'\) for a tape symbol \(c\) and a word \(v'\) with \(w' = u\,H\,v'\).

theorem step_result {pre post w' : List (TMSym Γ Λ)} {x : TMSym Γ Λ} (hx : IsCtl x)
    (hpre : ∀ y ∈ pre, ¬IsCtl y) (hpost : ∀ y ∈ post, ¬IsCtl y)
    (h : Step (rules M) (pre ++ x :: post) w') :
    (∃ q, x = state q ∧ nextState M pre q post = some w') ∨
      (x = halt ∧ ((∃ pre' c, pre = pre' ++ [tape c] ∧ w' = pre' ++ halt :: post) ∨
        (∃ c post', post = tape c :: post' ∧ w' = pre ++ halt :: post')))
Uses 8 · Used by 2
Statement usesOne-step rewriting · Control symbols · Symbols of the rewriting system of a single-tape machine · Rewriting at a state symbol · The rewriting system simulating a Turing machine
Proof usesRewriting rules · The eight kinds of rules of the machine-simulating rewriting system · Splitting a rewrite site at its control symbol
Used byThe halting word is irreducible · Local confluence on words with one control symbol

TheoremRewriting preserves the number of control symbols#✓fully proved

Let \(M\) be a single-tape Turing machine with finitely many states and tape symbols, and call the states and the halting symbol \(H\) control symbols. If a word \(w\) rewrites to \(w'\) in one step of the rewriting system simulating \(M\), then \(w\) and \(w'\) contain the same number of control symbols.

theorem ctlCount_eq_of_step {w w' : List (TMSym Γ Λ)} (h : Step (rules M) w w') :
    ctlCount w = ctlCount w'
Uses 7 · Used by 2
Statement usesOne-step rewriting · Symbols of the rewriting system of a single-tape machine · Number of control symbols · The rewriting system simulating a Turing machine
Proof usesRewriting rules · The eight kinds of rules of the machine-simulating rewriting system · Boolean test for control symbols
Used byThe rewrites from words with one control symbol are confluent · Thue equivalence from a word with one control symbol uses only controlled steps

TheoremLocal confluence on words with one control symbol#✓fully proved

Let \(M\) be a single-tape machine with finite tape alphabet and finite set of states, and let \(w\) be a word over the symbols of its rewriting system that contains exactly one control symbol (a state symbol or the halting symbol). If \(w\) rewrites in one step to \(w_1\) and in one step to \(w_2\) under the rules of \(M\), then there is a word \(d\) such that \(w_1\) rewrites to \(d\) in at most one step and \(w_2\) rewrites to \(d\) in zero or more steps.

Rewriting at a state symbol is deterministic, and the two erasures at the halting symbol commute.

theorem step_confluent {w w₁ w₂ : List (TMSym Γ Λ)} (hc : ctlCount w = 1)
    (h₁ : Step (rules M) w w₁) (h₂ : Step (rules M) w w₂) :
    ∃ d, ReflGen (Step (rules M)) w₁ d ∧ ReflTransGen (Step (rules M)) w₂ d
Uses 10 · Used by 1
Statement usesOne-step rewriting · Symbols of the rewriting system of a single-tape machine · Number of control symbols · The rewriting system simulating a Turing machine
Proof usesRewriting rules · Control symbols · A word with one control symbol splits at it · Rewriting at a state symbol · The rules for one transition · A rewrite at the control symbol
Used byThe rewrites from words with one control symbol are confluent

TheoremThe halting word is irreducible#✓fully proved

Let \(M\) be a single-tape Turing machine with finitely many states and tape symbols. There is no word \(w\) such that the halting word \(\vdash H \dashv\) rewrites to \(w\) in one step of the rewriting system simulating \(M\).

theorem not_step_haltWord (w : List (TMSym Γ Λ)) : ¬Step (rules M) haltWord w
Uses 6 · Used by 1
Statement usesOne-step rewriting · Symbols of the rewriting system of a single-tape machine · The halting word · The rewriting system simulating a Turing machine
Proof usesRewriting at a state symbol · A rewrite at the control symbol
Used byA single-tape machine halts iff its start word is Thue equivalent to the halting word

DefinitionRewrites from words with one control symbol#✓fully proved

Let \(M\) be a single-tape Turing machine with finitely many states and tape symbols, and call the states and the halting symbol \(H\) control symbols. A word \(w\) rewrites to \(w'\) by a controlled step when \(w\) contains exactly one control symbol and \(w\) rewrites to \(w'\) in one step of the rewriting system simulating \(M\).

def CtlStep (w w' : List (TMSym Γ Λ)) : Prop := ctlCount w = 1 ∧ Step (rules M) w w'
Uses 4 · Used by 3
Statement usesOne-step rewriting · Symbols of the rewriting system of a single-tape machine · Number of control symbols · The rewriting system simulating a Turing machine
Used byThe rewrites from words with one control symbol are confluent · Thue equivalence from a word with one control symbol uses only controlled steps · A single-tape machine halts iff its start word is Thue equivalent to the halting word

TheoremThue equivalence from a word with one control symbol uses only controlled steps#✓fully proved

Let \(M\) be a single-tape Turing machine with finitely many states and tape symbols, and call the states and the halting symbol \(H\) control symbols. Suppose \(w\) contains exactly one control symbol, and \(w\) and \(w'\) are equivalent under the equivalence relation generated by one-step rewriting in the rewriting system simulating \(M\). Then \(w\) and \(w'\) are equivalent under the equivalence relation generated by the one-step rewrites from words with exactly one control symbol.

theorem eqvGen_ctlStep {w w' : List (TMSym Γ Λ)} (h : EqvGen (Step (rules M)) w w')
    (hw : ctlCount w = 1) : EqvGen (CtlStep M) w w'
Uses 6 · Used by 1
Statement usesOne-step rewriting · Rewrites from words with one control symbol · Symbols of the rewriting system of a single-tape machine · Number of control symbols · The rewriting system simulating a Turing machine
Proof usesRewriting preserves the number of control symbols
Used byA single-tape machine halts iff its start word is Thue equivalent to the halting word

TheoremThe rewrites from words with one control symbol are confluent#✓fully proved

Let \(M\) be a single-tape Turing machine with finitely many states and tape symbols, and call the states and the halting symbol \(H\) control symbols. Consider the relation in which a word \(w\) with exactly one control symbol rewrites to \(w'\) by one step of the rewriting system simulating \(M\). This relation is confluent: if \(w\) rewrites in zero or more such steps to both \(w_1\) and \(w_2\), then \(w_1\) and \(w_2\) both rewrite in zero or more such steps to a common word.

theorem confluent_ctlStep : Confluent (CtlStep M)
Uses 7 · Used by 1
Statement usesRewrites from words with one control symbol · Symbols of the rewriting system of a single-tape machine
Proof usesOne-step rewriting · Number of control symbols · Rewriting preserves the number of control symbols · The rewriting system simulating a Turing machine · Local confluence on words with one control symbol
Used byA single-tape machine halts iff its start word is Thue equivalent to the halting word

TheoremA single-tape machine halts iff its start word is Thue equivalent to the halting word#✓fully proved

Let \(M\) be a single-tape Turing machine with finitely many states and tape symbols, write \(\vdash\) and \(\dashv\) for the left and right end markers and \(H\) for the halting symbol, and let \(l\) be an input word of tape symbols. Then \(M\) halts on \(l\) if and only if the start word of \(l\) and the halting word \({\vdash}\,H\,{\dashv}\) are equivalent under the reflexive, symmetric and transitive closure of one-step rewriting by the rewriting system simulating \(M\).

theorem tm0HaltsOn_iff_eqvGen (l : List Γ) :
    TM0HaltsOn M l ↔ EqvGen (Step (rules M)) (initWord l) haltWord
Uses 15 · Used by 1
Statement usesOne-step rewriting · Halting of a single-tape machine · Symbols of the rewriting system of a single-tape machine · The halting word · The start word · The rewriting system simulating a Turing machine
Proof usesDerivations in a string rewriting system · Rewriting rules · Rewrites from words with one control symbol · The rewrites from words with one control symbol are confluent · Number of control symbols · Thue equivalence from a word with one control symbol uses only controlled steps · Boolean test for control symbols · The halting word is irreducible · A single-tape machine halts iff its start word rewrites to the halting word
Used bySingle-tape halting many-one reduces to the word problem of a fixed Thue system

TheoremSingle-tape halting many-one reduces to the word problem of a fixed Thue system#✓fully proved

Let \(M\) be a single-tape Turing machine with finitely many states and tape symbols, and let \(R_M\) be the rewriting system simulating \(M\). Then the set of inputs on which \(M\) halts is many-one reducible to the set of pairs \((x, y)\) of words over the symbols of \(R_M\) that are equivalent under the reflexive, symmetric and transitive closure of one-step rewriting by \(R_M\).

theorem manyOneReducible_tm0HaltsOn_eqvGen [Primcodable Γ] [Primcodable (TMSym Γ Λ)] :
    ManyOneReducible (TM0HaltsOn M)
      fun p : List (TMSym Γ Λ) × List (TMSym Γ Λ) ↦ EqvGen (Step (rules M)) p.1 p.2
Uses 7 · Used by 1
Statement usesOne-step rewriting · Halting of a single-tape machine · Symbols of the rewriting system of a single-tape machine · The rewriting system simulating a Turing machine
Proof usesThe halting word · The start word · A single-tape machine halts iff its start word is Thue equivalent to the halting word
Used bySome finite Thue system has an undecidable word problem

TheoremSome finite Thue system has an undecidable word problem#✓fully proved

(Post, Markov) There are a finite alphabet \(\alpha\), with a primitive recursive coding of its letters by natural numbers, and a finite list \(R\) of rewriting rules over \(\alpha\) such that no multi-stack Turing machine decides, for words \(x\) and \(y\) over \(\alpha\), whether \(x\) and \(y\) are equivalent under the reflexive, symmetric and transitive closure of one-step rewriting by \(R\).

theorem exists_not_tm2Decidable_eqvGen :
    ∃ (α : Type) (_ : Fintype α) (_ : Primcodable α) (R : List (Rule α)),
      ¬TM2Decidable fun p : List α × List α ↦ EqvGen (Step R) p.1 p.2
Uses 12 · Used by 1
Statement usesRewriting rules · One-step rewriting · Decidability by multi-stack machines
Proof usesHalting of a single-tape machine · Symbols of the rewriting system of a single-tape machine · Single-tape halting many-one reduces to the word problem of a fixed Thue system · The rewriting system simulating a Turing machine · The halting problem for single-tape machines is undecidable · Primitive recursive coding of a finite type · Decidability transfers along mapping reductions · The restricted machine evaluates like the original · Restriction of a single-tape machine to a supporting set of states
Used byThe uniform word problem for Thue systems is undecidable

TheoremThe uniform word problem for Thue systems is undecidable#✓fully proved

There is a finite alphabet \(\alpha\), with a primitive recursive coding of its letters by natural numbers, such that no multi-stack Turing machine decides, for a finite list \(R\) of rewriting rules over \(\alpha\) and words \(x\) and \(y\) over \(\alpha\), whether \(x\) and \(y\) are equivalent under the reflexive, symmetric and transitive closure of one-step rewriting by \(R\).

theorem exists_not_tm2Decidable_thueWP :
    ∃ (α : Type) (_ : Fintype α) (_ : Primcodable α), ¬TM2Decidable (ThueWP (α := α))
Uses 6
Statement usesRewriting rules · The word problem of a Thue system · Decidability by multi-stack machines
Proof usesOne-step rewriting · Some finite Thue system has an undecidable word problem · Decidability transfers along mapping reductions

DefinitionImage of a PCP instance under a word map#✓fully proved

Given a map \(f\) from words over \(\alpha\) to words over \(\beta\) and a list \(P\) of dominoes over \(\alpha\), the image of \(P\) under \(f\) is the list of dominoes over \(\beta\) obtained by replacing each domino \((u, v)\) of \(P\) by \((f(u), f(v))\), in the same order.

def mapInstance (f : List α → List β) (P : List (Domino α)) : List (Domino β) :=
  P.map fun d ↦ (f d.1, f d.2)
Uses 1 · Used by 2
Statement usesDomino (Post correspondence problem)
Used byPCP over a finite alphabet many-one reduces to PCP over the binary alphabet · An injective word homomorphism preserves and reflects PCP solvability

TheoremAn injective word homomorphism preserves and reflects PCP solvability#✓fully proved

Let \(h\) map each letter of \(\alpha\) to a word over \(\beta\), and extend it to words by \(h(a_1 \cdots a_n) = h(a_1) \cdots h(a_n)\). If this extension is injective on words over \(\alpha\), then for every list \(P\) of dominoes over \(\alpha\), the list obtained from \(P\) by replacing each domino \((u, v)\) by \((h(u), h(v))\) has a PCP solution if and only if \(P\) has a PCP solution.

theorem pcp_map_iff {h : α → List β} (hinj : Function.Injective fun w : List α ↦ w.flatMap h)
    (P : List (Domino α)) : PCP (mapInstance (fun w ↦ w.flatMap h) P) ↔ PCP P
Uses 6 · Used by 1
Statement usesDomino (Post correspondence problem) · The Post correspondence problem · Image of a PCP instance under a word map
Proof usesPCP solution · Bottom word of a domino sequence · Top word of a sequence of dominoes
Used byPCP over a finite alphabet many-one reduces to PCP over the binary alphabet

DefinitionUnary code of a letter#✓fully proved

Given an indexing \(e\) assigning a natural number to each letter of \(\alpha\), the unary code of a letter \(a\) is the Boolean word consisting of \(e(a)\) copies of \(\mathrm{true}\) followed by one \(\mathrm{false}\); writing \(1\) for true and \(0\) for false, it is \(1^{e(a)} 0\).

def unaryCode (e : α → ℕ) (a : α) : List Bool := List.replicate (e a) true ++ [false]
Used by 2
Used byPCP over a finite alphabet many-one reduces to PCP over the binary alphabet · The unary code of an injective indexing is uniquely decodable

TheoremThe unary code of an injective indexing is uniquely decodable#✓fully proved

Let \(e\) be an injective map from \(\alpha\) to the natural numbers, and let \(c(a)\) be the unary code of a letter \(a\): \(e(a)\) copies of \(\mathrm{true}\) followed by one \(\mathrm{false}\). Then the map sending a word \(a_1 \cdots a_n\) over \(\alpha\) to the Boolean word \(c(a_1) \cdots c(a_n)\) is injective.

theorem unaryHom_injective {e : α → ℕ} (he : Function.Injective e) :
    Function.Injective fun w : List α ↦ w.flatMap (unaryCode e)
Uses 1 · Used by 1
Statement usesUnary code of a letter
Used byPCP over a finite alphabet many-one reduces to PCP over the binary alphabet

TheoremPCP over a finite alphabet many-one reduces to PCP over the binary alphabet#✓fully proved

Let \(\alpha\) be a finite alphabet with a primitive recursive encoding of its letters as natural numbers. Then the Post correspondence problem over \(\alpha\) is many-one reducible to the Post correspondence problem over the two-letter alphabet of Booleans \(\mathrm{true}\) and \(\mathrm{false}\): there is a computable map \(f\) sending each finite list \(P\) of dominoes over \(\alpha\) to a finite list \(f(P)\) of dominoes over the Booleans such that \(P\) has a PCP solution if and only if \(f(P)\) has a PCP solution.

theorem manyOneReducible_pcp_bool [Finite α] [Primcodable α] :
    ManyOneReducible (PCP (α := α)) (PCP (α := Bool))
Uses 6 · Used by 1
Statement usesDomino (Post correspondence problem) · The Post correspondence problem
Proof usesImage of a PCP instance under a word map · An injective word homomorphism preserves and reflects PCP solvability · Unary code of a letter · The unary code of an injective indexing is uniquely decodable
Used byThe Post correspondence problem is undecidable over the binary alphabet

TheoremThe Post correspondence problem is undecidable over the binary alphabet#✓fully proved

The Post correspondence problem over the two-letter alphabet of Booleans \(\mathrm{true}\) and \(\mathrm{false}\), that is, the property of a finite list \(P\) of dominoes over the Booleans of having a PCP solution, is not decidable by a multi-stack Turing machine: no multi-stack machine computes a total function \(g : \mathbb{N} \to \mathbb{N}\) such that, for every such \(P\) with natural-number encoding \(n_P\), \(g(n_P) = 1\) exactly when \(P\) has a PCP solution.

theorem not_tm2Decidable_pcp_bool : ¬TM2Decidable (PCP (α := Bool))
Uses 6
Statement usesDomino (Post correspondence problem) · The Post correspondence problem · Decidability by multi-stack machines
Proof usesPCP over a finite alphabet many-one reduces to PCP over the binary alphabet · The Post correspondence problem is undecidable · Decidability transfers along mapping reductions
79 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.