<p><em>The other contributor deleted his answer, maybe to let me extend my above comment, so here it is.</em></p>

<p>Let $T$ be a possibly nondeterministic transducer, and $L$ be a regular language.  Modify $T$ into a transducer $T'$ that checks that its input is in $L$ (by, e.g., changing the state set into the Cartesian product of the state sets of  $T$ and $L$, and modifying the transition function so that the $L$ part of the states is properly updated, while retaining the behavior of $T$.)</p>

<p>A <em>branch</em> of $T'$ is a sequence $\rho_1 C_1\rho_2 C_2 \cdots \rho_n C_n \rho_{n+1}$ such that $\rho_1\rho_2 \cdots \rho_{n+1}$ is an accepting simple path in $T'$, and each $C_i$ is a strongly connected component of $T'$ the states of which include the destination of $\rho_i$ (and the origin of $\rho_{i+1}$).  The branch is <em>tame</em> if:</p>

<ol>
<li><p>The input length of the path $\rho_1\rho_2\cdots\rho_{n+1}$ is greater than or equal to its output length;</p></li>
<li><p>For any $i$, any simple cycle in $C_i$, the input length of the cycle is greater than or equal to its output length.</p></li>
</ol>

<p><strong>Fact:</strong> $\big[$ For any $x, y$, $x[T']y$ implies $|y| \leq |x|$ $\big]$ iff all branches are tame.</p>

<p>The proof is rather immediate.  The latter property being decidable (as the number of branches is bounded, and the number of simple cycles too), this shows that the problem of the question is decidable.</p>

CC BY-SA 3.0
2015-10-17T17:32:03.920Z
It looks from the description that it’s even decidable in NL (hence in P), assuming $L$ is given by a FSA.
Emil Jeřábek
CC BY-SA 3.0
2015-10-17T18:50:03.637Z
I sent you a notice (sorry I didn't read carefully your comment before posting) but probably you didn't receive it after the deletion of the answer :-) ... but now - as a time refund - you should switch to (and solve!) this trickier one: "[Open problem](http://arxiv.org/pdf/1008.1667.pdf): Does there exist $n \geq 1$ and a computable encoding $S_n$ such that, for all $k \geq 1$, $L^{S_n}_{\leq n} = L^{S_n}_{\leq n+k}$?" :-D :-D
Marzio De Biasi
CC BY-SA 3.0
2015-10-18T09:59:23.777Z
@EmilJeřábek Indeed, it is quite clearly in co-NL (hence in NL).
Michaël Cadilhac
CC BY-SA 3.0
2015-10-18T10:00:56.947Z
@MarzioDeBiasi Thanks!  I indeed did not see your notice ☺ I'll work on refunding your time when I do have some ☺
Michaël Cadilhac
CC BY-SA 3.0
2015-10-17T17:22:37.537Z
2015-10-17T17:22:37.537Z
Michaël Cadilhac
<p>The transducers considered here are those Wikipedia calls <a href="https://en.wikipedia.org/wiki/Finite_state_transducer">finite state transducers</a>.  The behavior of a transducer $T$, that is, the relation it computes, is written $[T]$: a word $y$ is an output for $x$ iff $x[T]y$.</p>

<p><em>Question:</em> Is the following problem decidable:</p>

<blockquote>
  <p>Given: A transducer $T$ and a regular language $L$<br/>
  Decide: Does it hold that $\forall x \in L$, $\forall y$ a word, $x[T]y$ implies that $|y| \leq |x|$?</p>
</blockquote>

<p>I'm looking for nontrivial analysis/solvable subcases, reduction to known problems and/or related refs. (right now not even sure it is decidable in general...?)</p>

<p><em>Motivation:</em> this problem was inspired by analysis/inquiry into <a href="https://en.wikipedia.org/wiki/Automated_theorem_proving">automated theorem proving</a> of number theoretic problems in general and a highly-studied one, <a href="https://en.wikipedia.org/wiki/Collatz_conjecture">Collatz conjecture</a>, in particular.</p>

CC BY-SA 3.0
2015-10-16T17:09:55.663Z
ps (should have mentioned, as long known) FSM transducers are powerful enough to compute single iterations of TM ["instantaneous descriptions"](https://en.wikipedia.org/wiki/Turing_machine#The_.22state.22). hence the problem seems possibly to relate to [LBAs](https://en.wikipedia.org/wiki/Linear_bounded_automaton) and [CSLs](https://en.wikipedia.org/wiki/Context-sensitive_language).
vzn
CC BY-SA 3.0
2015-10-16T23:06:50.390Z
By $|F(x)|$ you speak of the number of outputs on input $x$, right?  Not the size of the outputs, in which case it'd be quite straightforward.
Michaël Cadilhac
CC BY-SA 3.0
2015-10-16T23:34:00.867Z
$x, F(x)$ are both words and $|F(x)|$ is the length of the "output" word. have some ideas but dont see anything straightfwd at moment hence the question. its presumably nontrivial due eg to $\epsilon$ inputs/ outputs on some transitions etc.
vzn
CC BY-SA 3.0
2015-10-16T23:41:20.587Z
So you implicitly assume that your transducer is functional—notation-wise, it wasn't clear to me :-)  So what about the following: Let $T$ be a (possibly nondeterministic) transducer and $L$ be a given regular language.  Modify $T$ into a transducer $T'$ so that it checks whether its input is in $L$, and all its states are reachable and co-reachable.  Then $|T(w)| \leq |w|$ for all $w \in L$ iff there is no simple cycle in the transducer $T'$ for which the input is smaller than the output, and some additional easy properties on the transitions not appearing in any SCC.
Michaël Cadilhac
CC BY-SA 3.0
2015-10-17T00:48:26.720Z
ok. for "input is smaller than the output" you mean over the cycle? think this is worth writing up as answer. there was another different way to formulate this/ related problem with stricter criteria which is presumably not (as) easy, maybe will try again on that ("part 2/ sequel/ followup") if your answer seems correct. this current problem is probably nearly a special case of the broader problem.
vzn
<ds.algorithms><reference-request><automata-theory><regular-language><dfa>
Is it decidable whether the output length of a transducer is bounded by the input length?
vzn
# Is it decidable whether the output length of a transducer is bounded by the input length?

(Asked by: username_0 on 2015-10-16)

The transducers considered here are those Wikipedia calls [finite state transducers](https://en.wikipedia.org/wiki/Finite_state_transducer). The behavior of a transducer $T$, that is, the relation it computes, is written $[T]$: a word $y$ is an output for $x$ iff $x[T]y$.

*Question:* Is the following problem decidable:

> Given: A transducer $T$ and a regular language $L$  
> Decide: Does it hold that $\forall x \in L$, $\forall y$ a word, $x[T]y$ implies that $|y| \leq |x|$?

I'm looking for nontrivial analysis/solvable subcases, reduction to known problems and/or related refs. (right now not even sure it is decidable in general...?)

*Motivation:* this problem was inspired by analysis/inquiry into [automated theorem proving](https://en.wikipedia.org/wiki/Automated_theorem_proving) of number theoretic problems in general and a highly-studied one, [Collatz conjecture](https://en.wikipedia.org/wiki/Collatz_conjecture), in particular.

**Tags:** ds.algorithms, reference-request, automata-theory, regular-language, dfa
> **Comments:**
> **username_0**: ps (should have mentioned, as long known) FSM transducers are powerful enough to compute single iterations of TM ["instantaneous descriptions"](https://en.wikipedia.org/wiki/Turing_machine#The_.22state.22). hence the problem seems possibly to relate to [LBAs](https://en.wikipedia.org/wiki/Linear_bounded_automaton) and [CSLs](https://en.wikipedia.org/wiki/Context-sensitive_language).  
> **username_1**: By $|F(x)|$ you speak of the number of outputs on input $x$, right?  Not the size of the outputs, in which case it'd be quite straightforward.  
> **username_0**: $x, F(x)$ are both words and $|F(x)|$ is the length of the "output" word. have some ideas but dont see anything straightfwd at moment hence the question. its presumably nontrivial due eg to $\epsilon$ inputs/ outputs on some transitions etc.  
> **username_1**: So you implicitly assume that your transducer is functional—notation-wise, it wasn't clear to me :-)  So what about the following: Let $T$ be a (possibly nondeterministic) transducer and $L$ be a given regular language.  Modify $T$ into a transducer $T'$ so that it checks whether its input is in $L$, and all its states are reachable and co-reachable.  Then $|T(w)| \leq |w|$ for all $w \in L$ iff there is no simple cycle in the transducer $T'$ for which the input is smaller than the output, and some additional easy properties on the transitions not appearing in any SCC.  
> **username_0**: ok. for "input is smaller than the output" you mean over the cycle? think this is worth writing up as answer. there was another different way to formulate this/ related problem with stricter criteria which is presumably not (as) easy, maybe will try again on that ("part 2/ sequel/ followup") if your answer seems correct. this current problem is probably nearly a special case of the broader problem.  

---

## 1 answers

### Answer by username_1 on 2015-10-17. Score: 8 | Accepted answer

*The other contributor deleted his answer, maybe to let me extend my above comment, so here it is.*

Let $T$ be a possibly nondeterministic transducer, and $L$ be a regular language. Modify $T$ into a transducer $T'$ that checks that its input is in $L$ (by, e.g., changing the state set into the Cartesian product of the state sets of $T$ and $L$, and modifying the transition function so that the $L$ part of the states is properly updated, while retaining the behavior of $T$.)

A *branch* of $T'$ is a sequence $\rho\_1 C\_1\rho\_2 C\_2 \cdots \rho\_n C\_n \rho\_{n+1}$ such that $\rho\_1\rho\_2 \cdots \rho\_{n+1}$ is an accepting simple path in $T'$, and each $C\_i$ is a strongly connected component of $T'$ the states of which include the destination of $\rho\_i$ (and the origin of $\rho\_{i+1}$). The branch is *tame* if:

1. The input length of the path $\rho\_1\rho\_2\cdots\rho\_{n+1}$ is greater than or equal to its output length;
2. For any $i$, any simple cycle in $C\_i$, the input length of the cycle is greater than or equal to its output length.

**Fact:** $\big[$ For any $x, y$, $x[T']y$ implies $|y| \leq |x|$ $\big]$ iff all branches are tame.

The proof is rather immediate. The latter property being decidable (as the number of branches is bounded, and the number of simple cycles too), this shows that the problem of the question is decidable.

> **Comments:**
> **username_2**: It looks from the description that it’s even decidable in NL (hence in P), assuming $L$ is given by a FSA.  
> **username_3**: I sent you a notice (sorry I didn't read carefully your comment before posting) but probably you didn't receive it after the deletion of the answer :-) ... but now - as a time refund - you should switch to (and solve!) this trickier one: "[Open problem](http://arxiv.org/pdf/1008.1667.pdf): Does there exist $n \geq 1$ and a computable encoding $S_n$ such that, for all $k \geq 1$, $L^{S_n}_{\leq n} = L^{S_n}_{\leq n+k}$?" :-D :-D  
> **username_1**: @EmilJeřábek Indeed, it is quite clearly in co-NL (hence in NL).  
> **username_1**: @MarzioDeBiasi Thanks!  I indeed did not see your notice ☺ I'll work on refunding your time when I do have some ☺  

---

