String rewriting systems

AbbreviationRewriting rules#✓fully proved

A rewriting rule over an alphabet \(\alpha\) is a pair \((l, r)\) of words over \(\alpha\); applying it replaces an occurrence of \(l\) by \(r\).

abbrev Rule (α : Type*) := List α × List α

Used by 48

Used byThe word aabbcc is generated by the \(a^n b^n c^n\) grammar · The word abc is generated by the \(a^n b^n c^n\) grammar · Rewriting steps preserve balancedness · Applying a production in context is a grammar step · Derivations compose under concatenation · Derivations extend by a left context · Derivations extend by a right context · Non-head or accepting cells convert to terminals · Runs of an LBA give grammar derivations · Generated form derives the initial configuration encoding · The generator derives the middle cells and itself · Replacing a block by a rule is a derivation step · Tail cells derive their activated encoding · Transitivity of grammar derivations · The eight kinds of rules of the machine-simulating rewriting system · Rewriting preserves the number of control symbols · The halting symbol erases the tape · A halted configuration rewrites to the halting word · Erasing rules · Some finite Thue system has an undecidable word problem · MPCP is undecidable · The Post correspondence problem is undecidable · Reachability for string rewriting is undecidable · The uniform word problem for Thue systems is undecidable · One machine step is one rewrite · Single-tape halting many-one reduces to string rewriting reachability · The rewriting system simulating a Turing machine · The rules for one transition · 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 · Derivations in a string rewriting system · The backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability for rules with nonempty sides many-one reduces to PCP · Rewriting steps keep the letters of the instance · Rewriting systems with nonempty sides · The total reduction of reachability with nonempty sides to MPCP · The domino of a rewriting rule · The reachability problem for string rewriting · Reachability reduces to MPCP · One-step rewriting · Letters of a rewriting instance · The word problem of a Thue system · The MPCP instance of a reachability instance

InductiveOne-step rewriting#✓fully proved

Let \(R\) be a string rewriting system, given as a list of rules. A word \(w\) rewrites to a word \(w'\) in one step of \(R\) when there are a rule \((l, r)\) of \(R\) and words \(u\) and \(v\) with \(w = u l v\) and \(w' = u r v\).

inductive Step (R : List (Rule α)) : List α → List α → Prop
  | mk {l r : List α} (u v : List α) : (l, r) ∈ R → Step R (u ++ l ++ v) (u ++ r ++ v)

Uses 1 · Used by 38

Statement usesRewriting rules

Used byThe word aabbcc is generated by the \(a^n b^n c^n\) grammar · The word abc is generated by the \(a^n b^n c^n\) grammar · Derivations preserve balancedness · One rewriting step of a grammar · Rewriting steps preserve balancedness · Applying a production in context is a grammar step · Derivations compose under concatenation · Derivations extend by a left context · Derivations extend by a right context · Non-head or accepting cells convert to terminals · Runs of an LBA give grammar derivations · Generated form derives the initial configuration encoding · The generator derives the middle cells and itself · Replacing a block by a rule is a derivation step · Tail cells derive their activated encoding · Transitivity of grammar derivations · 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 · The uniform word problem for Thue systems is undecidable · One machine step is one rewrite · Single-tape halting many-one reduces to the word problem of a fixed Thue system · 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 · Derivations in a string rewriting system · The backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Rewriting steps keep the letters of the instance · Reachability reduces to MPCP · The word problem of a Thue system

DefinitionDerivations in a string rewriting system#✓fully proved

For a list of rules \(R\), a word \(x\) derives a word \(y\) when \(x\) rewrites to \(y\) in zero or more steps of \(R\), that is, when \((x, y)\) lies in the reflexive-transitive closure of the one-step rewriting relation of \(R\).

def Derives (R : List (Rule α)) : List α → List α → Prop := Relation.ReflTransGen (Step R)

Uses 2 · Used by 23

Statement usesRewriting rules · One-step rewriting

Used byThe word aabbcc is generated by the \(a^n b^n c^n\) grammar · The word abc is generated by the \(a^n b^n c^n\) grammar · Derivation in an unrestricted grammar · Applying a production in context is a grammar step · Derivations compose under concatenation · Derivations extend by a left context · Derivations extend by a right context · Non-head or accepting cells convert to terminals · Runs of an LBA give grammar derivations · Generated form derives the initial configuration encoding · The generator derives the middle cells and itself · Replacing a block by a rule is a derivation step · Tail cells derive their activated encoding · Transitivity of grammar derivations · The halting symbol erases the tape · A halted configuration rewrites to the halting word · 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 · The backward direction of the MPCP reduction · The forward direction of the MPCP reduction · The reachability problem for string rewriting · Reachability reduces to MPCP

DefinitionThe reachability problem for string rewriting#✓fully proved

An instance \((R, x, y)\) consists of a string rewriting system \(R\), given as a list of rules, and two words \(x\) and \(y\); it is a yes-instance of the reachability problem when \(x\) rewrites to \(y\) in zero or more steps of \(R\).

def SR (I : List (Rule α) × List α × List α) : Prop := Derives I.1 I.2.1 I.2.2

Uses 2 · Used by 7

Statement usesDerivations in a string rewriting system · Rewriting rules

Used byMPCP is undecidable · The Post correspondence problem is undecidable · Reachability for string rewriting is undecidable · Single-tape halting many-one reduces to string rewriting reachability · 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

DefinitionRewriting systems with nonempty sides#✓fully proved

A string rewriting system \(R\), given as a list of rules \((l, r)\), has nonempty sides when every rule of \(R\) has a nonempty left side \(l\) and a nonempty right side \(r\).

def NonemptyRules (R : List (Rule α)) : Prop := ∀ r ∈ R, r.1 ≠ [] ∧ r.2 ≠ []

Uses 1 · Used by 6

Statement usesRewriting rules

Used byMPCP is undecidable · The Post correspondence problem is undecidable · Reachability for string rewriting is undecidable · Single-tape halting many-one reduces to string rewriting reachability · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability for rules with nonempty sides many-one reduces to PCP

23 fully proved

The dominoes

AbbreviationLifting a word to the extended alphabet#✓fully proved

A word \(a_1 \cdots a_n\) over \(\alpha\) is sent to the word \(a_1 \cdots a_n\) over the extended alphabet of \(\alpha\) in which each \(a_i\) is read as a letter.

abbrev lift (u : List α) : List (Sym α) := u.map letter

Uses 2 · Used by 8

Statement usesThe extended alphabet of the MPCP-to-PCP reduction · The alphabet inside the extended alphabet

Used byThe backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Comparing words of letters before a separator · Final domino · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · The domino of a rewriting rule · Reachability reduces to MPCP · The start domino of the reduction from reachability to MPCP

DefinitionThe start domino of the reduction from reachability to MPCP#✓fully proved

Let \(x\) be a word over an alphabet \(\alpha\), and extend \(\alpha\) by a star \(\star\) and an end marker \(\diamond\). The start domino of \(x\) has top the one-letter word \(\diamond\) and bottom the word \(\diamond x \star\), with the letters of \(x\) read as letters of the extended alphabet.

def startCard (x : List α) : Domino (Sym α) := ([endMark], endMark :: lift x ++ [star])

Uses 5 · Used by 5

Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · End marker · The star symbol · Lifting a word to the extended alphabet

Used byThe backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability reduces to MPCP · The MPCP instance of a reachability instance

DefinitionFinal domino#✓fully proved

For a word \(y\) over \(\alpha\), the final domino of \(y\) is the domino over the extended alphabet with top \(y \star \diamond\) and bottom \(\diamond\), where \(y\) is read as a word of letters, \(\star\) is the row separator and \(\diamond\) is the end marker.

def finalCard (y : List α) : Domino (Sym α) := (lift y ++ [star, endMark], [endMark])

Uses 5 · Used by 5

Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · End marker · The star symbol · Lifting a word to the extended alphabet

Used byThe backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability reduces to MPCP · The MPCP instance of a reachability instance

DefinitionThe separator domino#✓fully proved

Over the extended alphabet, that is, an alphabet \(\alpha\) together with a star \(\star\) and an end marker \(\diamond\), the separator domino has top and bottom both equal to the one-letter word \(\star\); the star separates the rows of a derivation.

def sepCard : Domino (Sym α) := ([star], [star])

Uses 3 · Used by 5

Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · The star symbol

Used byThe backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability reduces to MPCP · The MPCP instance of a reachability instance

DefinitionThe domino of a rewriting rule#✓fully proved

For a rule \((l, r)\) over an alphabet \(\alpha\), the domino of the rule has top \(l\) and bottom \(r\), read as words over the extended alphabet, that is, \(\alpha\) together with a star and an end marker.

def ruleCard (r : Rule α) : Domino (Sym α) := (lift r.1, lift r.2)

Uses 4 · Used by 5

Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · Rewriting rules · Lifting a word to the extended alphabet

Used byThe backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability reduces to MPCP · The MPCP instance of a reachability instance

DefinitionCopy domino#✓fully proved

For a letter \(a\) of \(\alpha\), the copy domino of \(a\) is the domino over the extended alphabet whose top and bottom are both the one-letter word \(a\).

def copyCard (a : α) : Domino (Sym α) := ([letter a], [letter a])

Uses 3 · Used by 5

Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · The alphabet inside the extended alphabet

Used byThe backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Reachability reduces to MPCP · The MPCP instance of a reachability instance

DefinitionLetters of a rewriting instance#✓fully proved

For an instance \((R, x, y)\) of the reachability problem, where \(R = [(l_1, r_1), \dots, (l_k, r_k)]\) is a list of rewriting rules and \(x\), \(y\) are words, the letters of the instance form the word \(l_1 r_1 l_2 r_2 \cdots l_k r_k \, x \, y\), a list in which a letter may occur several times.

def symbols (I : List (Rule α) × List α × List α) : List α :=
  I.1.flatMap (fun r ↦ r.1 ++ r.2) ++ I.2.1 ++ I.2.2

Uses 1 · Used by 6

Statement usesRewriting rules

Used byThe backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · Rewriting steps keep the letters of the instance · Reachability reduces to MPCP · The MPCP instance of a reachability instance

DefinitionThe MPCP instance of a reachability instance#✓fully proved

Let \((R, x, y)\) be an instance of the reachability problem over an alphabet \(\alpha\), where \(R = [(l_1, r_1), \dots, (l_k, r_k)]\), and write \(\#\) for the separator and \(\diamond\) for the end marker of the extended alphabet \(\mathrm{Sym}(\alpha)\), in which letters of \(\alpha\) are read as letters. Let \(a_1 \cdots a_m\) be the word \(l_1 r_1 l_2 r_2 \cdots l_k r_k \, x \, y\), the letters of the instance. The MPCP instance of \((R, x, y)\) is the list of dominoes (top word, bottom word) \((\diamond, \diamond x \#), (y \# \diamond, \diamond), (\#, \#), (l_1, r_1), \dots, (l_k, r_k), (a_1, a_1), \dots, (a_m, a_m)\), in this order. Its first domino is \((\diamond, \diamond x \#)\).

def toMPCP (I : List (Rule α) × List α × List α) : List (Domino (Sym α)) :=
  startCard I.2.1 :: finalCard I.2.2 :: sepCard :: (I.1.map ruleCard ++ (symbols I).map copyCard)

Uses 9 · Used by 5

Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · Rewriting rules · Copy domino · Final domino · The domino of a rewriting rule · The separator domino · The start domino of the reduction from reachability to MPCP · Letters of a rewriting instance

Used byThe backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Reachability with nonempty sides many-one reduces to MPCP with nonempty words · The total reduction of reachability with nonempty sides to MPCP · Reachability reduces to MPCP

Comparing words of letters with separators

TheoremLetters differ from the star#✓fully proved

For every letter \(a\) of the alphabet \(\alpha\), the symbol \(a\) of the extended alphabet of the MPCP-to-PCP reduction is different from the star \(\star\).

theorem letter_ne_star (a : α) : letter a ≠ star

Uses 3 · Used by 2

Statement usesThe extended alphabet of the MPCP-to-PCP reduction · The alphabet inside the extended alphabet · The star symbol

Used byThe backward direction of the MPCP reduction · Comparing words of letters before a separator

TheoremComparing words of letters before a separator#✓fully proved

Let \(u, v\) be words over \(\alpha\), read as words of letters, and let \(X, Y\) be words over the extended alphabet of \(\alpha\). If \(u X = v \star Y\), where \(\star\) is the row separator, then there is a word \(w\) over \(\alpha\) with \(v = u w\) and \(X = w \star Y\).

theorem exists_of_lift_append_eq {u v : List α} {X Y : List (Sym α)}
    (h : lift u ++ X = lift v ++ star :: Y) : ∃ w, v = u ++ w ∧ X = lift w ++ star :: Y

Uses 5 · Used by 1

Statement usesThe extended alphabet of the MPCP-to-PCP reduction · The star symbol · Lifting a word to the extended alphabet

Proof usesThe alphabet inside the extended alphabet · Letters differ from the star

Used byThe backward direction of the MPCP reduction

From solutions to derivations

TheoremThe backward direction of the MPCP reduction#✓fully proved

Let \((R, x, y)\) be a reachability instance and read words over \(\alpha\) as words of letters. Let \(A\) be a sequence of dominoes of the MPCP instance of \((R, x, y)\). For all words \(v, s, t\) over \(\alpha\), if \(s\) rewrites to \(t\) under \(R\) in zero or more steps and the top of \(A\) equals \(v \star t\) followed by the bottom of \(A\), where \(\star\) is the row separator, then \(s v\) rewrites to \(y\) under \(R\) in zero or more steps.

Reading the dominoes left to right, \(s\) is the part of the current row already matched, with bottoms \(t\), and \(v\) is the rest of the row still to be matched on top.

theorem derives_of_top_eq : ∀ (A : List (Domino (Sym α))), (∀ c ∈ A, c ∈ toMPCP I) →
    ∀ (v s t : List α), Derives I.1 s t → top A = lift v ++ star :: (lift t ++ bottom A) →
      Derives I.1 (s ++ v) I.2.2

Uses 20 · Used by 1

Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · Bottom word of a domino sequence · The star symbol · Top word of a sequence of dominoes · Derivations in a string rewriting system · Rewriting rules · Lifting a word to the extended alphabet · The MPCP instance of a reachability instance

Proof usesEnd marker · The alphabet inside the extended alphabet · One-step rewriting · Copy domino · Comparing words of letters before a separator · Final domino · Letters differ from the star · The domino of a rewriting rule · The separator domino · The start domino of the reduction from reachability to MPCP · Letters of a rewriting instance

Used byReachability reduces to MPCP

From derivations to solutions

TheoremRewriting steps keep the letters of the instance#✓fully proved

Let \((R, x, y)\) be an instance of the reachability problem over an alphabet \(\alpha\). If a word \(w\) rewrites to a word \(w'\) in one step of \(R\) and every letter of \(w\) is among the letters of the instance, then every letter of \(w'\) is among the letters of the instance.

theorem mem_symbols_of_step {w w' : List α} (h : Step I.1 w w')
    (hw : ∀ a ∈ w, a ∈ symbols I) : ∀ a ∈ w', a ∈ symbols I

Uses 3 · Used by 1

Statement usesRewriting rules · One-step rewriting · Letters of a rewriting instance

Used byThe forward direction of the MPCP reduction

TheoremThe forward direction of the MPCP reduction#✓fully proved

Let \((R, x, y)\) be a reachability instance and read words over \(\alpha\) as words of letters. If a word \(w\) over \(\alpha\) rewrites to \(y\) under \(R\) in zero or more steps and every letter of \(w\) occurs in a rule of \(R\), in \(x\) or in \(y\), then there is a sequence \(A\) of dominoes of the MPCP instance of \((R, x, y)\) whose top is \(w \star\) followed by the bottom of \(A\), where \(\star\) is the row separator.

theorem exists_cards_of_derives {w : List α} (h : Derives I.1 w I.2.2) :
    (∀ a ∈ w, a ∈ symbols I) → ∃ A : List (Domino (Sym α)), (∀ c ∈ A, c ∈ toMPCP I) ∧
      top A = lift w ++ star :: bottom A

Uses 19 · Used by 1

Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · Bottom word of a domino sequence · The star symbol · Top word of a sequence of dominoes · Derivations in a string rewriting system · Rewriting rules · Lifting a word to the extended alphabet · Letters of a rewriting instance · The MPCP instance of a reachability instance

Proof usesEnd marker · The alphabet inside the extended alphabet · One-step rewriting · Copy domino · Final domino · Rewriting steps keep the letters of the instance · The domino of a rewriting rule · The separator domino · The start domino of the reduction from reachability to MPCP

Used byReachability reduces to MPCP

TheoremReachability reduces to MPCP#✓fully proved

For an instance \((R, x, y)\) of the reachability problem, \(x\) rewrites to \(y\) in zero or more steps of \(R\) if and only if the MPCP instance of \((R, x, y)\) has an MPCP solution, that is, a solution that starts with its first domino.

theorem sr_iff_mpcp_toMPCP : SR I ↔ MPCP (toMPCP I)

Uses 23 · Used by 1

Statement usesThe modified Post correspondence problem · The extended alphabet of the MPCP-to-PCP reduction · Rewriting rules · The reachability problem for string rewriting · The MPCP instance of a reachability instance

Proof usesDomino (Post correspondence problem) · PCP solution · Bottom word of a domino sequence · End marker · The alphabet inside the extended alphabet · The star symbol · Top word of a sequence of dominoes · Derivations in a string rewriting system · One-step rewriting · Copy domino · The backward direction of the MPCP reduction · The forward direction of the MPCP reduction · Final domino · Lifting a word to the extended alphabet · The domino of a rewriting rule · The separator domino · The start domino of the reduction from reachability to MPCP · Letters of a rewriting instance

Used byReachability with nonempty sides many-one reduces to MPCP with nonempty words

The many-one reduction

DefinitionThe total reduction of reachability with nonempty sides to MPCP#✓fully proved

On an instance \((R, x, y)\) of the reachability problem, the reduction returns the MPCP instance of \((R, x, y)\) when every rule of \(R\) has a nonempty left side and a nonempty right side, and otherwise the empty list of dominoes, which has no solution.

def reduce (I : List (Rule α) × List α × List α) : List (Domino (Sym α)) :=
  cond (nonemptyWordsB I.1) (toMPCP I) []

Uses 5 · Used by 1

Statement usesDomino (Post correspondence problem) · The extended alphabet of the MPCP-to-PCP reduction · Boolean test for nonempty words · Rewriting rules · The MPCP instance of a reachability instance

Used byReachability with nonempty sides many-one reduces to MPCP with nonempty words

TheoremReachability with nonempty sides many-one reduces to MPCP with nonempty words#✓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 instances \((R, x, y)\) of the reachability problem over \(\alpha\), where \(R\) is a list of rewriting rules over \(\alpha\) and \(x\) and \(y\) are words over \(\alpha\), to finite lists of dominoes over \(\alpha'\) such that, for every such instance, the following are equivalent: 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\); and every domino of \(f(R, x, y)\) has a nonempty top word and a nonempty bottom word and \(f(R, x, y)\) has an MPCP solution.

theorem manyOneReducible_sr_mpcp :
    ManyOneReducible (fun I : List (Rule α) × List α × List α ↦ NonemptyRules I.1 ∧ SR I)
      (fun P : List (Domino (Sym α)) ↦ NonemptyWords P ∧ MPCP P)

Uses 23 · Used by 2

Statement usesDomino (Post correspondence problem) · The modified Post correspondence problem · Instances with nonempty words · The extended alphabet of the MPCP-to-PCP reduction · Rewriting systems with nonempty sides · Rewriting rules · The reachability problem for string rewriting

Proof usesPCP solution · End marker · The alphabet inside the extended alphabet · Boolean test for nonempty words · The nonempty-words test is primitive recursive · The star symbol · Copy domino · Final domino · Lifting a word to the extended alphabet · 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 · Letters of a rewriting instance · The MPCP instance of a reachability instance

Used byMPCP is undecidable · Reachability for rules with nonempty sides many-one reduces to PCP

TheoremReachability for rules with nonempty sides many-one reduces to PCP#✓fully proved

Let \(\alpha\) be an alphabet with a primitive recursive coding, let \(\alpha'\) be \(\alpha\) extended with two new symbols, the star and the end marker, and let \(\alpha''\) be \(\alpha'\) extended in the same way by two further new symbols. There is a computable function \(f\) from instances \((R, x, y)\) of the reachability problem over \(\alpha\), where \(R\) is a list of rewriting rules over \(\alpha\) and \(x\) and \(y\) are words over \(\alpha\), to finite lists of dominoes over \(\alpha''\) such that, for every such instance, \(f(R, x, y)\) has a PCP solution if and only if 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_sr_pcp :
    ManyOneReducible (fun I : List (Rule α) × List α × List α ↦ NonemptyRules I.1 ∧ SR I)
      (PCP (α := Sym (Sym α)))

Uses 10 · Used by 1

Statement usesDomino (Post correspondence problem) · The Post correspondence problem · The extended alphabet of the MPCP-to-PCP reduction · Rewriting systems with nonempty sides · Rewriting rules · The reachability problem for string rewriting

Proof usesThe modified Post correspondence problem · Instances with nonempty words · MPCP many-one reduces to PCP · Reachability with nonempty sides many-one reduces to MPCP with nonempty words

Used byThe Post correspondence problem is undecidable

Thue systems

DefinitionThe word problem of a Thue system#✓fully proved

On an instance \((R, x, y)\), where \(R\) is a list of rewriting rules and \(x\), \(y\) are words, the word problem asks whether \(x\) and \(y\) are related by the equivalence relation generated by the one-step rewriting relation of \(R\), that is, by its reflexive, symmetric and transitive closure.

def ThueWP (I : List (Rule α) × List α × List α) : Prop := EqvGen (Step I.1) I.2.1 I.2.2

Uses 2 · Used by 1

Statement usesRewriting rules · One-step rewriting

Used byThe uniform word problem for Thue systems is undecidable

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.