<p>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^*$:</p>

<p>$$\# x \, a \, H\, S \, b \, y \, \# \, w $$</p>

<p>where $w \in \{0,1\}^+$ and it outputs </p>

<p>$$\# x \, H \, S' \, a'\, b \, y \, \# \, w' $$ </p>

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

<p>$$\# x \, a' \, b \, H \, S' \, y \, \# \, w' $$ </p>

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

<p>$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.<br></p>

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

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

<p>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.</p>

<p>Note that:</p>

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

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

<p>$L = \{ \# \, H \, S_0\, \, 0^+ \# \, 0^+ \}$ </p>

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

<p>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.</p>

CC BY-SA 3.0
2015-10-24T16:29:47.707Z
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.
vzn
CC BY-SA 3.0
2015-10-23T23:04:10.430Z
2015-10-23T23:04:10.430Z
Marzio De Biasi
<p>This is an extended comment rather than an answer, but it may be helpful to find a decidable subcase.</p>

<p>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 <a href="http://www.springer.com/us/book/9780387986005" rel="nofollow">1</a> 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)$</p>

<p>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.</p>

<p>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.</p>

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

CC BY-SA 3.0
2015-10-26T20:47:45.327Z
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](http://arxiv.org/abs/cs/9906007) one online. it would help to define or cite where "transitive closure operators" are defined, & further outline or prove _"descending"_ property adheres.
vzn
CC BY-SA 3.0
2015-10-27T02:03:31.567Z
@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 (http://www.springer.com/us/book/9780387986005).
Boson
CC BY-SA 3.0
2015-10-28T09:39:11.733Z
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.
Michaël Cadilhac
CC BY-SA 3.0
2015-10-28T15:11:42.857Z
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?
vzn
CC BY-SA 3.0
2015-10-28T15:39:47.863Z
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.
Michaël Cadilhac
CC BY-SA 3.0
2015-10-26T08:53:23.970Z
2015-11-01T17:37:06.527Z
2015-11-01T17:37:06.527Z
Boson
<p>this is a followup/ sequel to this recent <a href="https://cstheory.stackexchange.com/questions/32835/is-it-decidable-whether-the-output-length-of-a-transducer-is-bounded-by-the-inpu">question</a> which was answered, this one presumably significantly harder. consider a deterministic <a href="https://en.wikipedia.org/wiki/Finite_state_transducer" rel="nofollow noreferrer">FSM transducer</a> $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). </p>

<p>now consider/ define a property of such sequences <em>"descending"</em>. a FSM sequence $x_i$ is <em>"descending"</em> 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.)</p>

<blockquote>
  <p>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 <em>descending?</em></p>
</blockquote>

<p>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.</p>

<p>motivation/ background: a long story, but inspired/ related to investigation of a highly studied open number theory <a href="https://en.wikipedia.org/wiki/Collatz_conjecture" rel="nofollow noreferrer">problem</a>. the basic idea is to look for/ formulate a generalized <a href="https://en.wikipedia.org/wiki/Loop_invariant" rel="nofollow noreferrer">loop</a> <a href="https://en.wikipedia.org/wiki/Invariant_(computer_science)" rel="nofollow noreferrer">invariant</a> function applicable to <a href="https://en.wikipedia.org/wiki/Automated_theorem_proving" rel="nofollow noreferrer">automated theorem proving</a>.</p>

CC BY-SA 3.0
2015-10-23T17:48:15.237Z
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.
Boson
CC BY-SA 3.0
2015-10-23T20:23:33.033Z
sounds promising... "SMO," do you mean [2nd order logic](https://en.wikipedia.org/wiki/Second-order_logic) ("MSOL")?
vzn
CC BY-SA 3.0
2015-10-23T21:52:36.560Z
$n$ is not given as a parameter. the sequences may have arbitrary/ varying lengths. (maybe there is some other way to bound it...?)
vzn
CC BY-SA 3.0
2015-10-23T23:24:43.093Z
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$?
Marzio De Biasi
CC BY-SA 3.0
2015-10-23T23:30:52.007Z
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).
vzn
CC BY-SA 3.0
2015-10-23T23:33:51.410Z
Ok, in that case the answer is (should be) ok. BTW if you require that every intermediate $F^i(x) \in L, 0 \leq i < n$ then the problem isn't too much different from the previous one (it's enough to check if exists an $x \in L$ for which $|F(x)| > |x|$ and $F(x) \notin L$). About the last part of your comment: "*... TM "runs" that do not move outside their initial input tapes*", yes but $L$ can be infinite, so you can "wait" a big input with enough space and time to make $M$ halt ... but such an input exists only if $M$ halts.
Marzio De Biasi
CC BY-SA 3.0
2015-10-24T00:21:40.240Z
@vzn Indeed, "SMO" is in fact Monadic Second Order Logic (MSO). Just a typo.
Boson
CC BY-SA 3.0
2015-10-24T16:51:06.800Z
@Marzio (thinking out loud some) label the sequence lengths as "$n_j$"; would a constraint that there exists a constructible function $f$ such that $n_j = O(f(|x|))$ change the conclusion (of undecidability)?
vzn
<reference-request><automata-theory><regular-language><dfa><decidability>
FSM transducer sequential composition decidability
vzn
# FSM transducer sequential composition decidability

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

this is a followup/ sequel to this recent [question](https://cstheory.stackexchange.com/questions/32835/is-it-decidable-whether-the-output-length-of-a-transducer-is-bounded-by-the-inpu) which was answered, this one presumably significantly harder. consider a deterministic [FSM transducer](https://en.wikipedia.org/wiki/Finite_state_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](https://en.wikipedia.org/wiki/Collatz_conjecture). the basic idea is to look for/ formulate a generalized [loop](https://en.wikipedia.org/wiki/Loop_invariant) [invariant](https://en.wikipedia.org/wiki/Invariant_(computer_science)) function applicable to [automated theorem proving](https://en.wikipedia.org/wiki/Automated_theorem_proving).

**Tags:** reference-request, automata-theory, regular-language, dfa, decidability

> **Comments:**
> **username_1**: 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.  
> **username_0**: sounds promising... "SMO," do you mean [2nd order logic](https://en.wikipedia.org/wiki/Second-order_logic) ("MSOL")?  
> **username_0**: $n$ is not given as a parameter. the sequences may have arbitrary/ varying lengths. (maybe there is some other way to bound it...?)  
> **username_2**: 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$?  
> **username_0**: 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).  
> **username_2**: Ok, in that case the answer is (should be) ok. BTW if you require that every intermediate $F^i(x) \in L, 0 \leq i < n$ then the problem isn't too much different from the previous one (it's enough to check if exists an $x \in L$ for which $|F(x)| > |x|$ and $F(x) \notin L$). About the last part of your comment: "*... TM "runs" that do not move outside their initial input tapes*", yes but $L$ can be infinite, so you can "wait" a big input with enough space and time to make $M$ halt ... but such an input exists only if $M$ halts.  
> **username_1**: @username_0 Indeed, "SMO" is in fact Monadic Second Order Logic (MSO). Just a typo.  
> **username_0**: @Marzio (thinking out loud some) label the sequence lengths as "$n_j$"; would a constraint that there exists a constructible function $f$ such that $n_j = O(f(|x|))$ change the conclusion (of undecidability)?  

---

## 2 answers

### Answer by username_2 on 2015-10-23. Score: 4 | Accepted answer

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.

> **Comments:**
> **username_0**: 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 username_1 misunderstood the question (it is stated briefly and not totally non-misinterpretable) or is mistaken.  

---

### Answer by username_1 on 2015-10-26. Score: 0

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](http://www.springer.com/us/book/9780387986005) 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.

> **Comments:**
> **username_0**: 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](http://arxiv.org/abs/cs/9906007) one online. it would help to define or cite where "transitive closure operators" are defined, & further outline or prove _"descending"_ property adheres.  
> **username_1**: @username_0 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 (http://www.springer.com/us/book/9780387986005).  
> **username_3**: 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.  
> **username_0**: 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?  
> **username_3**: 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.  

---

