We have the following task:

Take as input a finite set of string pairs. Each pair represents a substitution. Replace exactly one instance of the left with the right. A substitution can only be performed on x if the left is a substring of x. For example $01rightarrow 10$ means replace one 01 with 10, and can only be applied if 01 is in the string. The algorithm should decide if for the given set there exists a string such that applying a non – zero number of the substitutions yields the initial string.

I am wondering if this is a decidable task. It seems like it should be possible to establish an upper bound on the length of the string and number of substitutions, but I haven’t been able to. And from the other end I tried to build a test based on invariants, since invariants can be used to show a lot of sets can’t loop. For example

$$

{011rightarrow 101, 101rightarrow 110}

$$

Can never produce a loop. We can show this since each rule decreases the average position of 1s in the string when used. Thus it can never produce a string with the same average position as the start thus it can never produce the start.

But there are some cases that I can’t think of a clever invariant. For example

$$

{1001rightarrow 0110}

$$

Which clearly can’t form a loop, but I can’t think of a property which it always increases.

Is this problem decidable?