<p>By a <em>transducer</em> 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 <a href="https://dl.acm.org/doi/10.1145/2984450.2984453" rel="nofollow noreferrer">this paper</a>, where they are called &quot;sequential,&quot; &quot;rational,&quot; and &quot;regular&quot; in order of increasing power).</p>
<p>Anyway, the answer is <strong>yes,</strong> these function classes admit logical characterizations. Roughly, the idea is to use the model-theoretic notion of an interpretation. Given two signatures <span class="math-container">$\Sigma$</span> and <span class="math-container">$\Gamma$</span>, an interpretation <span class="math-container">$\Sigma \to \Gamma$</span> is (roughly) a <span class="math-container">$\Gamma$</span>-definition of each symbol in <span class="math-container">$\Sigma$</span>. (This can be with respect to whatever base logic you choose.) An interpretation gives you a map between structures <em>in the other direction,</em> that is, from <span class="math-container">$\Gamma$</span>-structures to <span class="math-container">$\Sigma$</span>-structures. (Roughly: given a <span class="math-container">$\Gamma$</span>-structure, the interpretation allows us to interpret the symbols in <span class="math-container">$\Sigma$</span>.)</p>
<p>In finite model theory, strings over a fixed alphabet are identified with finite structures in a related signature. So a map from <span class="math-container">$\Gamma$</span>-structures to <span class="math-container">$\Sigma$</span>-structures becomes a function <span class="math-container">$\Gamma^\star \to \Sigma^\star$</span> (conflating alphabets and signatures).</p>
<p>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 <em>interpretations</em> capture regular <em>functions</em>. By restricting interpretations to something called &quot;order-preserving interpretations,&quot; we get <em>rational functions</em>. (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.</p>
<p><strong>Caveat:</strong> 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.</p>

CC BY-SA 4.0
2023-05-05T02:12:33.367Z
I'd also mention the correspondence between multidimensional MSO interpretations and *polyregular* functions: https://arxiv.org/abs/1905.13190
Lê Thành Dũng 'Tito' Nguyễn
CC BY-SA 4.0
2023-05-09T18:49:49.673Z
Good point. The interpretations that the authors of this paper use are (as far as I can tell) genuinely interpretations in the classical model-theoretic sense, as opposed to the interpretations I mention in my answer. The difference is whether elements of the output structure are identified with fixed-width tuples of elements of the input structure, or some fixed number of copies of elements of the input structure.
Siddharth
CC BY-SA 4.0
2023-05-01T14:52:00.953Z
2023-05-01T14:52:00.953Z
Siddharth
<p>There's a notion of &quot;regular&quot; 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 <span class="math-container">$f$</span> is &quot;regular&quot; if the set of all <span class="math-container">$(x_1,\ldots,x_n,y)$</span> with <span class="math-container">$y = f(x_1,\ldots,x_n)$</span> 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 &quot;end of word&quot; character for inputs shorter than the longest.</p>
<p>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 <span class="math-container">$a$</span>s from a word, but this function is not &quot;regular&quot; as above. Are there any interesting logical correlates of finite state transducers?</p>

<lo.logic><automata-theory><regular-language>
Logical Equivalents of Finite State Transducers
TomKern
# Logical Equivalents of Finite State Transducers

(Asked by: username_0 on 2023-04-29)

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?

**Tags:** lo.logic, automata-theory, regular-language

---

## 1 answers

### Answer by username_1 on 2023-05-01. Score: 4

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](https://dl.acm.org/doi/10.1145/2984450.2984453), 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.

> **Comments:**
> **username_2**: I'd also mention the correspondence between multidimensional MSO interpretations and *polyregular* functions: https://arxiv.org/abs/1905.13190  
> **username_1**: Good point. The interpretations that the authors of this paper use are (as far as I can tell) genuinely interpretations in the classical model-theoretic sense, as opposed to the interpretations I mention in my answer. The difference is whether elements of the output structure are identified with fixed-width tuples of elements of the input structure, or some fixed number of copies of elements of the input structure.  

---

