Check if a string substitution rule will ever generate another string

Question

Not homework.

Given two strings S and T of same length. Given a set of replacement rules, that find substring A in S and replace it with string B. A and B have the same length.

Is there a sequence of rule application, such that it make string S into string T?

Example: We have replacement rules

cat->dog
dog->cut

we have string S1:awesomecat and S2:awesomecut

A sequence of replacement can be

awesomecat 
awesomedog cat->dog
awesomecut dog->cut

That's a easy example, it's possible there are rules like this.

cat->dog
ate->dog
dog->cat

I believe there is no better way to answer this than try every single rule in every single state. Which would be exponential time. But I don't know if there are better solutions to it.

Answer 1

I recommend you read Godel, Escher, Bach =) It discusses exactly what you are describing here.

In conclusion, one solution proposed is to find an invariant to your system: a property that, if true at the start of the manipulations, must in all cases also be true at the end of your manipulations.

If your first string possess that invariant, and your ending string does not, then your substitution rule will never generate the second string.

Your invariant rule can be more powerful...for example, it can be an if and only if relationship (an invariant is true in the end step if and only if it is true at the first step), so you can prove that the end string is unreachable if there is an invariant that is not true in the first string. Note that these if and only if relationships follow automatically from the standard if relationships if all of your rules work both way (you can apply them backwards and forwards)

For example, here is a possible invariant in your first system:

• All contiguous strings not containing the contiguous string combination 'cat' or 'dog' within them must also be present at the end state

Given that invariant rule, it is straightforward to provide a decision formula to decide whether or not a string is possible given a starting string.

---

append

I hope you don't mind if I adopt Hofstadter's terms, in that:

• A given, starting string will be called an 'axiom'
• Axioms may be acted on by a set of rules
• Any string of letters is called a 'theorem'; a string of letters that can be produced by the rules from the given axioms is called a 'valid theorem'

So, your question moves from "can X produce Y?" to "is Y a valid theorem, derivable from X?"

So, let's approach your string substitution problem from a more general terms. We will call A the ordered set of all substituted strings, and A the ordered set of all substituting strings. Therefore, here we have our single generalized rule:

"xA[n]y" => "xB[n]y"

This says, "If ever we see a theorem with a string in set A, surrounded by strings x and y, then we may derive, also, xB[n]y, where B[n] is the corresponding substituting string.

Let's find some invariants, that are true, regardless of what is in sets A and B.

• As a consequence of your substituting strings always being the same length as their substituted string, any letter in an axiom that is not found in in A must not move

For example, if we have axiom abcdea, and ruleset A=["cd",de"], it's easy to see that the letters a and b are not found in A. Therefore, we can say that all theorems in this system must be of the form ab##a. This gives us a rule to find what is not a theorem.

However, for very long sets A, this might not help us that much, for A might conceivably use all letters.

Let's try making this more useful...

• Any letter at the end of an axiom, that is not at the end of a string in A, cannot move. The same can be said for any letter at the beginning of an axiom, that is not at the beginning of a string in A.

Let's say we have A=["dog","cat","ton"], any if an axiom ends in any letter that is not g, t, or c, all derivable theorems must also end in the same letter. If an axiom begins with any letter not d, c, or t, all derivable theorems must also begin with the same letter, as well.

This is somewhat more useful, because for any A with a size < 26, you will have letters that they do not end or begin with. However, it becomes a lot less likely for your axioms to begin or end with those specific letters.

However, we find that we can extend this further:

• Any continuous string of letters at the beginning of an axiom that is not a continuous string at the beginning of a string in A must not move; the same for a continuous string at the end of an axiom that is not a continuous string at the end of a string in A.

We'll find that this is a lot more useful! A has to be at least 26^n elements large for us to dismiss this invariant as useless.

Now, note, we can go backwards, too! That is, we can say:

• Any continuous string of letters at the beginning of a theory that is not a continuous string at the beginning of a string in B must also be there in all axioms; the same for a continuous string at the end of a theorem that is not a continuous string at the end of a string in B.

With those rules, I've assembled a decision tree for figuring out which cases we have locked, and which cases are indeterminable. You'll notice that we only have two such indeterminable cases.

Now all that's left is to find an invariant of the those two cases. However, we can notice one thing:

• An invariant rule to CASE 2 can also be applied to CASE 1, with the leading/trailing "not-in-A/B" strings ignored

That is, if you have A=["cat","dog"],B=["dog","cut"], and axiom-theorem boabcdut boablmut, then any invariant rules you have that you can apply to CASE 2's can also be applied to cdut => mlut, with the non-matching leading string boab ignored. This simplifies things considerably.

So, we've basically resolved both undetermined case to one case; let's see what else we can analyze...

...another time. I'll get back to this in a bit.

Answer 2

You can easily map this problem to a directed graph in which all rules are directed paths from one node to another.

Upon receiving inputs A and B, check the diff between them, and see if you have a path along the graph that yields expected result.