Logical Equivalents of Finite State Transducers

Question

There's a notion of "regular" function on words in automata theory that corresponds nicely to functions in WS1S/Büchi Arithmetic/the logic of words with a prefix and equal-length relation. Specifically, a function $f$ is "regular" if the set of all $(x_1,\ldots,x_n,y)$ with $y = f(x_1,\ldots,x_n)$ is accepted by some DFA that reads in inputs in parallel. That is, it reads in all first characters, then all second characters, then all third characters, etc., reading in an "end of word" character for inputs shorter than the longest.

There's another notion of function in automata theory given by finite state transducers, but this is not the same. It's easy to construct a transducer that removes all $a$s from a word, but this function is not "regular" as above. Are there any interesting logical correlates of finite state transducers?

Answer 1

By a transducer I assume you mean an automaton which can print output on transitions. The extensional equivalence between deterministic and nondeterministic automata as well as 1-way and 2-way automata breaks when we pass to transducers; there are at least three robust function classes sitting on top of the regular languages (cf. Figure 3 of this paper, where they are called "sequential," "rational," and "regular" in order of increasing power).

Anyway, the answer is yes, these function classes admit logical characterizations. Roughly, the idea is to use the model-theoretic notion of an interpretation. Given two signatures $\Sigma$ and $\Gamma$, an interpretation $\Sigma \to \Gamma$ is (roughly) a $\Gamma$-definition of each symbol in $\Sigma$. (This can be with respect to whatever base logic you choose.) An interpretation gives you a map between structures in the other direction, that is, from $\Gamma$-structures to $\Sigma$-structures. (Roughly: given a $\Gamma$-structure, the interpretation allows us to interpret the symbols in $\Sigma$.)

In finite model theory, strings over a fixed alphabet are identified with finite structures in a related signature. So a map from $\Gamma$-structures to $\Sigma$-structures becomes a function $\Gamma^\star \to \Sigma^\star$ (conflating alphabets and signatures).

Anyway, so now we just have to choose the right logic with the right type of interpretation (there are various kinds). Just as spectra of MSO sentences capture regular languages over strings, MSO interpretations capture regular functions. By restricting interpretations to something called "order-preserving interpretations," we get rational functions. (Note that fragments of MSO work too, in particular monadic LFP.) There is a way to get sequential functions too using, again, order preserving interpretations with respect to a fragment of MSO.

Caveat: there are small but important technical differences, which I'm shoving under the rug, between interpretations in model theory and those in formal language theory.