The monadic theory of morphic infinite words and generalizations.
We present new examples of infinite words which have a decidable monadic theory. Formally, we consider structures {N, >, P} which expand the ordering {N, >} of the natural numbers by a unary predicate P; the corresponding infinite word is the characteristic 0-1-sequence xp of P. We show that for a morphic predicate P the associated monadic second-order theory MTh{N, >, P) is decidable, thus extending results of Elgot and Rabin (1966) and Maes (1999). The solution is obtained in the framework of semigroup theory, which is then connected to the known automata theoretic approach of Elgot and Rabin. Finally, a large class of predicates P is exhibited such that the monadic theory MTh(N, >, P) is decidable, which unifies and extends the previously known examples.
Introduction
In this paper we study the following decision problem about a xed !-word x:
Given a Buchi automaton A, does A accept x?
If the problem (Acc x ) is decidable, this means intuitively that one can use x as
external oracle information in nonterminating nite-state systems and still keep
decidability results on their behaviour. We solve this problem for a large class of
!-words, the so-called morphic words and some generalizations, complementing
and extending results of Elgot and Rabin [11] and Maes [15].
The problem (Acc x ) is motivated by a logical decision problem regarding
monadic theories, starting from the fundamental work of Buchi [8] on the equivalence
between the monadic second-order theory MThhN;<i of the linear order
hN; <i and !-automata (more precisely: Buchi automata). Buchi used this reduction
of formulas to automata to show that MThhN;<i is decidable. The
decidability proof is based on the fact that a sentence  of the monadic second-order
language of hN; <i can be converted into an input-free Buchi automaton
A such that  holds in hN; <i i A admits some successful run; the latter is
easily checked.
It was soon observed that Buchi's Theorem is applicable also in a more
general situation, regarding expansions of hN; <; P i of the structure hN; <i by
a xed predicate P  N. Here one starts with a formula (X) with one free set
variable and considers an equivalent Buchi automaton A over the input alphabet
is true in hN; <i with P as interpretation of X i
A accepts the characteristic word xP over B associated with P (the i-th letter
of xP is 1 In other words: The theory MThhN; <; P i is decidable if
one can determine, for any given Buchi automaton A, whether A accepts xP .
Elgot and Rabin [11] followed this approach via the decision problem (Acc xP )
and found several interesting predicates P such that MThhN; <; P i is decidable,
among them the set of factorial numbers n!, the set of k-th powers n k for any
xed k, and the set of k-powers k n for any xed k.
Elgot and Rabin (and later also Siefkes [18]) used an automata theoretic anal-
ysis, which we call contraction method, for the solution of the decision problem
(Acc xP ). The idea is to reduce the decision problem to the case of ultimately
periodic !-words (which is easily solvable). Given P as one of the predicates
mentioned above, Elgot and Rabin showed that for any Buchi automaton A,
the 0-sections in xP can be contracted in such a way that an ultimately periodic
!-word  is obtained which is accepted by A i xP is accepted by A. For the
ultimately periodic word , one can easily decide whether it is accepted by A.
More recently, A. Maes [15] studied \morphic predicates", which are obtained
by iterative application of a morphism on words (see Section 2 for deni-
tions). The morphic predicates include examples (for instance, the predicate of
the Fibonacci numbers) which do not seem to be accessible by the Elgot-Rabin
method. Maes proved that for any morphic predicate P , the rst-order theory
decidable, and he also introduced appropriate (although spe-
cial) versions of morphic predicates of higher arity. It remained open whether
for each morphic predicate P , the monadic theory MThhN; <; P i is decidable.
In the present paper we answer this question positively, based on a new (and
quite simple) semigroup approach to the decision problem (Acc xP In Section 2
we show that for morphic predicates P the problem (Acc xP ) is decidable. As
a consequence, we nd new examples of predicates P with decidable monadic
theory MThhN; <; P i. Prominent ones are the Fibonacci predicate (consisting
of all Fibonacci numbers) and the Thue-Morse word predicate (consisting of
those numbers whose binary expansion has an even number of 1's).
In the second part of the paper, we embed this approach into the framework
of the contraction method. This method is shown to be applicable to predicates
which we call \residually ultimately periodic". We prove two results: Each mor-
phic predicate is residually ultimately periodic, and a certain class of residually
ultimately periodic predicates shares strong closure properties, among them
under sum, product, and exponentiation. This allows to obtain many example
predicates P for which the monadic theory MThhN; <; P i is decidable.
It should be noted that for certain concrete applications (such as for the
Fibonacci predicate) the semigroup approach is much more convenient than an
explicit application of the contraction method, and only an analysis in retrospect
reveals the latter possibility. Also morphic predicates like the Thue-Morse word
predicate are not approachable directly by the contraction method, because
there are no long sections of 0's or 1's.
Let us nally comment on example predicates P where the corresponding
Buchi acceptance problem (Acc xP ) and hence MThhN; <; P i is undecidable, and
give some comments on unsettled cases and on related work.
First we recall a simple recursive predicate P such that MThhN; <; P i is
undecidable. For this, consider a non-recursive, recursively enumerable set Q
of positive numbers, say with recursive enumeration m
recursive but
even the rst-order theory FThhN; <; P i is undecidable: We have
some element x of P , the element x is the next element after x in P , a
condition which is expressible by a rst-order sentence  k over hN; <; P i. Buchi
and Landweber [9] and Thomas [19] determined the recursion theoretic complexity
of theories MThhN; <; P i for recursive P ; it turns out, for example, that
for recursive P the theory MThhN; <; P i is truth-table-reducible to a complete
-set, and that this bound cannot be improved. The situation changes when
recursive predicates over countable ordinals are considered (see [22]). In [20] it
was shown that for each predicate P , the full monadic theory MThhN; <; P i is
decidable i the weak monadic theory WMThhN; <; P i is (where all set quantiers
are assumed to range only over nite sets). However, there are examples P
such that the rst-order theory FThhN; <; P i is decidable but WMThhN; <; P i
is undecidable ([19]).
In the present paper we restrict ourselves to expansions of hN; <i by unary
predicates. For expansions hN; <; fi by unary functions f , the undecidability of
MThhN; <; fi arises already in very simple cases, like for the doubling function
2n. For a survey on these theories see [16].
On the other hand, it seems hard to provide mathematically natural recursive
predicates P for which MThhN; <; P i is undecidable. A prominent example of
a natural predicate P where the decidability of MThhN; <; P i is unsettled is
the prime number predicate. As remarked already by Buchi and Landweber in
[9], a decidability proof should be dicult because it would in principle answer
unsolved number theoretic problems like the twin prime hypothesis (which states
that innitely many pairs primes exist). The only known result is
that MThhN; <; P i is decidable under the linear case of Schinzel's hypothesis
[4].
Part of the results of the present paper has been presented at the conference
MFCS'2000 [10].
automata over morphic predicates
A morphism  from A  to itself is an application such that the image of any word
an is the concatenation (a (an ) of the images of its letters. A
morphism is then completely dened by the images of the letters. In the sequel,
we describe morphisms by just specifying the respective images of the letters as
in the following example
Let A be a nite alphabet and let  be a morphism from A  to itself. For
any integer n, we denote  n the composition of n copies of  . Let
the sequence of nite words dened by (a) for any integer n. If the rst
letter of (a) is a, then each word xn is a prex of xn+1 . If furthermore the
sequence of length jx n j is not bounded, the sequence converges to an
innite word x which is denoted by  ! (a). The word x is a xed point of the
morphism since it satises
Example 1 Let consider the morphism  given by
The words are respectively equal to
It can be easily proved by induction on n that  n+1
Therefore, the xed point  ! (a) is equal to the innite word abc 2 bc 4 bc 6 bc
An innite word x over B is said to be morphic if there is a morphism
from A  to itself and a morphism  from A  to B  such that In
the sequel, the alphabet B is often the alphabet and the morphism
is letter to letter.
The characteristic word of a predicate P over the set N of non-negative
integers is the innite word over the alphabet B dened by b
predicate is said to be morphic i its
characteristic word is morphic.
These denitions are illustrated by the following two examples.
Example 2 Consider the morphism  introduced in the preceding example and
the morphism  given by
The morphic word actually the characteristic word
of the predicate Ng. This can be easily proved using the equality
1. The square predicate is therefore morphic.
It will proved in the sequel that the class of morphic predicates contains all
predicates of the form fn k jn 2 Ng and fk n jn 2 Ng for any xed integer k.
Example 3 Consider the morphism  from B
to B
dened by
The xed point  is the characteristic word of the
predicate P with the binary expansion of n contains an even number
of 1. The xed point  ! (1) is the well-known Thue-Morse word. We refer the
reader to [5] for an interesting survey on that sequence and related works of A.
Thue.
Recall that a Buchi automaton is an automaton
is a nite set of states, E  Q  A  Q is the set of transitions and I and F
are the sets of initial and nal states. A path is successful if it starts in an
initial state and goes innitely often through a nal state. An innite word is
accepted if it is the label of a successful path. We refer the reader to [21] for a
complete introduction. Now we can state the main result and in the corollary,
its formulation in the context of monadic theories:
Theorem 4 Let (a)) be a xed morphic word where  : A  ! A  and
are morphisms. For any Buchi automaton A, it can be decided
whether x is accepted by A.
As explained in the introduction, the theorem can be transferred to a logical
decidability result, invoking Buchi's Theorem [8] on the equivalence between
monadic formulas over hN; <i and Buchi automata:
Corollary 5 For any unary morphic predicate P , the monadic second-order
theory of hN; <; P i is decidable.
Proof (of Theorem automaton. Dene the
equivalence relation  over A  by
F
F
means that there is a path from p to q labeled by u and p u
F
means that there is a path from p to q labeled by u which hits some nal state.
This equivalence relation captures that two nite words have the same behavior
in the automaton with respect to the Buchi acceptance condition. It was already
introduced by Buchi in [8].
Denote by  the projection from A  to A  = which maps each word to its
equivalence class.
The equivalence relation  is a congruence of nite index. Indeed, for any
words u, v, u 0 and v 0 , the following implication holds: If
This property allows us to dene a product on the classes which endows
the set A  = with a structure of nite semigroup. The projection  is then a
morphism from A  onto A  =.
Furthermore, for any xed states p and q, there are at most three possibilities
for any word u: Either there is a path from p to q through a nal state, or there
is a path from p to q but not through a nal state or there is no path from p
to q labeled by u. This proves that the number of classes is bounded by 3 n 2
where n is the number of states of the automaton.
The following observation gives the main property of the congruence .
Suppose that the two innite words x and x 0 can be factorized
and x
k for any k  0. Then x is accepted by A
accepted by A. Indeed, suppose that x is the label of a successful path.
This path can be factorized
where q 0 is initial and where the nite path q k
a nal state for
innitely many k. Since u k  u 0
k for any k  0, there is another path
where the nite path q k
a nal state whenever q k
does.
This proves that x 0 is also the label of a successful path and that it is accepted
by A. In particular, if an innite word x can be factorized
that u 1  u 2     , then x is accepted by A i u
1 is also accepted by A.
Since a is the rst letter (a), the word (a) is equal to au for some nonempty
nite word u. It may be easily veried by induction on n that for any integer n,
one has
The word can be factorized
We claim that there are two positive integers n and p such that for any k  n,
the relation u k  u k+p holds. This relation is equivalent to (u k
morphism from A  into a semigroup is completely determined by the images of
the letters. Therefore, there are nitely many morphism from A  into the nite
semigroup A  =. This implies that there are two positive integers n and p such
that      This implies that
k greater than n, and thus u k  u k+p . Note that these two integers n and p
can be eectively computed. It suces to check that ( n (b))  ( n+p (b)) for
any letter b of the alphabet A.
Dene the sequence (v k ) k0 of nite words by v
1. The word x can be factorized
and the relations v 1  v 2  v 3    hold. This proves that the word x is accepted
by the automaton A i the word v
1 is accepted by A. This can be obviously
be decided.
3 A large class of morphic predicates
The purpose of this section is to give a uniform representation of a large class of
morphic predicates: We will show that each predicate
k  0 and a polynomial Q(n) with non-negative integer values is morphic. This
supplies a large class of predicates P where the decision problem (Acc xP ) and
hence the monadic theory of hN; <; P i is decidable. In particular, the classical
examples fk xed k in N of [11] are covered
by this.
As a preparation, we shall develop a sucient condition on sequences
to dene a morphic predicate. It will involve the notion of a N-rational sequence.
These considerations will also show that the Fibonacci predicate fFn
(where
We refer the reader to [17] for a complete introduction and to [3] for a survey
although we recall here the denitions.
Definition 6 A sequence (un ) n0 of integers is N-rational if there is a graph G
allowing multiple edges, sets I and F of vertices such that un is the number of
paths of length n from a vertex of I to a vertex of F . The graph G is said to
recognize the sequence (un ) n0 .
An equivalent denition is obtained by considering non-negative matrices. A
sequence (un ) n0 is N-rational i there is a matrix M in N kk and two vectors
L in B 1k and C in B k1 such that un = LM n C. It suces indeed to consider
the adjacency matrix M of the graph and the two characteristic vectors of the
sets I and F of vertices. It also possible to assume that the two vectors L and
respectively belong N 1k and N k1 instead of B 1k and B k1 since the class
of N-rational sequences is obviously closed under addition. A triplet (L; M;C)
such that un = LM n C is called a matrix representation of the sequence
and the integer k is called the dimension of the representation. The following
example illustrates these notions.
Example 7 The number of successful paths of length n in the graph pictured in

Figure

1 is the Fibonacci number Fn where F
This shows that the sequence (Fn ) n0 is N-rational. This sequence has the
following matrix representation of dimension 2
which can be deduced from the graph of Figure 1.

Figure

1: A graph for the Fibonacci sequence
We now state the main result of this section.
Theorem 8 Let un be a sequence of non-negative integers and let
un be the sequence of dierences. If there is some integer l such that dn  1 for
any n  l and such that the sequence (d n ) nl is N-rational, then the predicate
As a rst illustration of the Theorem, reconsider the predicate of the Fibonacci
Each dierence is equal to Fn 1 , it
obviously satises dn  1 for n  1, and the sequence (Fn ) n0 is N-rational as
shown in Example 7. So the Fibonacci predicate is morphic.
With the following corollary we obtain a large collection of morphic pred-
icates, including the predicates of the form fn k
considered in [11].
Corollary 9 Let Q be a polynomial such that Q(n) is integer for any integer n
and let k be a positive integer. The predicate
0g is morphic.
The proof of the corollary is entirely based on the following lemma.
a polynomial with a positive leading coecient such that
Q(n) is integer for any integer n. Let k be a positive integer and let un be
dened by un = Q(n)k n . There is a non-negative integer l such that the sequence
Note that such a polynomial may have non-integer coecients as the polynomial
Proof Let d be the degree of Q. We claim that there are then a non-negative
integer l and positive integers a a d such that for any n,
d
a i
Let Q l (n) be the polynomial Q(n + l). Since Q l (n) is integer for any integer n,
the polynomial Q l (n) is equal to a linear combination of the binomials with
integer coecients (see [12, p. 189]). There is a unique sequence a
of d integers such that for any integer n
d
a l;i
Since the binomials satisfy the well-known relation n+1
, it
follows that the coecients a l;i satisfy the following relation. For any integer l,
one has a l+1;d = a l;d and a a l;i+1 for i < d. Since the leading
coecient of Q l is positive, the coecient a l;d is also positive for any l. Using
the relation on the coecients on the a l;i , it can be proved by induction on the
dierence d i that for any i  d, there is an integer l i such that a l;i is positive
for any l  l i . The integer l dened the required
property.
We now dene the matrix M and the vectors L and C as follows. The
vector L is the vector of dimension d
d. The matrix M is the square matrix of dimension d dened by
d. The
vector C is the the vector of dimension d
It is pure routine to prove by induction on n that LM n is the vector Ln given
by L
for 0  i  d. Therefore un+l is equal to LM n C for any
and the sequence (un+l ) n0 is N-rational.
The proof of Theorem 8 needs some preliminary result that we now state.
This lemma makes easier the proof that certain predicates are morphic. It
essentially states that the property of being morphic is preserved by shifting
and by changing a nite number of values. In particular, if two predicates P
and P 0 coincide for almost every n, then P is morphic i P 0 is morphic.
Lemma 11 Let P be a predicate and let R be a nite set of integers. Let k be
a non-negative integer and let P 0 be the predicate R [
is morphic i P 0 is morphic.
Proof Let P be a morphic predicate. Assume that the characteristic word xP
of P is equal to ( ! (a)) where  and  are respectively morphisms from A
into itself and from A  into B  . Let x be the xed point  ! (a) and let u be the
nite word such that (a) = au. The innite word x can be then factorized
We rst prove that both predicates P
are also morphic. Let A 0 be the alphabet A [ where a 0 and a 1 are two
new symbols. Dene the morphism  0 from A 0  into itself by  0 (a
any b in A. It is clear that the xed point
Dene the morphism  0 from A 0  into B  by  0 (a 1
any b in A. If  0 (a 0 ) is set to 0, then the word  is the characteristic
word of P 0 and if  0 (a 0 ) is set to 1, then the word  is the characteristic
word of P 00
We now prove that there is a positive integer k such that the predicate
be the alphabet A [
where a 0 is a new symbol. Dene the morphism  0 from A 0  into itself by
any b in A. It is clear that the xed point
Let k be the length of u. Dene the morphism  0 from A 0  into B  by (a
any b in A. The word  0 is the characteristic
word of P 0 .
The claimed result follows then easily from the two previous results.
The following two results will be used in the proof of Theorem 8. The rst
result is due to Schutzenberger. We refer the reader to [17, Thm II.8.6] and [6,
Thm V.2.1] for complete proofs.
Theorem 12 (Sch utzenberger 1970) Let (un ) n0 be a N-rational sequence
such that un  1 for any n. The sequence (un 1) n0 is also N-rational.
For the next result, we need the notion of a D0L-sequence. A N-rational
sequence (un ) n0 of integers is said to be a D0L-sequence if it can be recognized
by a graph all of whose states are nal. Equivalently, a N-rational sequence
(un ) n0 is a D0L-sequence if it has a matrix representation (L; M;C) such that
all components of L are either 0 or 1 and such that all components of C are
equal to 1. We have then the following result [17, Lem III.7.4].
Every N-rational sequence (u n ) n0 can be decomposed into D0L-
sequences. This means that there are two integers K and p such that each
sequence (u k+np ) n0 for k  K is a D0L-sequence.
We nally come to the proof of Theorem 8.
Proof We suppose that un satises dn  1 for n  l and that the
sequence (d n )n  l is N-rational. By Lemma 11, it may be assumed without
loss of generality that l = 0. By Theorem 12, the sequence (v n ) n0 dened by
that sequence can be decomposed into
D0L-sequences. There are two two integers K and p such that each sequence
(v k+np ) n0 for k  K is a D0L-sequence. By Lemma 11, it may be assumed
again without loss of generality that and that u
the sequence v Each sequence v k has a matrix
representation such that each component of L k are either 0 or 1
and such that all components of C k are equal to 1. Let d k be the dimension of
that representation. Dene the alphabet A by
Dene the morphism from A  into itself by
a 7! ac L0;1
c k;i 7! c Mk;i;1
It can be easily proved by induction on n that
Y
where each w k;i is a word on the alphabet fc k;j j 1  j  d k g of length v k;i .
Actually the number occurrences of the letter c k;j in the word w k;i is the j-th
component of the vector L k M i
k . Dene then the morphism  from A  into B
by
As a complement to Corollary 9 (that predicates fQ(n)k n j n 2 Ng are
morphic), we formulate a necessary condition for a predicate P to be morphic.
It turns out that the factorial predicate fn! j n 2 Ng does not fall under this
condition, which shows that it is not morphic. In the subsequent section, we
shall develop a framework where such predicates can be handled together with
the morphic ones, thus unifying the contraction method of Elgot and Rabin
with the results above.
Proposition 14 Let (un ) n0 be a strictly increasing sequence of integers. If
the predicate fun
integer k.
Proof Suppose that the characteristic word of the predicate fun j n 2 Ng is
equal to ( ! (a)) where  and  are respectively morphisms from A  into itself
and from A  into B  . Let x be the xed point  ! (a) and let u be the nite word
such that (a) = au. The innite word x can be then factorized
Let k be the integer dened by (b)j. It can be easily shown by
induction on n that j n (b)j  k n for any letter b. Let B the set of letters b
such that (b) contains at least one 1, that is
g. We claim
that if for a xed letter b, there is an integer n such that  n (b) contains a letter
of B, the smallest integer satisfying this property is smaller than the cardinality
of A. This follows from the fact that a letter c appears in  n (b) i there is a
sequence of letters such that b appears in (b i )
for 0  i < n. For any integer n, the word  n (a)
contains therefore a letter of B and the result follows easily.
Residually ultimately periodic predicates
In this section, we develop a framework which merges the contraction method
of Elgot and Rabin with the semigroup approach used for morphic predicates.
The common generalization of the two approaches is captured by the notion of
residually ultimately periodic innite words. We introduce these words and we
show that morphic words belong to this class. The application to the contraction
method is developed in the subsequent section.
Definition 15 A sequence (un ) n0 of words over an alphabet A is said to
be residually ultimately periodic if for any morphism  from A  into a nite
semigroup S, the sequence (un ) is ultimately periodic.
This property is said to be eective i for any morphism  from A  into a
nite semigroup, two integers n and p such that for any k  n,
can be eectively computed. An innite word x is called residually ultimately
periodic if it can be factorized where the sequence (u n ) n0 is
eectively residually ultimately periodic. The following proposition shows how
this property can be used for deciding the problem (Acc x
Proposition 16 If the innite word x is residually ultimately periodic, the
problem (Acc x ) is decidable.
Proof Let A = (Q; E; I ; F ) be a Buchi automaton. Dene the equivalence
relation  over A  by
The relation  is a congruence of nite index. The application which maps any
nite word to its class is therefore a morphism from A  into the nite semigroup
A  =.
This congruence has the following main property. Suppose that the two
innite words x and x 0 can be factorized
such that u k  u 0
k for any k  0. Then x is accepted by A i x 0 is accepted
by A.
Since the sequence (u n ) n0 is residually ultimately periodic, there are two
integers n and p such that for any k greater than n, Therefore, x
is accepted by A i the word v
1 is accepted by A where v
We illustrate this notion by the following example.
Example 17 The sequence of words (a n! ) n0 is residually ultimately periodic.
This sequence is actually residually ultimately constant. It is indeed well-known
that for any element s of a nite semigroup S and any integer n greater than
the cardinality of S, s n! is equal to a xed element usually denoted s ! in the
literature [2, p. 72].
The sequences of words which are residually ultimately constant have been
considerably studied. They are called implicit operations in the literature [2]. A
slight variant of the previous example shows that the sequence (u n ) n0 dened
by un residually ultimately constant. Since (n
equal to nn! 1, the word u 0 u 1 is the characteristic word of the factorial
predicate Ng. The monadic theory of hN; <; P i where P is the
factorial predicate is therefore decidable by the previous proposition.
In the following propositions we connect the residually ultimately periodic
sequences to the innite words obtained by iterating morphisms.
Proposition  be a morphism from A  into itself and let u be a word
over A. The sequence un =  n (u) is residually ultimately periodic, and this
property is eective.
Proof Let  be a morphism from A  into a nite semigroup S. Since S is
nite, there are nitely many morphisms from A  into S. Therefore, there are
two integers n and p such that    This implies that for any k
greater that n, one has    . Note that the
two integers n and p can be eectively computed. It suces to nd n and p
such that ( n any letter a in A.
It follows from the proposition that a morphic word has a factorization whose
factors form a residually ultimately periodic sequence. Let x be a morphic word
are morphisms and let u be the nite word such that
au. The word x can be factorized
and un = ( n (u)) for n  1. By the proposition, the sequence ( n (u)) n0 is
residually ultimately periodic. The sequence (u n ) n0 is therefore also residually
ultimately periodic.
5 The predicate class K
The decidability of the decision problem (Acc x ) for an innite word x involves a
\good" factorization of the word x. In the case morphic words, this factorization
is naturally provided by the generation of x via a morphism. Another approach
is to consider the canonical factorization of the word x induced by the blocks
which form the word x (representing the distances between the successive
elements of the predicate). The contraction method as developed by Elgot and
Rabin [11] and Siefkes [18] reduces the sequence of these nite words from 0  1
to an ultimately periodic sequence. In this section we embed this method into
the framework developed above.
If strictly increasing sequence of integers, the characteristic
word xP of the predicate can be canonically factorized
un is the word 0 kn+1 kn 1 1 over the alphabet B . If this
sequence of words is residually ultimately periodic and if furthermore
this property is eective, it is decidable whether the word xP is accepted by a
Buchi automaton and the monadic theory of hN; <; P i is therefore decidable.
We will prove that the class of sequences such that this property holds
contains interesting sequences like (n k ) and that it is
also closed under several natural operations like sum, product and exponentiation

The following lemma essentially states that it suces to consider the sequence
un = a kn+1 kn over a one-letter alphabet.
Lemma 19 Let (un ) n0 be a sequence of words over A and let a be a letter.
The sequence (un ) n0 is residually ultimately periodic i the sequence (u n a) n0
is residually ultimately periodic. Moreover this property is eective for
i it is eective for (un a) n0 .
Proof It is clear that if the sequence (u n ) n0 is residually ultimately periodic,
then the sequence (un a) n0 is also residually ultimately periodic. Indeed, for
any morphism  from A  into nite semigroup, the relation
implies that if the sequence (un ) n0 is ultimately periodic, then the sequence
(una) is also ultimately periodic.
Conversely let  be a morphism from A  into a nite semigroup S. Let ^
S be
the semigroup S 1 S with the product dened by (s; t)(s
be the morphism from A  into ^
S dened by It may be easily
veried by induction on the length on the word w that
Therefore, if the sequence (un a) n0 is residually ultimately periodic, the sequences
(una) and (un ) are ultimately periodic. The sequence (u n ) n0 is
then residually ultimately periodic
If A is the one-letter alphabet fag, the semigroup A  is isomorphic to the
set N of integers by identifying any word a n with the integer n. Therefore, a
sequence of integers is said to be residually ultimately periodic i the
sequence a kn is residually ultimately periodic.
K be the class of increasing sequences (k n ) n0 of integers
such that the sequence (k n+1 kn ) n0 is residually ultimately periodic.
By Lemma 19 and by Proposition 16, we conclude:
Theorem be in K and let xP be the characteristic word of the
predicate Ng. Then the decision problem (Acc xP ) is decidable
and the monadic theory MThhN; <; P i is also decidable.
We give two comments, the rst one on the relation between the class K and
residually ultimately periodicic sequences, the second one on a similar class of
predicates introduced by Siefkes [18].
As stated in Corollary 28 below, each sequence in K is residually ultimately
periodic. The converse is not true as the following example shows. Let
be an innite word over the alphabet B , that is b Consider the
sequence dened by
)!. If the word x has innitely many
occurrences of 1, the sequence (k n ) n0 is then residually ultimately periodic (cf.
Example 17). However, if the word x is not ultimately periodic, the sequence
residually ultimately periodic.
In [18], Siefkes studies predicates generated by sequences
two conditions: to be \eectively ultimately reducible" (which corresponds
to being eectively residually ultimately periodic), and to have an essentially
increasing sequence of dierences kn+1 kn , i.e., for each d  0, we have
eectively computable from d). The second
assumption ensures that the sequence (k n+1 kn ) n0 is residually ultimately
periodic in our sense. Although most natural predicates of the class K can also
be treated by Siefkes' approach, there are some exceptions. For instance, let
dened by is even and by
is odd. This sequence (k n ) n0 is in the class K but Siefkes' second assumption
does not apply.
The following theorem shows that the class K contains interesting sequences
and that it is closed under several natural operations.
Theorem 22 Any sequence (k n ) n0 such that the sequence (k n+1 kn ) n0 is
N-rational belongs to K. If the sequences belong to K, the
following sequences also belong to K:
(sum and product) kn
(exponentiation) k l n for a xed integer k and k l n
(generalized sum and product)
By Lemma 10, the class K contains any sequence of the form k n Q(n) where
k is a positive integer and Q is a polynomial such that Q(n) is integer for any
integer n. By applying the generalized product to the sequences
the sequence (n!) n0 belongs to K.
The closure by dierences shows that K contains any rational sequence
of integers such that lim n!1 (k n+1 kn rational
sequence of integers is the dierence of two N-rational sequences [17, Cor. II.8.2].
The class K is also closed by other operations. For instance, it can be proved
that if both sequences belong to K, then the sequence
dened by
belongs to K.
The class K is closed under sum, dierence product and exponentiation but
the following example shows that it not closed under quotient.
Example 23 Consider the sequence
This sequence is not
residually ultimately periodic since the sequence (k n mod 4) is not ultimately
periodic. It turns out that (k n mod p) is not ultimately periodic unless
[1]. It can be easily seen that the greatest integer l such that 2 l divides kn is
the number of 1 in the binary expansion n. Therefore, (k n mod 4) is equal to 2
if n is a power of 2 and to 0 otherwise.
For two integers t and p, dene the equivalence relation  t;p on N as follows.
For any integers k and k 0 , one has
The integers t and p are respectively called the threshold and the period of
the relation  t;p . Note that the relation k  t;p k 0 always implies that
mod p. The equivalence relation  t;p is of nite index and it is compatible with
sums and products. Indeed if k  t;p k 0 and l  t;p l 0 hold then both relations
relations  t;p for t and p capture
the property of being residually ultimately periodic for sequences of integers.
Lemma 24 A sequence (k n ) n0 of integers is residually ultimately periodic i
for any integers t and p there are two integers t 0 and p 0 such that for any n
greater than t 0 , one has kn  t;p kn+p 0 .
Proof Indeed, this condition is sucient since for any element s of a nite
semigroup, there are two integers t and p such that s . Conversely, this
condition is also necessary. The set N= t;p equipped with addition is a nite
semigroup and the canonical projection from N to N= t;p is a morphism.
The following result is almost trivial but it will often be be used.
Lemma
l be l relations associated with xed integers
residually ultimately periodic
sequences of integers. There are two integers r and q such that k j;n  t i ;p i
for any 1  i  l, any 1  j  m and any n greater than r.
Proof Since each sequence (k i;n ) n0 is residually ultimately periodic, there are
two integer r i;j and q i;j such that k j;n  t i ;p i
for any n greater than t i;j .
The two integers r and q dened by
the required property.
The following lemma states that the class of residually ultimately periodic
sequences of integers is closed under sum and product. These results follow
from a more general result which states the class of residually ultimately periodic
sequences of words are closed under substitution. More precisely, if the sequence
of morphisms from A  into B  is such that each sequence ( n (a)) n0
is residually ultimately periodic and if the sequence (u n ) n0 of words over A
is also residually ultimately periodic, then the sequence ( n (un
residually ultimately periodic. If each word un is for instance equal to the xed
word ab and if the morphism  n maps a to vn and b to wn , the word  n (u)
is equal to vn wn . The class of residually ultimately periodic sequences of words
are closed under concatenation. If un is equal to a kn and if  n (a) is equal to
a l n , then  n (un ) is equal to a kn l n . We give here a direct proof of these results
which relies on the compatibility of any relation  t;p with sums and products.
Lemma 26 Let (k n ) n0 and (l n ) n0 be two residually ultimately periodic sequences
of integers. Both sequences are also residually
ultimately periodic. If lim n!1 (k n l n then the sequence (k n l n ) n0
is also residually ultimately periodic.
The following example shows that the assumption on the limit of the sequence
kn l n is really necessary. Let be an innite word
over the alphabet B . Consider the sequences (k n ) n0 and (l n ) n0 dened by
These two sequences are obviously residually
ultimately periodic (cf. Example 17). However, the dierence kn l n is equal
to n!. If the word x is not ultimately periodic, the sequence (k n l n ) n0
is not residually ultimately periodic.
Proof By Lemma 25, there are then r and q such that kn  t;p kn+q and
l n  t;p l n+q for any n greater than r. This yields kn
and kn l n  t;p kn+q l n+q for n greater than r. The sequences
are residually ultimately periodic.
The relations kn  t;p kn+q and l n  t;p l n+q imply that
and l This yields kn l
the dierence kn l n is greater than t for all n greater
than some r 0 . Then for any n greater than r and r 0 , one has kn l n  t;p
kn+q l n+q for n greater than r 0 and the sequence (k n l n ) n0 is residually
ultimately periodic.
The following lemma states the class of residually ultimately periodic sequences
of integers is closed under generalized sum and product when l
It will be used to prove the general case.
Lemma be a residually ultimately periodic sequence of inte-
gers. The sequences (Kn ) n0 and (Ln ) n0 dened by
are also residually ultimately periodic.
Proof Let  t;p be the relation associated with two xed integers t and p. There
are then two integers r and q such that kn  t;p kn+q for any n grater than r.
Let k be the sum
. Note that
integer l.
There are then two integers r 0 and q 0 such that r 0 k  t;p (r
that , Kn  t;p Kn+qq 0
holds for any n greater than r Indeed, one has
r
t;p
r
t;p
r
t;p
r
The proof for Ln is very similar. It suces to replace each sum by a product.
For instance, the constant k is dened by
and the two integers
r 0 and q 0 are chosen such that k r 0
.
The previous lemma has the following corollary.
Corollary 28 Any sequence (k n ) n0 in K is residually ultimately periodic.
The following lemma is needed to prove that the class K is closed under
generalized sum and product.
residually ultimately periodic
sequences of integers. Both sequences (Kn ) n0 and (Ln ) n0 dened by
are then residually ultimately periodic.
Proof Let  t;p be the relation associated with two xed integers t and p. There
are then two integers r and q such that kn  t;p kn+q for any n grater than r. Let
k be the sum
. Note that
integer n greater
than r. There are then two integers r 0 and q 0 such that r 0 k  t;p (r
Lemma 25, there are also two integers r 00 and q 00 such that l n  r;q l n+q 00
and
dn  r+r 0 q;qq 0 dn+q 00 for any n greater than r 00 . We claim that Kn  t;p Kn+q 00
for any n greater than r 00 .
We rst claim that Kn+q 00  t;p
the result obviously
holds. Otherwise, one has l n  r and l n+q 00  r. Since l
has k i  t;p k i+l where l = l n+q 00 l n for any l n  i. This proves the claim.
We now prove that
i=ln  t;p Kn . If the result holds
obviously. Otherwise, one has dn  r
we may assume that dn+q 00 > dn . Since dn+q
suppose that dn+q 00
l. One has then
t;p
l n+dn+lqq 0
t;p
l n+dn r 0 q
t;p
l n+dn r 0 q
t;p
l n+dn X
The proof for Ln is similar. It suces to replace each sum by a product.
We nally come to the proof of theorem 22.
Proof We prove that any sequence (k n ) n0 such that the sequence (k n+1
kn ) n0 is N-rational belongs to K. This follows from Theorem 8 and from
Proposition but we also provide a direct proof. If the sequence (d n ) n0
is dened by is N-rational, there is a matrix representation
(L; M;C) such that the relation  t;p to
matrices by setting M  t;p M 0 i the relation M k;l  t;p M 0
k;l holds for any
(k; l)-entry of the matrices. There are then two integers r and q such that
M r  t;p M r+q and this implies M n  t;p M n+q for n greater than r. Thus, one
has dn  t;p dn+q for n greater than r.
If both sequences belong to to K, Lemma 26 applied
to the sequences (k n+1 kn ) n0 and (l n+1 l n ) n0 shows that the sequence
belongs then to K. If furthermore, the assumption on the limit is
fullled, it also shows that the sequence (k n l n ) n0 belongs then to K.
The dierence kn+1 l n+1 kn l n is equal to kn+1 (l n+1 l n )+(kn+1 kn )l n . By
Lemma 27, the sequences (k n ) n0 and (l n ) n0 are residually ultimately periodic.
By Lemma 26, the sequence of dierences is then residually ultimately periodic
and the sequence (k n l n ) n0 belongs then to K.
The dierence k l n+1 k l n is equal to k l n (k l n+1 l n 1). By lemma 27, both
sequences k l n and k l n+1 l n are residually ultimately periodic. By Lemma 26, the
sequence of dierences is then residually ultimately periodic and the sequence
belongs then to K.
Let Kn be the sum
. The dierence Kn+1 Kn is equal to the sum
. By Lemma 27, the sequence (l n ) n0 is residually ultimately periodic
and by Lemma 29, the sequence of dierences is then residually ultimately
periodic.
Let Kn be the product
. The dierence Kn+1 Kn is equal to
l n
Y
l n+1
Y
By Lemma 29, the sequence (Ln ) n0 dened by
residually
ultimately periodic. By Lemma 27 applied to the sequence (Ln ) n0 , the sequence
dened by L 0
residually ultimately periodic.
By Lemma 26, the sequence of dierences is then residually ultimately periodic
and the sequence (Kn ) n0 belongs then to K.
Let dn be the dierence kn+1 kn , let d 0 n be the dierence k l n+1
n . We
assume that the sequence (k n ) n0 is strictly increasing and we also assume that
l n  2 for n greater than some constant which can be eectively computed.
We prove that the sequence (d 0
residually ultimately periodic. Let  t;p
be the relation associated with two xed integers t and p. We rst claim that
greater than t. On has indeed the following inequalities
Since the sequence (k n ) n0 is assumed to be strictly increasing, dn is non-zero
and kn is greater than t for any n greater than t.
By Lemma 25, there are two integers s and m such that k n  t;p k n+m for
any integer k and any integer n greater than s. Note that if n  s and if
k  t;p l, then k n  t;p l n  t;p l n+m . By Lemma 25, there are two integers r
and q such that kn  t;p kn+q , dn  t;p dn+q 0
, l n  s;m l n+q for any integer n
greater than r. We claim that d 0
for any integer n greater than r.
n+q  t, it suce to prove that d 0
n+q mod p. The
relations kn  t;p kn+q and l n  s;m l n+q 0
imply k l n
n+q . The relation
kn+1  t;p kn+q+1 and l n+1  r;q l n+q+1 imply k l n+1
n+q+1 . This two
relations then imply d 0
n+q mod p.
Conclusion
We have introduced a large class of unary predicates P over N such that the
corresponding Buchi acceptance problem Acc xP (and hence the monadic theory
decidable. The class contains all morphic predicates (which
solves a problem of Maes [14, 15]). The connection to the work by Elgot and
Rabin [11] and Siefkes [18] was established by extending the class of morphic
predicates to the class of the residually ultimately periodic predicates. Finally,
strong closure properties (under sum, product, and exponentiation) were shown
for certain residually ultimately periodic predicates (where the sequence of differences
of successive elements is residually ultimately periodic). Altogether we
obtain a large collection of concrete examples P such that MThhN; <; P i is de-
cidable, containing the k-th powers and the k-powers for each k, the value sets of
polynomials over the integers, the factorial predicate, the Fibonacci predicate,
as well as the predicates derived from morphic words like the Thue-Morse word
and the Fibonacci word.
Let us mention some open problems.
Our results do not cover expansions of hN; <i by tuples predicates
rather than by single predicates. In his dissertation, Hosch [13] has solved
the problem for the special case of the predicates P
Ng. We do
not know whether MThhN; <; decidable if the P i are just known
to be residually ultimately periodic.
There should be more predicates P for which the Buchi acceptance problem
Acc xP and hence the theory MThhN; <; P i is decidable. A possible next step
is to consider Sturmian words, a natural generalization of morphic words (see
[7]).
Finally, we should recall the intriguing question already asked by Buchi and
Landweber in [9] (\Problem 1"): Is there an \interesting" recursive predicate P
such that MThhN; <; P i is undecidable? How about P being the prime number
predicate?

Acknowledgement

The authors would like to thank Jorge Almeida, Jean-Paul Allouche, Jean Berstel
and Jacques Desarmenien for very interesting suggestions and comments.



--R

Linear cellular automata
Finite Semigroups and Universal Algebra.

Decidability and undecidibility of theories of with a predicate for the primes.
Axel Thue's work on repetitions in words.
Rational Series and Their Languages.



The monadic theory of morphic in
Decidability and undecidibility of extensions of second
Concrete Mathe- matics
Decision Problems in B
Decidability of the
An automata theoretic decidability proof for the
Open questions around B

Decidable extensions of monadic second order successor arith- metic
The theory of successor with an extra predicate.
On the bounded monadic theory of well-ordered structures
Automata on in
Ehrenfeucht games
--TR
Rational series and their languages
Automata on infinite objects
Linear cellular automata, finite automata and Pascal''s triangle
Open questions around BuMYAMPERSANDuml;chi and Presburger arithmetics
An automota theoretic decidability proof for first-order theory of <inline-equation> <f> <fen lp="ang"><blkbd>N</blkbd>,MYAMPERSANDlt;,P<rp post="ang"></fen></f> </inline-equation> with morphic predicate P
Concrete Mathematics
Automata
The Monadic Theory of Morphic Infinite Words and Generalizations
Ehrenfeucht Games, the Composition Method, and the Monadic Theory of Ordinal Words
Decision problems in buechi''s sequential calculus

--CTR
Alexander Rabinovich, On decidability of monadic logic of order over the naturals extended by monadic predicates, Information and Computation, v.205 n.6, p.870-889, June, 2007
Jean Berstel , Luc Boasson , Olivier Carton , Bruno Petazzoni , Jean-Eric Pin, Operations preserving regular languages, Theoretical Computer Science, v.354 n.3, p.405-420, 4 April 2006
Erich Grdel , Wolfgang Thomas , Thomas Wilke, Literature, Automata logics, and infinite games: a guide to current research, Springer-Verlag New York, Inc., New York, NY, 2002
morphic predicates;second-order