There are several decision problems for certain computation models with atoms that are decidable when atoms admit certain well quasi order (WQO), and undecidable otherwise. We recall the problems and formulate few questions related to WQOs.
A conjecture I posted a while ago, concerning reachability of states in automata with atoms after a Brzozowski phase, has been refuted by Mikołaj Bojańczyk.
One research direction to consider is rewriting systems with orbit-finite sets of rules. There is a nice application to knot theory.
Fix attention on equality atoms.
Given an orbit-finite, deterministic automaton on the alphabet of atoms, a Brzozowski phase amounts to:
- reversing the direction of all transition arrows and swapping initial and accepting states,
- determinising the result, and
- cutting to the reachable part.
This is a straightforward generalization of the classical Pumping Lemma for regular languages. It was proved independently by the Warsaw team and by Filippo Bonchi, Daniela Petrisan and Alexandra Silva.