In this post, all relations are over finite words with finite alphabets.
Automatic relations. A
regular n-ary relation can is the set of
n-tuples recognisable by a DFA over $\Sigma^n$. Hence all words related by a regular relation have the same length.
Automatic relations are regular relations augmented with a special symbol $\bot$ that is used to indicate tail spaces. For example, a binary automatic relation $R$ relates two words $w$ and $w'$ iff $(w\bot^n,w'\bot^m)\in R$ for all $n,m\ge 0: |w|+n=|w'|+m$. In this way an automatic binary relation allows for the existence of an infinite sequence $w_0,w_1,...$ with $w_0\ R\ w_1\ R\ w_2...$ and $|w_0|<|w_1|<...$.
Examples. The following binary relations are automatic: lexicographic ordering, bitwise operations on binary strings, rational number ordering, "a subword of" over a unary alphabet, length ordering, and the edge relation of the configuration space of a TM.
Automatic structures. Recall that a structure $A$ is a tuple $(D; R_1, . . . , R_m)$ where $D$ is a non-empty set called the domain and $R_1,...,R_m$ are basic (or atomic) relations on $D$.
Theorem. (Hodgson 1982)
The first-order theory of any automatic structure is decidable.
More precisely, there is an algorithm that given a FO formula $\phi(x_1,...,x_n)$ and an automatic structure $A$, produces a DFA $A_\phi$ recognising the tuples $(a_1,...,a_n)$ that satisfies the formula in $A$. This can be shown by induction on the structure of the formula, using the fact that automata recognisable relations are closed under the Boolean operations and the projection operations. This automata construction also indicates a connection between automatic structures and FO-definable structures, namely,
Corollary. A structure first-order definable in an automatic structure is automatic.
Rational & regular relations. Rational relations are language recognised by finite state transducers over alphabet $(\Sigma\cup\{\epsilon\})\times(\Sigma\cup\{\epsilon\}).$ Rational relations can encode computations of TMs. Regular relations are exactly the rational relations that preserve lengths.
Examples. The following relations are rational but not automatic: "a subword of", "a prefix of", etc.
Fact. Determinisation of transducer is not always possible and the result may not be unique. In fact it is undecidable as for whether a rational relation has a deterministic transducer.
Fact. Rational relations are not closed under complementation and intersection.
Fact. A rational relation can be recognised by a finite transducer on $(\Sigma_\epsilon)\times(\Sigma_\epsilon)$.
Resources
1.
Uniformization in Automata Theory, Arnaud Carayol
2.
Three Lectures on Automatic Structures, Bakhadyr Khoussainov and Mia Minnes.
