# Standard alphabets beyond equality atoms

In this post, I try to give a characterization of standard alphabets (i.e. alphabets where Turing machines determinize) which works for many choices of atoms.

Theorem. Assume that the atoms are oligomorphic, have a decidable first-order theory, and for every one can compute the number of orbits of -tuples of atoms. The following conditions are equivalent for every orbit finite set .

1. Turing machines over input alphabet determinize
2. There exists a function   which is computable by a deterministic Turing machine, and such that two words are in the same orbit if and only if they have the same image under .

Proof. I assume that is equivariant, and the Turing machines in items 1 and 2 are also equivariant.  Let us begin by introducing some notation. For an equivariant orbit-finite set , define a representation to be any equivariant partial function

Every  equivariant orbit-finite set has at least one representation.  By oligomoprhism, the kernel of , which is an equivariant parital equivalence relation on -tuples of atoms, is  first-order definable, by a formula with variables.  For , let

be the lifting of to tuples of atoms of length , obtained  by applying   to the first atoms of the input, then the next atoms of the input, and  so on times.  Again, the kernel of is first-order definable, and the formula can be computed given .

Definition. Let be a representation of . Define a -deatomization of a word to be a first-order formula defining an orbit of which cotnains some word such that .

Under some representation of  first-order logic formulas as bit strings, one can see an -representation as a bit string. Define the canonical -deatomization to be function

which maps a word to its lexicographically smallest -deatomization. We claim that conditions 1 and 2 in the theorem are equivalent to

3. for some (equivalently, every) representation , the canonical -deatomization is computed by some deterministic Turing machine.

To prove the equivalence of 1,2 and 3, we use the following lemma, which lifts computation of Turing machines from words with atoms to their deatomized versions.

Lemma. Let be orbit-finite sets with atoms, with representations . Then for every relation

computed by a (possibly nondeterministic) Turing machine, there exists a relation

computed by a (possibly nondeterministic) Turing machine, such that . Diagrammatically

Proof of the lemma. By simulating the logic of the Turing machine. The proof uses the assumptions on decidability of first-order theory and computing the number of orbits.

1 implies 2. It is straightforward to see that a nondeterministic Turing machine can compute the canonical deatomization . Assumption 1 says that machines can be determinized, and therefore there is a deterministic Turing machine computing . This proves 3, which immediately implies 2.

2 implies 3.  Suppose that is computed by some deterministic Turing machine. Let

be obtained by applying the lemma to . To compute  , we  do the following: enumerate all possible strings in until finding a string such that . This string is .

3 implies 1. Using the lemma, the whole computation can be done without atoms.

This completes the proof of the theorem.

Question: Are conditions 1,2 and 3 equivalent to the following condition 4?

4. There is a deterministic Turing machine recognizing

In general, 2 implies 4, because to test if and are in the same orbit, it suffices to check if they have the same image under . For the converse implication, from 4 to 2, some kind of fresh-elimination procedure would be useful.