3
$\begingroup$

I have two questions concerning ground reachability in string and term rewriting systems.

String Rewriting Systems:

Let $\Sigma$ be a finite alphabet.

I have a set of rules $R$ of the form $a_ib_i = c_id_i$ where $a_i,b_i,c_i,d_i$ are symbols in $\Sigma$.

Problem 1: Given strings $u$ and $w$ in $\Sigma^*$ of size $n$ can $u$ be transformed into $w$ by the application of rules in $R$?

Question1: Can Problem 1 be solved in time polynomial in $n$? Note that in this case the problem is trivially decidable since the rules do not increase the size of the strings.

Term Rewriting Systems:

Now I have a ranked alphabet $\Sigma$ with function symbols of arity $0$, $1$ and $2$.

I have a set $R$ of rules of the form (where $x,y,z$ are variables and $f,g,h,k$ are function symbols)

  1. $f(x,y) = g(y,x)$
  2. $f(x,g(y,z)) = h(x,k(y,z))$

Problem 2: Given ground terms $u$ and $w$ over $\Sigma$ with $n$ leaves, can $u$ be transformed into $w$ by the application of rules in $R$?

Question 2: Can Problem 2 be solved in time polynomial in $n$? Note that decidability is also trivial here, since the rules do not increase the size of a term.

$\endgroup$
  • 1
    $\begingroup$ Problem 1 is PSPACE complete; an immediate "dirty proof" is that for - possibly increasing or decreasing - rules of max length $2$ ($a_i \to b_i, a_i \to b_i c_i, a_i b_i \to c_i d_i, a_i b_i \to c_i$) it is undecidable. But it should also be easy to build a direct reduction that simulates the behaviour of a given LBA. $\endgroup$ – Marzio De Biasi Jan 22 '16 at 13:42
  • $\begingroup$ @MarzioDeBiasi, could you please say a bit more on your proposal of proof of PSPACE completeness. I see that adding a rule of the form $a\rightarrow bc$ turns the problem undecidable since the size of the string can grow indefinitely. But I'm only interested in length preserving rules of length 2. So I don't see why the undecidability of rewriting systems with length-increasing rules would imply PSPACE completeness of those with length preserving rules. $\endgroup$ – verifying Jan 24 '16 at 23:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.