this is a followup/ sequel to this recent question which was answered, this one presumably significantly harder. consider a deterministic FSM transducer $F$ and its mapping $F(x)$ of an input word $x$. define a sequence/ composition of such mappings $x_n = F(\ldots F(x_1))$ where $F^n(x)$ is $n$ sequential mappings of $x$. the sequence terminates if/ "at the point" that $F(x_n)$ is unaccepted (by the FSM transducer).

now consider/ define a property of such sequences "descending". a FSM sequence $x_i$ is "descending" iff $|x_i| \geq |x_{i + 1}|$ where $|x|$ denotes word length, and for all $i,j$, $x_i \neq x_j$. (by defn all such sequences must be finite/ terminating.)

question: given an input regular language $L$ and a FSM transducer $F$. is it decidable if all sequences $x_n = F^n(x) = F(\ldots F(x))$ for all $x \in L$ are descending?

a complete answer would be ideal but prefer partial answer(s) to none at all. looking for nontrivial analysis, reduction(s) to known problems, refs to related literature etc.

motivation/ background: a long story, but inspired/ related to investigation of a highly studied open number theory problem. the basic idea is to look for/ formulate a generalized loop invariant function applicable to automated theorem proving.

  • 2
    $\begingroup$ The transductions defined by deterministic 2-way FSM transducers are exactly those recognized by SMO. Descending sequences seem to be definable with a transitive closure operator. So I guess your problem is PSPACE. I do not have time to elaborate right now, but I certainly will during the week-end. $\endgroup$
    – Boson
    Oct 23, 2015 at 17:48
  • $\begingroup$ sounds promising... "SMO," do you mean 2nd order logic ("MSOL")? $\endgroup$
    – vzn
    Oct 23, 2015 at 20:23
  • $\begingroup$ $n$ is not given as a parameter. the sequences may have arbitrary/ varying lengths. (maybe there is some other way to bound it...?) $\endgroup$
    – vzn
    Oct 23, 2015 at 21:52
  • $\begingroup$ I gave a quick answer, but I have another question: do you require that $x, F(x), F^2(x), ..., F^{n-1} \in L$, until $F^n(x) \notin L$ ? In other words, all the intermediate "steps" must be in $L$? $\endgroup$ Oct 23, 2015 at 23:24
  • $\begingroup$ the intermediate words may or may not be in L. still parsing/ thinking over your answer & will probably respond later. wrt it (and "hint") the problem seems only applicable (or maybe nearly? or exactly? equivalent) to TM "runs" that do not move outside their initial input tapes. and the problem of detecting whether a TM eventually halts not moving off of a single given input tape is decidable (and related to CSL recognition). $\endgroup$
    – vzn
    Oct 23, 2015 at 23:30

2 Answers 2


The problem seems undecidable: consider a transducer $F$ that parses and "executes" a single step of a Turing machine $M$ with the head $H$ on symbol $a$, in state $S$ and with tape content $x[a]by$ where $a,b \in \Sigma; x,y \in \Sigma^*$:

$$\# x \, a \, H\, S \, b \, y \, \# \, w $$

where $w \in \{0,1\}^+$ and it outputs

$$\# x \, H \, S' \, a'\, b \, y \, \# \, w' $$

if the head moves left, i.e. $\sigma(a,S)\to (a',S',L)$ or it outputs

$$\# x \, a' \, b \, H \, S' \, y \, \# \, w' $$

if the head moves right, i.e. $\sigma(a,S)\to (a',S',R)$.

$w'$ is simply $w +1$ (binary addition with the LSB on the left) and its "role" is to make $x_{i+1} \neq x_j \forall j \leq i$ as required.

If $M$ halts (when $S'$ is a final state), then $F$ adds an extra $\#$ at the end (i.e. it makes the output ascending) and rejects to stop the sequence; otherwise it accepts and the length is unaltered.

If there is not enough space for a right move of the head then $F$ rejects to stop the sequence.

If there is not enough space for writing $w+1$ (carry overflow on the right), it simply replaces the last digit with $\#$ (to make $x_{i+1} \neq x_i$) and rejects to stop the sequence.

Note that:

  1. $F$ needs only a limited look-ahead buffer (4 symbols) to make the rewrite and also to perform the $w+1$ operation;
  2. the internal states of $F$ embeds the internal states of $M$ so it can simulate the transition function $\sigma$;

Now, consider $M$ on an empty tape; we can use an (infinite) regular language:

$L = \{ \# \, H \, S_0\, \, 0^+ \# \, 0^+ \}$

$M$ halts if and only if $F^n(x)$ is not descending for all $n$, for all $x \in L$

Indeed the only length increase occurs when $F$ runs on $\# \, H \, S_0\, 0^s \, \# \, 0^t$ and $s,t$ are such that $M$ halts in less than $2^t$ steps using at most $s$ space.

  • $\begingroup$ very clever, thx! do not see any issues. the TM may also run out of left space, but thats a quibble & has no effect on the conclusion. also with minor modifications a language L with a single infinite expression "0+" is apparently sufficient. actually was hunting for something decidable but dont see a way to rescue it. with this, am presuming Boson misunderstood the question (it is stated briefly and not totally non-misinterpretable) or is mistaken. $\endgroup$
    – vzn
    Oct 24, 2015 at 16:29

This is an extended comment rather than an answer, but it may be helpful to find a decidable subcase.

Assume that the transduction $F$ is definable in some logic $\mathcal{L}$, i.e. there exists some formula $\alpha_F(x,y)$ of $\mathcal{L}$, with free SO variables encoding words $x$ and $y$, which is true only when $y = F(x)$. Given a word $x$, the property "$(F^n(x))$ is descending" is definable in SO with transitive closure (see 1 for a definition): $(\forall y . TC(\alpha_F)(x,y))(\forall z . \exists z' . \alpha_F(y,z') \wedge TC(\alpha_F)(z',z)) (|z| \leq |y| \wedge z \neq y)$

The transitive closure operator works as expected. If $\phi$ is a formula with two free variables, it describes a binary relation $R$ over the domain of the variables. $TC(\phi)$ then describes the transitive closure $R^*$ of this relation. Intuitively, the transitive closure allows (in a controlled way) an arbitrary number of quantifications: when $x R^* y$, then $x R^i y$ for some $i$, but expressing $R^i$ would require $i$ existential quantifiers.

Thus, the language $L_d = \{ x \in L ~|~ (F^n(x)) \text{ is descending} \}$ is definable in $\mathcal{L}$ + SO + TC. Thus, if in the latter logic $\mathcal{L}$ + SO + TC, the universality is decidable, then your problem is decidable as well.

Unfortunately, little is known about the appropriate logic needed to define the above $\alpha_F$ in the general case.

  • $\begingroup$ looks roughly applicable and am indeed looking for "near" decidable variants, need to dive in further. it would be helpful to expand all the specialized abbrevs. the paper seems to be a version of this one online. it would help to define or cite where "transitive closure operators" are defined, & further outline or prove "descending" property adheres. $\endgroup$
    – vzn
    Oct 26, 2015 at 20:47
  • 1
    $\begingroup$ @vzn I edited my answer to try to address your comments. I think the main relevant reference would be the monograph on descriptive complexity by Neil Immermann (springer.com/us/book/9780387986005). $\endgroup$
    – Boson
    Oct 27, 2015 at 2:03
  • 1
    $\begingroup$ You have two catches; a minor one, and a major one. The minor one is that you have to expand your logic with $|x| \leq |y|$ (the Härtig quantifier would do). The major one is that even though $L_d$ is indeed definable, emptiness (or universality) of it may not be decidable. This is the whole "catch" of finite model theory: membership is somewhat trivially decidable, but emptiness may not be (even, say, FO[+] has undecidable emptiness over words). Some word logics on infinite models (such as WS1S) still have decidable emptiness, but this is more an exception. $\endgroup$ Oct 28, 2015 at 9:39
  • $\begingroup$ thx for revisions but still having trouble following. is this all saying something like for decidability, the language $L_d$ must be expressible in some logic $\mathcal{L}$, where "emptiness is decidable"? so to solve it one would have to search for logics $\mathcal{L}$ where emptiness is decidable and express $L_d$ in it? does anyone have a list of such logics? is the latter part of the answer sketching out a means to decide emptiness for an MSO-definable statement? $\endgroup$
    – vzn
    Oct 28, 2015 at 15:11
  • 1
    $\begingroup$ As long as the predicates are decidable, any logic on words is decidable. That is, given a word, I can check whether it satisfies the formula. This is because the word structure is finite (in descriptive complexity, it is $\langle \{1, \ldots, |w|\}, Q_0, Q_1\rangle$ with $Q_b$ the set of positions where there is a $b$). Deciding if the formula is satisfiable, i.e., if the language it describes is empty, is very often undecidable (again, FO[+] is such a logic). I'm not sure I understand what is sketched at the end of this answer, though. $\endgroup$ Oct 28, 2015 at 15:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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