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
.
- Turing machines over input alphabet
determinize
- 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.