One research direction to consider is rewriting systems with orbit-finite sets of rules. There is a nice application to knot theory.
Yesterday I saw a talk by Igor Potapov (I will post a link to Igor’s slides when they are available, a paper is here), which contains an interesting application to knot theory. Namely, there exist
- A representation of knots by words over the alphabet . This representation is called Gauss word, every word in represents (not necessarily uniquely) some knot.
- A rewriting system. The rewriting rules correspond to Reidemeister moves.
such that two words represent equivalent knots if and only if one can rewrite into using the rewriting rules.
This motivates the study of orbit-finite rewriting problems. Given
- an orbit-finite set of rewriting rules (pairs of words) ;
- a source word and a target word ;
consider the following problems:
Infix rewriting. Can one go from to by doing a finite number of steps where in each step, one replaces an infix by a word such that ?
Prefix rewriting. The same as above, but only with prefixes.
Infix rewriting is undecidable already for finite alphabets, but maybe there are some restrictions which are decidable for orbit-finite alphabets. (One restriction that works for orbit-finite alphabets is that the system is commutative, i.e. it contains a rule for every two letters of the alphabet. This corresponds to Petri nets for finite alphabets, and for infinite alphabets it corresponds to some data variant of Petri nets.)
It seems likely that prefix rewriting is decidable. For finite alphabets, the set of words reachable from the source is regular. (This is essentially the set of reachable stack configurations of a pushdown automaton.) It seems to me that for orbit-finite alphabets, the set should be recognized by a nondeterministic orbit-finite automaton.
The rewriting system that is used in knot theory is even more general than infix rewriting, on the other hand it is one specific rewriting system. It might be the case that for every source word, the set of reachable word might be recognized by some kind of automaton.