A result of Grädel and McColm shows that over finite structures, the logic DTCL is strictly less expressive than the logic TCL. My question is: can this result be translated into some separation result concerning Turing machines with atoms?
In Automata theory in nominal sets (Thm. 9.3), we provided a necessary and sufficient criterion for the existence of least finite supports for arbitrary atoms. It was not clear whether the criterion could be significantly simplified for Fraisse atoms. I show that it cannot be made as simple as we originally conjectured.
One research direction to consider is rewriting systems with orbit-finite sets of rules. There is a nice application to knot theory.
We study the relationship between standard alphabets over the equality atoms, and those which can be made homogeneous using finitely many relations and functions. We leave open the problem whether these notions coincide.
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.
We study a derivation quasi-order between between alphabets. Whenever is derived from and is non-standard then is non-standard too. We identify also a class of minimal non-standard alphabets wrt. the quasi-order.
This post discusses equivalence of:
1. existence of the least supports
2. representation theorem
Fact. Suppose that is a one-orbit set and
is an equivariant function. Then is a bijection.