10
$\begingroup$

The transducers considered here are those Wikipedia calls finite state transducers. 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 of number theoretic problems in general and a highly-studied one, Collatz conjecture, in particular.

|cite|improve this question
$\endgroup$
  • 2
    $\begingroup$ ps (should have mentioned, as long known) FSM transducers are powerful enough to compute single iterations of TM "instantaneous descriptions". hence the problem seems possibly to relate to LBAs and CSLs. $\endgroup$ – vzn Oct 16 '15 at 17:09
  • $\begingroup$ 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. $\endgroup$ – Michaël Cadilhac Oct 16 '15 at 23:06
  • $\begingroup$ $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. $\endgroup$ – vzn Oct 16 '15 at 23:34
  • $\begingroup$ 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. $\endgroup$ – Michaël Cadilhac Oct 16 '15 at 23:41
  • $\begingroup$ 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. $\endgroup$ – vzn Oct 17 '15 at 0:48
8
$\begingroup$

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.

|cite|improve this answer
$\endgroup$
  • 1
    $\begingroup$ It looks from the description that it’s even decidable in NL (hence in P), assuming $L$ is given by a FSA. $\endgroup$ – Emil Jeřábek Oct 17 '15 at 17:32
  • $\begingroup$ 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: 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 $\endgroup$ – Marzio De Biasi Oct 17 '15 at 18:50
  • 1
    $\begingroup$ @EmilJeřábek Indeed, it is quite clearly in co-NL (hence in NL). $\endgroup$ – Michaël Cadilhac Oct 18 '15 at 9:59
  • $\begingroup$ @MarzioDeBiasi Thanks! I indeed did not see your notice ☺ I'll work on refunding your time when I do have some ☺ $\endgroup$ – Michaël Cadilhac Oct 18 '15 at 10:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.