1: \documentclass[12pt]{article}
2: \usepackage{amssymb, amsmath}
3:
4: \allowdisplaybreaks
5:
6: %To eliminate comments, just switch % in the following two
7: %lines to the other def of \COMMENT. THe overfull box is intentional
8: %\newcommand{\COMMENT}[1]{\ \linebreak\fbox{\parbox{1.1\textwidth}{#1}}}
9: %\newcommand{\COMMENT}[1]{}
10: \parindent=0pt
11: \pagestyle{plain} % numbers on titles are not easy to implement
12: \newcommand{\longpage}{\enlargethispage{\baselineskip}}
13: \newcommand{\romanitems}{\renewcommand{\labelenumii}{(\roman{enumii})}}
14:
15:
16: % environments
17:
18: \newtheorem{theorem}{Theorem}
19: \newtheorem{lemma}[theorem]{Lemma}
20: \newtheorem{proposition}[theorem]{Proposition}
21: \newtheorem{corollary}[theorem]{Corollary}
22: \newtheorem{remark}[theorem]{Remark}
23: \newtheorem{example}[theorem]{Example}
24:
25: \newenvironment{proof}{{\em Proof.} }{\medspace}
26:
27:
28: \newcommand{\qed}{\hfill$\square$}
29: \newcommand{\PSPACE}{\mathrm{PSPACE}} %%% 060700VD
30: \newcommand{\EXPSPACE}{\mathrm{EXPSPACE}}
31: \newcommand{\N}{\mathbb{N}}
32: \newcommand{\M}{\mathbb{M}}
33: \newcommand{\R}{\mathbb{R}}
34: \newcommand{\B}{\mathbb{B}}
35: \newcommand{\dep}{\mathbin{\rule[.5ex]{1em}{.5pt}}}
36: \newcommand{\idep}{\,\rule[.35ex]{.5em}{.5pt}\,}
37: % \newcommand{\noedge}{\mathbin{\hspace{2em}}}
38:
39: \renewcommand{\phi}{\varphi}
40: \newcommand{\diese}{\mathrel{\#}}
41: \newcommand{\alp}{\mathop{\mathrm{alph}}}
42: \newcommand{\alphinf}{\mathop{\mathrm{alphinf}}}
43: \newcommand{\Alphinf}{\mathop{\mathrm{Alphinf}}}
44: \newcommand{\Min}{\mathop{\mathrm{Min}}}
45: \newcommand{\Max}{\mathop{\mathrm{Max}}}
46: \newcommand{\id}{\mathop{\mathrm{id}}}
47: \newcommand{\eval}{\mathrm{eval}}
48: \newcommand{\pexp}{\mathrm{exp}}
49: \newcommand{\leftp}{\mathrm{l}}
50: \newcommand{\rightp}{\mathrm{r}}
51: % \newcommand{\leftp}{\mathrm{left}}
52: % \newcommand{\rightp}{\mathrm{right}}
53: \newcommand{\head}{\mathrm{head}}
54: \newcommand{\Head}{\mathrm{Head}}
55: \newcommand{\body}{\mathrm{body}}
56: \newcommand{\Body}{\mathrm{Body}}
57: \newcommand{\tail}{\mathrm{tail}}
58: \newcommand{\Tail}{\mathrm{Tail}}
59: % \newcommand{\mod}{\mathop{\mathrm{mod}}}
60: \newcommand{\Trans}{\mathrm{Trans}}
61: \newcommand{\restr}{\!\!\upharpoonright}
62:
63: \newcommand{\RLangA}{P}
64: \newcommand{\RLangB}{\Pi}
65: \newcommand{\invol}{\overline{\,^{\,^{\,}}}}
66: \newcommand{\atab}{\hspace*{10mm}}
67: \newcommand{\OO}{{\mathcal O}}
68:
69: \newcommand{\ob}{\bar{b}}
70: \newcommand{\oa}{\bar{a}}
71: \newcommand{\oc}{\bar{c}}
72: \newcommand{\od}{\bar{d\,\!}}
73: \newcommand{\ox}{\overline{X}}
74: \newcommand{\oy}{\overline{Y}}
75: \newcommand{\oz}{\overline{Z}}
76:
77: \def\uwv #1{(u_{#1},w_{#1},v_{#1})}
78: \def\Fl #1#2{\uwv{#1} \cdots \uwv{#2}}
79:
80:
81: \begin{document}
82:
83: \title{The existential theory of equations with rational
84: constraints in free groups is $\PSPACE$--complete}
85: \author{Volker Diekert$^{1}$,
86: Claudio Guti{\'e}rrez$^{2}$,
87: Christian Hagenah$^{1}$}
88: \date{ \small
89: ${^{1}}$ Inst.~f{\"u}r Informatik, Universit{\"a}t Stuttgart, \\
90: Breitwiesenstr.~20-22, D-70565 Stuttgart \\
91: diekert@informatik.uni-stuttgart.de \;\;
92: christian@hagenah.de \\
93: ${^{2}}$
94: Depto. de Ciencias de la Computaci{\'o}n,
95: Universidad de Chile, \\
96: Blanco Encalada 2120, Santiago, Chile \\
97: cgutierr@dcc.uchile.cl
98: }
99: % \date{\today} % optional
100: \maketitle
101:
102:
103: \paragraph{ACM Classification}
104: F.2. Analysis of Algorithms and Problem Complexity,
105: F.2.2. Computation on Discrete Structures,
106: F.4. Mathematical Logic and Formal Languages. \\
107: {\bf Subject Descriptor} Equations in Free Groups.
108:
109:
110: \begin{abstract}
111: It is known that the existential theory of equations in free groups is
112: decidable. This is a famous result of Makanin.
113: On the other hand it has been shown that the scheme of his
114: algorithm is not primitive recursive.
115: In this paper we present an algorithm that works in polynomial space,
116: even in the more general setting where each variable has a rational
117: constraint, that is, the solution has to respect a specification given
118: by a regular word language.
119: Our main result states that the existential
120: theory of equations in free groups with rational constraints is
121: $\PSPACE$--complete. We obtain this result as a corollary of the
122: corresponding statement about free monoids with involution.
123: \end{abstract}
124:
125:
126: %%%%%%%%%%%%%%%%%%%%%%
127: \section{Introduction}\label{sec:intro}
128:
129: Around the 1980's a great progress was achieved on the algorithmic
130: decidability of elementary theories of free monoids and groups. In
131: 1977 Makanin \cite{mak77} proved that the existential theory of
132: equations in free monoids is decidable by presenting an algorithm
133: which solves the satisfiability problem for a single word equation
134: with constants. In 1983 he extended his result to the more complicated
135: framework in free groups \cite{mak83a}. In fact,
136: using a result by Merzlyakov \cite{merz66} he also showed
137: that the positive theory of equations in free groups is decidable
138: \cite{mak84}, and
139: Razborov was able to
140: give a description of the whole solution set \cite{raz84}. The
141: algorithms of Makanin are very complex: For word equations the running
142: time was first estimated by several towers of exponentials and it took
143: more than 20 years to lower it down to the best known bound for
144: Makanin's original algorithm, which is to date $\EXPSPACE$
145: \cite{gut98focs}. For solving equations in free groups Ko{\'s}cielski
146: and Pacholski \cite{kp98} have shown that the scheme proposed by
147: Makanin is not primitive recursive.
148:
149:
150: In 1999 Plandowski invented another method for solving word
151: equations and he showed that the satisfiability problem for word
152: equations is in $\PSPACE$, \cite{pla99focs}. One ingredient of his
153: work is to use data compression to reduce the exponential space to
154: polynomial space. The importance of data compression was first
155: recognized by Rytter and Plandowski when applying {L}empel-{Z}iv
156: encodings to the minimal solution of a word equation \cite{pr98icalp}.
157: Another important notion is the definition of an $\ell$-factorization
158: of the solution being explained below. Guti{\'e}rrez extended
159: Plandowski's method to the case of free groups, \cite{gut2000stoc}.
160: Thus, a non-primitive recursive scheme for solving equations in free
161: groups has been replaced by a polynomial space bounded algorithm.
162: Hagenah and Diekert worked independently in the same direction and
163: using some ideas of Guti{\'e}rrez they obtained a result which
164: includes the presence of rational constraints. This appeared as extended
165: abstract in \cite{dgh2001} and also
166: as a part
167: of the PhD-thesis of Hagenah \cite{hagenahdiss2000}.
168:
169: The present paper is a journal version of
170: \cite{dgh2001,gut2000stoc}. It shows that the existential theory of
171: equations in free groups with rational constraints is
172: $\PSPACE$--complete. Rational constraints mean that a possible
173: solution has to respect a specification which is given by a regular
174: word language. The idea to consider regular constraints for word
175: equations goes back to Schulz \cite{sch91} who also pointed out the
176: importance of this concept, see also \cite{dmm99tcs,gv97icalp}.
177: The
178: $\PSPACE$--completeness for the case of word equations with regular
179: constraints has been stated by Rytter already, as cited in
180: \cite[Thm.~1]{pla99focs}.
181:
182: Our proof reduces the case of equations with rational constraints in free groups
183: to the case equations with regular constraints in free monoids with involution,
184: which turns out to be the central object.
185: (Makanin uses the notion of ``paired alphabet'', but a main difference is that
186: he considered ``non contractible'' solutions only, whereas we deal
187: with general solutions and, in addition, we have constraints.)
188: During our work we extend the method of
189: \cite{pla99focs} such that it copes with the involution and the method
190: of \cite{gut2000stoc} such that it copes with rational constraints.
191: The first step is a reduction to the satisfiability problem of a
192: single equation with regular constraints in a free monoid with
193: involution. In order to avoid an exponential blow-up, we do not use a
194: reduction as in \cite{mak84}, but a simpler one. In particular, we can
195: handle negations simply by positive rational constraints. In the
196: second step we show that the satisfiability problem of a single
197: equation with regular constraints in a free monoid with involution is
198: still in $\PSPACE$. This part is rather technical and we introduce
199: several new notions like base-change, projection, partial solution, and free
200: interval. The careful handling of free intervals is necessary because
201: of the constraints. In some sense this is the only additional
202: difficulty which we will meet when dealing with constraints. After
203: these preparations we can follow Plandowski's method.
204: Throughout we shall use many of the deep ideas which were presented
205: in \cite{pla99focs}, and apply them in a different setting.
206: Hence, as we cannot use
207: Plandowski's result as a black box, we have to go through the whole
208: construction again. As a result our paper is (involuntarily)
209: self-contained, up to standard knowledge in combinatorics on words and
210: linear Diophantine equations.
211:
212:
213: \section{Free Groups and their Rational Subsets}
214:
215: Let $\Sigma$ be a finite alphabet. By $F(\Sigma)$ we denote the free group
216: over $\Sigma$. Elements of $F(\Sigma)$ can be represented by words in
217: $(\Sigma \cup \overline{\Sigma})^{*}$, where
218: $\overline{\Sigma}= \{\, \overline{a} \mid a \in \Sigma \,\}$. We read
219: $\overline{a}$ as $a^{-1}$ in $F(\Sigma)$ and we use the convention that
220: $\overline{\overline{a}}=a$.
221: Hence the set $\Gamma=\Sigma \cup \overline{\Sigma}$ is equipped with an
222: involution
223: $\invol:\Gamma \to \Gamma$;
224: the involution is extended to $\Gamma^{*}$ by
225: $\overline{a_1 \cdots a_n} = \overline{a_n} \cdots \overline{a_1}$ for
226: $n \geq 0$ and $a_i \in \Gamma$, $1 \leq i \leq n$.
227: The empty word as well as the unit element in other monoids
228: is denoted by $1$. By $\psi : \Gamma^* \to
229: F(\Sigma)$ we denote the canonical homomorphism.
230: A word $w \in \Gamma^*$ is {\em freely reduced\/}, if it
231: contains no factor of the form $a \overline{a}$ with $a \in \Gamma$.
232: The
233: reduction of a word $w \in \Gamma^*$ can be computed by using the Noetherian
234: and confluent rewriting system $\{\,a\overline{a}\rightarrow 1 \mid a \in \Gamma\,\}$.
235: For $w \in \Gamma^*$ we denote by $\widehat w$ the freely reduced word which denotes
236: the same group element in $F(\Sigma)$ as $w$.
237: Hence, $\psi(u)=\psi(v)$ if and only if $\widehat u=\widehat v$ in $\Gamma^*$.
238:
239: The class of {\em rational languages} in $F(\Sigma)$ is inductively defined
240: as follows: Every finite subset of $F(\Sigma)$ is
241: rational.
242: If
243: $\RLangA_1,\RLangA_2 \subseteq F(\Sigma)$ are rational, then
244: $\RLangA_1 \cup \RLangA_2$, $\RLangA_1 \cdot \RLangA_2$, and
245: $\RLangA_1^*$ are rational. Hence, $\RLangA \subseteq F(\Sigma)$ is
246: rational if and only if $\RLangA=\psi(\RLangA')$ for some regular
247: language $\RLangA' \subseteq \Gamma^*$.\footnote{We
248: follow the usual convention to call a rational
249: subset of a free monoid {\em regular}.
250: This convention is due to Kleene's Theorem
251: stating that regular, rational, and recognizable
252: have the same meaning in free monoids. But in free
253: groups these notions are different and we have
254: to be more precise.} In particular, we can use
255: a non-deterministic
256: finite automata over $\Gamma$ for specifying rational group
257: languages over $F(\Sigma)$.
258:
259:
260: The following proposition is due to M.~Benois \cite{ben69},
261: see also \cite[Sect. III. 2] {berstel79}.
262:
263: \begin{proposition} \label{benois}
264: Let $\RLangA' \subseteq \Gamma^*$ be a regular language and
265: $\RLangA=\psi(\RLangA') \subseteq F(\Sigma)$. Then we effectively find a
266: regular language $\widetilde{\RLangA}'\subseteq \Gamma^*$ such that
267: $\widetilde{\RLangA}'=\{\,\widehat w \in \Gamma^* \mid \psi(w) \not\in \RLangA
268: \,\}$.
269: Hence,
270: the complement of $\RLangA$ is the rational group language
271: $\psi(\widetilde{\RLangA}')$
272: and the family of rational group languages is an effective Boolean algebra.
273: \end{proposition}
274:
275: \begin{proof}
276: (Sketch) Using the same state set (and some additional transitions
277: which are labeled with the empty word) we can construct (in polynomial
278: time) a finite automaton which accepts the following language
279: $$\RLangA''=\{\,v \in \Gamma^* \mid \exists u\in \RLangA':
280: u \stackrel{*}{\rightarrow} v \,\}$$
281: where $u \stackrel{*}{\rightarrow} v$ means that $v$ is a descendant of $u$ by
282: the convergent rewriting system $\{\,a \overline{a} \rightarrow 1 \mid a \in
283: \Gamma\,\}$.
284: Then we complement $\RLangA''$ with respect to
285: $\Gamma^*$; and we build the intersection
286: with the regular set of freely reduced words.\qed
287: \end{proof}
288:
289: \section{The Existential Theory}
290:
291: In the following $\Omega$ denotes a finite set of variables (or unknowns) and we
292: let $\invol:\Omega \to \Omega$ be an involution without
293: fixed points. Clearly, if $X \in \Omega$ has an interpretation in $F(\Sigma)$,
294: then we read $\overline{X}$ as $X^{-1} \in F(\Sigma)$.
295:
296: The {\em existential theory of equations with rational constraints in free groups} is
297: inductively defined as follows. Atomic formulae are either of the form $W=1$,
298: where $W \in (\Gamma \cup \Omega)^*$ or of the form $X \in \RLangA$,
299: where $X$ is in
300: $\Omega$ and $\RLangA \subseteq F(\Sigma)$ is a rational language. A propositional
301: formula is build up by atomic formulae using negations, conjunctions and
302: disjunctions. The existential theory refers to closed existentially quantified
303: propositional formulae which evaluate to {\em true\/} over $F(\Sigma)$.
304:
305: \begin{theorem} \label{theo1}
306: The following problem is $\PSPACE$--complete.
307:
308: INPUT: A closed existentially quantified propositional formula with rational
309: constraints in the free group $F(\Sigma)$ for some finite alphabet $\Sigma$.
310:
311: QUESTION: Does the formula evaluate to {\em true\/} over $F(\Sigma)$?
312: \end{theorem}
313:
314: The $\PSPACE$--hardness follows {}from a result of Kozen
315: \cite{koz77}, since (due to the constraints) the {\em empty
316: intersection} problem of regular sets can easily be encoded in the
317: problem above. The same argument applies to Theorems~\ref{theo2} and
318: \ref{theo3} below and therefore the $\PSPACE$--hardness is not
319: discussed further in the sequel: We have to show the inclusion in $\PSPACE$,
320: only.
321:
322:
323: The $\PSPACE$ algorithm for solving Theorem~\ref{theo1} will be
324: described by a (highly) non-deterministic procedure. We will make sure
325: that if the input evaluates to true, then at least one possible output
326: is true. If it evaluates to false, then no (positive) output is
327: possible. By standard methods (Savitch's Theorem) such a procedure can
328: be transformed into a polynomial space bounded deterministic decision
329: procedure, see any textbook on complexity theory,
330: e.g.~\cite{hu79,pap94}.
331:
332: We start the procedure as follows. Using the rules of DeMorgan we may assume
333: that there are no negations at all, but the atomic formulae are now of the
334: either form: $W=1$, $W \neq 1$, $X \in \RLangA$, $X \not\in \RLangA$ with
335: $W\in (\Gamma \cup \Omega)^*$, $X \in \Omega$, and $\RLangA \subseteq F(\Sigma)$
336: rational.\footnote{The reason that we keep $X \not\in \RLangA$ instead of
337: $X \in \widetilde \RLangA$ where $\widetilde \RLangA = F(\Sigma) \setminus \RLangA$ is
338: that the complementation may involve an exponential blow-up of the state space;
339: this has to be avoided.}
340:
341: The next step is to replace every formula $W \neq 1$ by
342: $$\exists X: WX=1 \wedge X \not\in \{1\},$$
343: where X is a fresh variable, hence we can put $\exists X$ to the front. Now we
344: eliminate all disjunctions. More precisely, every subformula of type $A \vee B$
345: is non-deterministically replaced either by $A$ or by $B$. At this stage the
346: propositional formula has become a conjunction of formulae of type $W=1$,
347: $X \in \RLangA$, $X \not\in \RLangA$ with $W \in (\Gamma \cup \Omega)^*$,
348: $X \in \Omega$, and $\RLangA \subseteq F(\Sigma)$ rational.
349:
350: We may assume that $|W|\geq 3$, since
351: if $1 \leq |W| < 3$, then we may replace $W=1$ by $Wa\overline{a}=1$
352: for some $a \in \Gamma$. For the following it is convenient to assume
353: that $|W|=3$ for all subformulae $W=1$. This is also easy to achieve. As
354: long as there is a subformula $x_1 \cdots x_k = 1$, $x_i \in \Gamma
355: \cup \Omega$ for $1 \leq i \leq k$ and $k \geq 4$, we replace it by the
356: conjunction
357: $$\exists Y: x_1 x_2 Y = 1 \wedge \overline{Y} x_3 \cdots x_k=1,$$
358: where $Y$ is a fresh variable and $\exists Y$ is put to the front, and
359: then proceed recursively.
360: This finishes the first phase. The output of this phase is a system of atomic
361: formulae of type $W=1$, $X \in \RLangA$, $X \not\in \RLangA$ with
362: $W \in (\Gamma \cup \Omega)^3$, $X \in \Omega$, and $\RLangA \subseteq
363: F(\Sigma)$ rational.
364:
365: At this point we switch to the existential theory of equations with
366: regular constraints in free monoids where these monoids
367: have an involution. Recall that $X
368: \in \RLangA$ (resp. $X \not\in \RLangA$) means in fact $X \in
369: \psi(\RLangA')$ (resp. $X \not\in \psi(\RLangA')$) where $\RLangA'
370: \subseteq \Gamma^*$ is a regular word language specified by some
371: finite non-deterministic automaton.
372: Using $\psi$-symbols we obtain an interpretation over
373: $(\Gamma^*,\invol)$ without changing the truth value by
374: replacing syntactically each subformula $X \in \RLangA$ (resp. $X
375: \not\in \RLangA$) by $\psi(X) \in \psi(\RLangA')$ (resp. $\psi(X)
376: \not\in \psi(\RLangA')$) and by replacing each subformula $W=1$ by
377: $\psi(W)=1$.
378:
379: We keep the interpretation over words,
380: but we eliminate now all occurrences of $\psi$ again. We begin with the
381: occurrences of $\psi$ in the constraints. Let $\RLangA' \subseteq
382: \Gamma^*$ be regular being accepted by some finite automaton with
383: state set $Q$. As stated in the in the first part of the proof of
384: Proposition~\ref{benois}, we construct a finite automaton, using the
385: same state set, which accepts the following language
386: $$\RLangA''=\{\,v \in \Gamma^* \mid \exists u\in \RLangA':
387: u \stackrel{*}{\rightarrow} v \,\}.$$
388: In particular, $\psi(\RLangA') = \psi(\RLangA'')$ and
389: $\widehat \RLangA \subseteq \RLangA''$ where
390: $\widehat \RLangA = \{\,\widehat u \in \Gamma^* \mid u \in \RLangA'\,\}$.
391:
392: We replace all positive atomic subformulae of the form
393: $\psi(X) \in \psi(\RLangA')$ by $X \in \RLangA''$. A simple reflection shows that
394: the truth value has not changed since we can think of $X$ of being a freely reduced
395: word. For a negative formulae $\psi(X) \not\in \psi(\RLangA')$ we have to be a
396: little more careful. Let $N \subseteq \Gamma^*$ be the regular set of all
397: freely reduced words. The language $N$ is accepted by a deterministic finite automaton
398: with $|\Gamma|+1$ states. We replace $\psi(X) \not\in \psi(\RLangA')$ by
399: \[
400: X \not\in \RLangA'' \wedge X \in N,
401: \]
402: where $\RLangA''$ is as above. Again the truth value did not change.
403:
404: We now have to deal with the formulae $\psi(xyz)=1$ where $x,y,z \in \Gamma \cup
405: \Omega$. Observe that the underlying propositional formula is satisfiable over
406: $\Gamma^*$ if and only if it is satisfiable in freely reduced words. The following
407: lemma is well-known. Its easy proof is left to the reader.
408:
409: \begin{lemma} \label{lem1}
410: Let $u,v,w \in \Gamma^*$ be freely reduced words. Then we have
411: $\psi(uvw)=1$ (i.e. $uvw=1$ in $F(\Sigma)$) if and only if there are
412: words $P, Q, R \in \Gamma^*$ such that $u=PQ$, $v=\overline{Q}R$, and
413: $w=\overline{R}\,\overline{P}$ holds in $\Gamma^*$.
414: \end{lemma}
415:
416: Based on this lemma we replace each atomic subformulae $\psi(xyz)=1$ with $x,y,z
417: \in \Gamma \cup \Omega$ by a conjunction
418: $$\exists P \exists Q \exists R: x=PQ \wedge y=\overline{Q}R \wedge
419: z=\overline{R}\,\overline{P},$$
420: where $P$, $Q$, $R$ are fresh variables
421: and the existential block is put to the front. The new existential
422: formula has no occurrence of $\psi$ anymore. The atomic subformulae
423: are of the form $x=yz$, $X \in \RLangA$, $X \not\in \RLangA$, where
424: $x,y,z\in \Gamma \cup \Omega$ and $\RLangA \subseteq \Gamma^*$ is
425: regular. The size of the formula is linear in the size of the original
426: formula. Therefore Theorem~\ref{theo1} is a consequence of Theorem~\ref{theo2}.
427:
428: \section{Free Monoids with Involution}
429:
430: As above, let $\Gamma$ be an alphabet of constants and $\Omega$ be an alphabet of
431: variables. There are involutions $\invol:\Gamma \to
432: \Gamma$ and $\invol:\Omega \to \Omega$. The involution
433: on $\Omega$ is without fixed points, but we explicitly allow fixed points for
434: the involution on $\Gamma$.
435: \footnote {Fixed points for
436: the involution on constants are needed in the proof later anyhow
437: and this more general setting leads to further applications, \cite{dl2001}}
438: The involution is extended to
439: $(\Gamma \cup \Omega)^*$ by
440: $\overline{x_1 \cdots x_n} = \overline{x_n} \cdots \overline{x_1}$ for
441: $n \geq 0$ and $x_i \in \Gamma \cup \Omega$, $1 \leq i \leq n$.
442:
443: {}From now on, all monoids $M$ under consideration are equipped with
444: an involution $\invol:M \to M$, i.e. we have $\overline{1} = 1$ for
445: the unit element, $\overline{\overline{x}}=x$, and
446: $\overline{xy}=\overline{y}\,\overline{x}$ for all $x,y\in M$. A
447: homomorphism between monoids $M$ and $M'$ is therefore a mapping $h: M
448: \to M'$ such that $h(1)=1$, $h(xy)=h(x)h(y)$, and
449: $h(\overline{x})=\overline{h(x)}$ for all $x,y \in M$. The pair
450: $(\Gamma^*, \invol)$ is called a \emph{free monoid with
451: involution}.
452: \footnote{Note that $(\Gamma^*, \invol)$
453: is a free monoid which has an involution, but
454: it is not a free object in the category of
455: monoids with involution, as soon as the involution has fixed points.}
456:
457: The existential theory of equations with regular constraints in free
458: monoids with involution is based on atomic formulae of type $U=V$
459: where $U,V \in (\Gamma \cup \Omega)^*$ and of type $X \in \RLangA$
460: where $X \in \Omega$ and $\RLangA \subseteq \Gamma^*$ is a regular
461: language specified by some non-deterministic finite automaton. Again,
462: a propositional formula is build up by atomic formulae using
463: negations, conjunctions and disjunctions. The existential theory
464: refers to closed existentially quantified propositional formulae which
465: evaluate to {\em true\/} over $(\Gamma^*,\invol)$.
466:
467: The following statement is the main result of the paper.
468:
469: \begin{theorem} \label{theo2}
470: The following problem is $\PSPACE$--complete.
471:
472: INPUT: A closed existentially quantified propositional formula with regular
473: constraints in a free monoid with involution over $(\Gamma, \invol)$.
474:
475: QUESTION: Does the formula evaluate to {\em true\/} over $(\Gamma^*,\invol)$?
476: \end{theorem}
477:
478:
479:
480: The proof of Theorem~\ref{theo2} is in a first step
481: (next section) a reduction
482: to Theorem~\ref{theo3}. The proof of Theorem~\ref{theo3}
483: will be the essential technical contribution.
484:
485: \section{From Regular Constraints to Boolean Matrices
486: and a Single Equation}
487:
488: The first part of the proof is very similar to what we have done above.
489: By DeMorgan we have no negations and all subformulae are of type
490: $U=V$, $U \neq V$, $X \in \RLangA$, $X \not\in \RLangA$, where
491: $U,V \in (\Gamma \cup \Omega)^*$, $X \in \Omega$, and $\RLangA \subseteq \Gamma^*$
492: is regular.
493:
494: Since we work over a free monoid $\Gamma^*$ it is easy to handle inequalities
495: $U \neq V$ where $U,V \in (\Gamma \cup \Omega)^*$.
496: We recall it under the assumption $|\Gamma| \geq 2$:
497: A subformulae $U\neq V$ is replaced by
498: \[
499: \exists X \exists Y \exists Z: \bigvee_{a \neq b}
500: (U=VaX \vee V=UaX \vee (U=XaY \wedge V=XbZ)).
501: \]
502: Making guesses we can eliminate all disjunctions and we obtain a
503: propositional formula which is a single conjunction over subformulae of type
504: $U=V$, $X \in \RLangA$, and $X \not\in \RLangA$ where
505: $U,V \in (\Gamma \cup \Omega)^*$, $X \in \Omega$, and
506: $\RLangA \subseteq \Gamma^*$ is regular.
507:
508: By another standard procedure we can replace a conjunction of word
509: equations over $(\Gamma \cup \Omega)^*$ by a single word equation
510: $L=R$ with $L,R \in (\Gamma \cup \Omega)^+$. For example,
511: we may choose a new letter $a$ and then
512: we can replace a system
513: $L_1 = R_1$, $L_2 = R_2, \ldots , L_k = R_k$ by
514: $L_1a L_2a \cdots a L_k = R_1a R_2a \cdots a R_k$ and a list
515: $X \in \Gamma^*$ for all $X \in \Omega$;
516: this works since $a \not\in \Gamma$.
517:
518: Therefore we may assume
519: that our input is given by a single equation
520: $L=R$ with $L,R \in (\Gamma \cup \Omega)^+$ and by two lists $(X_j \in
521: \RLangA_j, 1\leq j \leq m)$ and $(X_j \not\in \RLangA_j, m < j \leq
522: k)$ where $X_j \in \Omega$ and each regular
523: language $\RLangA_j \subseteq \Gamma^*$ is specified by some
524: non-deterministic automaton ${\mathcal A}_j = (Q_j, \Gamma, \delta_j,
525: I_j, F_j)$ where $Q_j$ is the set of states, $\delta_j \subseteq Q_j
526: \times \Gamma \times Q_j$ is the transition relation, $I_j \subseteq
527: Q_j$ is the subset of initial states, and $F_j \subseteq Q_j$ is the
528: subset of final states, $1 \leq j \leq k$. Of course, a variable $X$
529: may occur several times in the list with different constraints,
530: therefore we might have $k$ greater than $|\Omega|$.
531: The question is whether there is a solution.
532:
533: A \emph{solution} is a mapping $\sigma: \Omega \to
534: \Gamma^*$
535: being extended
536: to a homomorphism $\sigma: (\Gamma \cup \Omega)^* \to \Gamma^*$ by
537: leaving the letters from $\Gamma$ invariant such that the
538: following conditions are satisfied:
539: \[
540: \begin{array}{rcll}
541: \sigma(L) & = & \sigma(R), \\
542: \sigma(\overline{X})& = &\overline{\sigma(X)}&\textrm{for } X \in \Omega,\\
543: \sigma(X_j) & \in & \RLangA_j & \textrm{for } 1\leq j \leq m,\\
544: \sigma(X_j) & \not\in & \RLangA_j &\textrm{for } m < j \leq k.
545: \end{array}
546: \]
547:
548: For the next steps it turns out to be more convenient
549: to work within the framework of Boolean matrices instead of finite automata:
550: Let $Q$ be the disjoint union of the state spaces $Q_j$, $1 \leq j \leq k$.
551: We may assume that $Q=\{1,\ldots,n\}$. Let
552: $\delta = \bigcup_{1 \leq j \leq k} \delta_j$, then
553: $\delta \subseteq Q \times \Gamma \times Q$ and with each $a \in \Gamma$ we
554: can associate a Boolean $n \times n$ matrix $g(a) \in \B^{n \times n}$
555: such that $g(a)_{i,j} = $ ``$(i, a, j) \in \delta$'' for $1 \leq i,j \leq n$.
556: Since our monoids should have an involution, we
557: shall in fact work with $2n \times 2n$ matrices.
558: Henceforth $M \subseteq \B^{2n \times 2n}$ denotes the following monoid with
559: involution:
560: $$M= \{\, \begin{pmatrix}A & 0 \\ 0 & B \end{pmatrix}
561: \mid A,B \in \B^{n \times n} \,\},$$
562: where $$ \overline{ \begin{pmatrix} A & 0 \\ 0 & B \end{pmatrix}} =
563: \begin{pmatrix} B^T & 0 \\ 0 & A^T \end{pmatrix}$$
564: and the operator ${\ }^T$ denotes the transposition. We define a homomorphism
565: $h: \Gamma^* \to M$ by
566: $$h(a)=\begin{pmatrix} g(a) & 0 \\ 0 & g(\overline{a})^T \end{pmatrix}
567: \,\textrm{for}\, a \in \Gamma,$$
568: where the mapping
569: $g: \Gamma \to \B^{n \times n}$ is defined as above. The homomorphism $h$
570: can be computed in polynomial time and it respects the involution. Now, for
571: each regular language $\RLangA_j$, $1 \leq j \leq k$ we compute vectors
572: $I_j, F_j \in \B^{2n}$ such that for all $w \in \Gamma^*$ and $1 \leq j \leq k$
573: we have the equivalence:
574: $$w \in \RLangA_j \Leftrightarrow I_{j}^T h(w) F_j =1.$$
575: Having done these computations we make a non-deterministic guess
576: $\rho(X) \in M$ for each variable $X \in \Omega$. We verify
577: $\rho(\overline{X})=\overline{\rho(X)}$ for all
578: $X \in \Omega$ and whenever there is a constraint of type $X \in \RLangA_j$
579: for some $1 \leq j \leq m$ (or $X \not\in \RLangA_j$ for some $m<j \leq k$),
580: then we verify $I_{j}^T \rho(X) F_j=1$, if $1 \leq j \leq m$ (or
581: $I_{j}^T \rho(X) F_j=0$, if $m<j \leq k$).
582:
583: After these preliminaries, we introduce the formal definition of an
584: {\em equation $E$ with constraints}:
585: Let $d,n\in \N$ and let $M \subseteq
586: \B^{2n \times 2n}$ be the monoid with involution defined above. We
587: consider an equation of length $d$ over some $\Gamma$ and $\Omega$
588: with constraints in $M$ being specified by a list $E$ containing the
589: following items:
590: \begin{itemize}
591: \item The alphabet $(\Gamma,\invol)$ with involution.
592: \item The homomorphism $h: \Gamma^* \to M$ which is specified by a
593: mapping $h: \Gamma \to M$ such that
594: $h(\overline{a})=\overline{h(a)}$ for all
595: $a \in \Gamma$.
596: \item The alphabet $(\Omega,\invol)$ with involution without fixed points.
597: \item A mapping $\rho: \Omega \to M$ such that
598: $\rho(\overline{X})=\overline{\rho(X)}$ for all
599: $X \in \Omega$.
600: \item The equation $L=R$ where $L,R \in (\Gamma \cup \Omega)^+$ and $|LR|=d$.
601: \end{itemize}
602: We will denote this list simply by
603: \[
604: E = (\Gamma, h, \Omega, \rho ; L=R).
605: \]
606:
607: A convenient definition for the input size is
608: given by $n + d + \log_2(|\Gamma|+|\Omega|)$.
609: This definition takes into account that there might be constants
610: or variables with constraints which are not present in the equation.
611: Recall that $n$ refers to the dimension of the boolean matrices, and
612: this parameter is part of the input.
613:
614:
615: A {\em solution} of $E$ is
616: a mapping $\sigma: \Omega \to \Gamma^*$ (being extended
617: to a homomorphism $\sigma: (\Gamma \cup \Omega)^* \to \Gamma^*$
618: by leaving the letters from $\Gamma$ invariant) such that the following
619: three conditions are satisfied:
620: \begin{eqnarray*}
621: \sigma(L) & = & \sigma(R), \\
622: \sigma(\overline{X}) & = & \overline{\sigma(X)} \,
623: \textrm{for all}\, X\in \Omega, \\
624: h\sigma(X) & = & \rho(X) \,\textrm{for all}\, X\in \Omega.
625: \end{eqnarray*}
626: By the
627: reduction above, Theorem~\ref{theo2} is a consequence of the next statement
628: which says that the satisfiability problem of equations with constraints
629: can be solved in polynomial space.
630:
631: \begin{theorem} \label{theo3}
632: The following problem is $\PSPACE$--complete.
633:
634: INPUT: An equation $E_0$ with constraints
635: $E_0 = (\Gamma_0, h_0 , \Omega_0, \rho_0 ; L_0=R_0).$
636:
637: QUESTION: Is there a solution $\sigma : \Omega_0 \to \Gamma_0^*$?
638: \end{theorem}
639:
640: For the proof we need an explicit space
641: bound. Therefore we fix some polynomial $p$ and and
642: we allow working space $p(n + d + \log_2(|\Gamma|+|\Omega|)$.
643: An appropriate choice of the polynomial $p$
644: can be calculated {}from the presentation below.
645: What is important is that the notions of
646: {\em admissibility\/} being used in the next sections always refer to some fixed polynomials.
647: The following lemma states that some basic operations, which
648: we have to perform several times
649: can be done in $\PSPACE$.
650:
651: \begin{lemma} \label{basicops}
652: The following two problems can be
653: solved in polynomial space with respect to the
654: input size $ n + \log ( |\Gamma|)$.
655:
656: \smallbreak
657: INPUT: A matrix $A \in M$ and a mapping
658: $h: \Gamma \to M$.
659:
660: QUESTION: Is there some $w \in \Gamma^*$ such that $h(w)=A$?
661: \smallbreak
662: INPUT: A matrix $A \in M$ and a mapping
663: $h: \Gamma \to M$.
664:
665: QUESTION: Is there some $w \in \Gamma^*$ such that $h(w)=A$ and
666: $w=\overline{w}$?
667: \end{lemma}
668: \begin{proof}
669: The first question can be solved by guessing a word $w$
670: letter by letter and calculating $h(w)$. The second question can be
671: solved since $w=\overline{w}$ implies $w=ua\overline{u}$ for some
672: $u \in \Gamma^*$ and $a \in \Gamma \cup \{1\}$ with $a=\overline{a}$. Hence
673: we can guess $u$ and $a$. During the guess we compute
674: $B=h(u)$ and then we verify $A=Bh(a)\overline{B}$. \qed
675: \end{proof}
676:
677: Here is a first application of Lemma~\ref{basicops}: Assume that an equation with constraints
678: $E = (\Gamma, h , \Omega, \rho ; L=R)$
679: contains in the specification some variable $X$ which does not occur
680: in $LR\overline{LR}$, then the equation might be unsolvable, simply
681: because $\rho(X) \not\in h(\Gamma^*)$. However, by
682: the lemma above
683: we can test this in $\PSPACE$. If $\rho(X) \in h(\Gamma^*)$,
684: then we can safely cancel $X$ and $\overline{X}$.
685: Thus, we put this test in the preprocessing,
686: and in the following we shall assume that all variables occur
687: somewhere in
688: $LR\overline{LR}$. In particular, we may assume $|\Omega| \leq 2|LR|$.
689:
690:
691: \section{The Exponent of Periodicity}
692: \label{teop }
693: A key step in proving Theorem~\ref{theo3}
694: is to find a bound on the exponent of periodicity
695: in a minimal solution.
696: This idea is used in all known algorithms for solving
697: word equations in general,
698: c.f., \cite{mak77,pla99focs}.
699:
700: Let $w \in \Gamma^*$ be a word. The exponent of periodicity $\pexp(w)$ is
701: defined by
702: $$\pexp(w) = \sup \{\,\alpha \in \N \mid \exists u,v,p \in \Gamma^*,p \neq 1:
703: w=u p^\alpha v\,\}.$$
704: We have $\pexp(w)>0$ if and only if $w$ is not the empty word. Let
705: $E = (\Gamma, h, \Omega, \rho, L=R)$
706: be an equation with constraints. The exponent
707: of periodicity of $E$ is also denoted by $\pexp(E)$. It is defined by
708: $$\pexp(E) = \inf\{ \{\,\pexp(\sigma(L)) \mid
709: \sigma {\rm\,is\,a\,solution\,of\,} E\,\} \cup \{\infty\} \, \}.$$
710: By definitions we have $\pexp(E) < \infty$ if and only if $E$ is solvable.
711: Here we show that the well-known result from word equations
712: \cite{kp96} transfers to the situation here. The exponent of periodicity of
713: a solvable equation can be bounded by a singly exponential function.
714: Thus, in the following sections we shall assume that if $E_0$
715: is solvable, then $\pexp(E_0) \in 2^{\OO(d+n\log n)}$.
716: This is the content of the next proposition.
717:
718: \begin{proposition}\label{singleexp}
719: Let $ E = (\Gamma,h, \Omega, \rho; L=R)$ be an equation with constraints and
720: let $\sigma:\Omega \rightarrow \Gamma^*$ be a solution. Then we
721: find effectively a solution $\sigma':\Omega \rightarrow \Gamma^*$
722: such that $\exp(\sigma'(L)) \in 2^{\OO(d + n\log n)}$.
723: \end{proposition}
724:
725: The rest of this section is devoted to prove
726: Proposition~\ref{singleexp}.
727: Since it follows standard lines, the proof
728: can be skipped in a first reading.
729:
730:
731:
732: \begin{proof}
733: Let $p\in A^{+}$ be a primitive word. In our setting the definition of
734: the {\em $p$-stable normal
735: form} of a word $w \in A^*$
736: depends on the property whether or not $\overline{p}$
737: is a factor of $p^2$. So we distinguish two cases
738: and in the following we also write
739: $p^{-1}$
740: for denoting $\overline{p}$. Then, for example, $p^{-3}$
741: means the same as $\overline{p}^{3}$.
742:
743:
744: First case: We assume that $\overline{p}$ is not a factor of $p^2$.
745: The idea is to replace each maximal factor of the form $p^{\alpha}$
746: with $\alpha \geq 2$ by a sequence $p,\alpha - 2,p$ and each maximal
747: factor of the form $\overline{p}^{\alpha}$ with $\alpha \geq 2$ by a
748: sequence $\overline{p},-(\alpha - 2),\overline{p}$.
749: This leads to the following notion:
750:
751:
752:
753: The {\em $p$-stable normal
754: form} (first kind) of $w \in A^*$
755: is a
756: shortest sequence ($k$ is minimal)
757: \[
758: ( u_{0},\varepsilon_{1}\alpha _{1},u_{1},\ldots ,
759: \varepsilon_{k}\alpha _{k},u_{k})
760: \]
761: such that $k\geq 0$, $u_{0},u_{i}\in A^{*}$, $\varepsilon_{i} \in
762: \{+1,-1\}$,
763: $\alpha _{i}\geq 0$
764: for
765: $1\leq i\leq k$, and the following conditions are satisfied:
766: \begin{itemize}
767: \item $w=u_{0}p^{\varepsilon_{1}\alpha _{1}}u_{1}\cdots
768: p^{\varepsilon_{k}\alpha _{k}}u_{k}$.
769:
770: \item $k=0$ if and only if neither $p^{2}$
771: nor $\overline{p}^2$ is a factor of $w.$
772:
773: \item If $k\geq 1$, then:
774: \begin{eqnarray*}
775: u_{0} &\in &A^{*}p^{\varepsilon_{1}}\setminus A^{*}p^{\pm 2}A^{*}, \\
776: u_{i} &\in &( A^{*}p^{\varepsilon_{i+1}}\cap p^{\varepsilon_{i}} A^{*})
777: \setminus A^{*}p^{\pm 2}A^{*}\,
778: \mbox{ for }1\leq i<k, \\
779: u_{k} &\in & p^{\varepsilon_{k}}A^{*}\setminus A^{*}p^{\pm 2}A^{*}.
780: \end{eqnarray*}
781: \end{itemize}
782: % \e{definition}
783:
784: The $p$-stable normal form of $\overline{w}$
785: becomes
786: $$( \overline{u_{k}},-\varepsilon_{k}\alpha _{k},u_{k-1},\ldots
787: ,-\varepsilon_{1}\alpha _{1},\overline{u_{0}}) .$$
788:
789: \begin{example} Let $ p = a\overline{a}ba\overline{a} $ with $b \not=\overline{b}$
790: and $w = p^4\overline{b}a\overline{a} p^{-1}a\overline{a}\overline{b}p^{-2}$.
791: Then the $p$-stable normal form of $w$ is:
792: $$
793: (\overline{a}a\overline{a}b, 2, a\overline{a}ba\overline{a}\overline{b}a\overline{a}, -1,
794: a\overline{a}\overline{b}a\overline{a}\overline{b}a\overline{a},0,
795: a\overline{a}\overline{b}a\overline{a}).
796: $$
797: \end{example}
798:
799: Second case: We assume that
800: $\overline{p}$
801: is a factor of $p^2$. Then we can write $p =rs$ with
802: $\overline{p} = sr$ and $r = \overline{r}$, $s = \overline{s}$.
803: We allow $ r =1$, hence the second case includes the case $p =
804: \overline{p}$. In fact, if $ r =1$, then below we obtain
805: the usual definition of $p$-stable normal
806: form.
807: Moreover, by switching to some conjugated word of $p$
808: we could always assume that $r \in \{1, a\}$ for some letter $a$
809: being fixed by the involution, $a = \overline{a}$,
810: but this switch is not made here.
811: The idea is to replace each maximal factor of the form $(rs)^{\alpha}r$
812: with $\alpha \geq 2$ by a sequence $rs,\alpha - 2,sr$.
813: In this notation
814: $\alpha - 2$ is representing the factor $(rs)^{\alpha -2}r
815: =p^{\alpha - 2}r = r \overline{p}^{\alpha - 2} $.
816:
817:
818: The {\em $p$-stable normal
819: form} (second kind) of $w \in A^*$
820: is now a
821: shortest sequence ($k$ is minimal)
822: \[
823: ( u_{0},\alpha _{1},u_{1},\ldots ,
824: \alpha _{k},u_{k})
825: \]
826: such that $k\geq 0$, $u_{0},u_{i}\in A^{*},\;\alpha _{i}\geq 0$ for
827: $1\leq i\leq k$, and the following conditions are satisfied:
828: \begin{itemize}
829: \item $w=u_{0}p^{\alpha _{1}} r u_{1}\cdots
830: p^{\alpha _{k}} r u_{k}$.
831:
832: \item $k=0$ if and only if $p^2 r$ is
833: not a factor of $w.$
834:
835: \item If $k\geq 1$, then:
836: \begin{eqnarray*}
837: u_{0} &\in &A^{*}rs\setminus (A^{*}p^{2}rA^{*} \cup A^*rs rs), \\
838: u_{i} &\in &( A^{*}rs \cap srA^{*})
839: \setminus (srsr A^* \cup A^{*}p^{2}rA^{*}\cup A^*rs rs)\,
840: \mbox{ for }1\leq i<k, \\
841: u_{k} &\in & srA^{*}\setminus (A^{*}p^{2}rA^{*}\cup srsrA^*).
842: \end{eqnarray*}
843: \end{itemize}
844: % \e{definition}
845:
846: Since $\overline{rs} =sr$,
847: the $p$-stable normal form of $\overline{w}$
848: becomes
849: $$( \overline{u_{k}},\alpha _{k},u_{1},\ldots
850: ,\alpha _{1},\overline{u_{0}}). $$ So, for the second kind no negative
851: integers interfere.
852:
853:
854: \begin{example} Let $ p = a\overline{a}b$ with $b =\overline{b}$.
855: Then $r = a\overline{a}$ and $s= b$. Let
856: $w = \overline{a}p^4ap^3 a$
857: Then the $p$-stable normal form of $w$ is:
858: $$
859: (\overline{a}ba\overline{a}b, 2, ba\overline{a}baa\overline{a}b,0,ba\overline{a}ba).$$
860: \end{example}
861:
862: In both cases
863: we can write the $p$-stable normal form of $w$
864: as a sequence $$( u_{0},\alpha _{1},u_{1},\ldots ,\alpha _{k},u_{k}) $$
865: where $u_i$ are words and $\alpha _{i}$ are integers.
866:
867: For every finite semigroup $S$ there is a number $c(S)$ such that for
868: all $s\in S$ the element $s^{c(S)}$ is idempotent, i.e., $s^{c(S)} =
869: s^{2c(S)}$. It is clear that the number $c(M)$ for our monoid $M
870: \subseteq \mathbb{B}^{2n\times 2n}$ is the same as the number
871: $c(\mathbb{B}^{n\times n})$. It is well-known \cite{mar77} that we
872: can take $c(\mathbb{B}^{n\times n}) = n!$
873: (it is however more convenient to define $c(M) = 3$ for
874: $n = 1$). Hence in the following
875: $c(M) = \max\{3,n!\}$.
876:
877: For specific situations this
878: might be an overestimation, but
879: this choice guarantees $h(uv^{c(M)}w) =
880: h(uv^{2c(M)}w)$ for all $u,v,w\in \Gamma^*$ and all $h:\Gamma^* \rightarrow M$.
881:
882: Now, let $w,w'\in\Gamma^*$ be words such that the $p$-stable normal
883: forms are identical up to one position where for $w$ appears an
884: integer $\alpha_i$ and for $w'$ appears an integer $\alpha_i'$.
885: We know $h(w) = h(w')$ whenever
886: the following conditions are satisfied: $\alpha_i \cdot
887: \alpha_i' > 0$, $|\alpha_i| \geq c(M)$, $|\alpha_i'| \geq c(M)$, and
888: $\alpha_i \equiv \alpha_i' \pmod {c(M)}$. Then we have $h(w) = h(w')$.
889: This is the reason to change the syntax of the $p$-stable normal form.
890: Each non-zero integer $\alpha'$ is written as $\alpha' = \varepsilon (q +
891: \alpha c(M))$ where $\varepsilon, q, \alpha$ are uniquely defined by
892: $\varepsilon \in \{ +1, -1 \}$, $0\leq q < c(M)$, and $\alpha \geq 0$.
893: For $\alpha'= 0 $ we may choose $\varepsilon = q = \alpha = 0$.
894: We shall read $\alpha$ as a variable ranging over
895: non-negative integers, but $\varepsilon$, $q$, and $c(M)$
896: are viewed as constants. In fact, if $|\alpha'| < c(M)$,
897: then we best view $\alpha$ also as a constant in order to avoid
898: problems with the constraints.
899:
900: Let $u$, $v$, and $w$ be words such that $uv= w$ holds.
901: Write these words in their $p$-stable normal
902: forms:
903: \[
904: \begin{array}{ll}
905: u \colon &(u_{0},\varepsilon_{1}(q_{1}+\alpha _{1}c(S)),
906: u_{1},\ldots ,\varepsilon_{k}(q_{k}+\alpha
907: _{k}c(S)),u_{k}), \\
908: v \colon &(v_{0},\varepsilon'_{1}(s_{1}+\beta _{1}c(S)),
909: v_{1},\ldots ,\varepsilon'_{\ell}(s_{\ell }+\beta
910: _{\ell }c(S)),v_{\ell }), \\
911: w \colon &(w_{0},\varepsilon''_{1}(t_{1}+\gamma _{1}c(S)),
912: w_{1},\ldots ,\varepsilon''_{m}(t_{m}+\gamma
913: _{m}c(S)),w_{m}).
914: \end{array}
915: \]
916:
917:
918: Since $uv = w$ there are many identities. For example, for $k,\ell \geq 2$
919: we have $u_{0}=w_{0}$, $v_{l}=w_{m}$, $%
920: q_{1}=t_{1}$, $\alpha _{1}=\gamma _{1}$, etc. What exactly happens
921: depends only on the $p$-stable normal form of the product
922: $u_{k}v_{0}$. There are several cases, which easily can be listed.
923: We treat only one of them, which is in some sense the worst case in
924: order to produce a large exponent of periodicity. This is the case
925: where $ p = rs$ with $r = \overline{r}$ and $s = \overline{s}$. Then
926: it might be that $u_k= srsr_1 $ and $v_0 = r_2srs$ with $r_1r_2 =
927: r$ (and $r_1 \not= 1 \not= r_2$).
928: Hence we have $u_{k}v_{0}=sp^{3}$ and $k+\ell =m+1$.
929: It follows $\alpha_1 = \gamma_1, \ldots, \alpha_{k-1} = \gamma_{k-1}$,
930: $\beta_2 = \gamma_{k+1}, \ldots, \beta_{\ell} = \gamma_{m}$,
931: and there is only one non-trivial identity:
932:
933: \[q_{k}+s_{1}+4 +(
934: \alpha _{k}+\beta _{1})c(S)=t_{k}+\gamma _{k}c(S).
935: \]
936: Since by assumption $c(S)\geq 3$, the case $u_{k}v_{0}=sp^{3}$
937: leads to the identity:
938: \[
939: \gamma _{k}= \alpha _{k}+\beta _{1}
940: + c\mbox{ with } c \in \{0,1,2\}.
941: \]
942:
943: Assume now that $\alpha _{k}\geq 1$ and $ \beta _{1}\geq 1$.
944: If we replace $\alpha _{k}$, $\beta _{1}$, and $\gamma _{k}$
945: by some $\alpha _{k}' \geq 1$, $\beta _{1}' \geq 1$, and $\gamma _{k}'
946: \geq 1$
947: such that still $\gamma'_{k}= \alpha'_{k}+\beta'_{1}
948: + c$, then we obtain new words $u'$, $v'$, and $w'$ with the same
949: images under $h$ in $M$ and still the identity $u'v'=w'$.
950:
951:
952:
953: What follows then is completely analogous to what has been done in
954: detail in \cite{kp96,gut2000stoc,hagenahdiss2000,die98lothaire}.
955: Using the $p$-stable normal form we can associate with an equation $L
956: = R$ of denotational length $d$ together with its solution $\sigma:
957: \Omega \rightarrow \Gamma^*$ some linear Diophantine system of
958: $d$ equations in at most
959: $3d$ variables. The variables range over natural numbers since zeros are
960: substituted. (In fact the
961: number of variables can be reduced to be at most
962: $2|\Omega|$). The parameters of this system are such that maximal
963: size of a minimal solution (with respect to the component wise partial
964: order of $\mathbb{N}^d$) is in $\OO(2^{1.6d})$ with the same approach
965: as in
966: \cite{kp96}. This tight bound is based in turn on the work of \cite{gs78}; a
967: more moderate bound $2^{\OO(d)}$ (which is enough for our purposes) is
968: easier to obtain, see e.g.\ \cite{die98lothaire}. The maximal size of
969: a minimal solution of the linear Diophantine system has a backward
970: translation to a bound on the exponent of periodicity. For this
971: translation we have to multiply with the factor $c(M) \in 2^{\OO(n\log
972: n)}$ and to add $c(M) +1$. Putting everything together we
973: obtain the claim of the proposition.
974: \qed
975: \end{proof}
976:
977:
978:
979: \section{Exponential Expressions}
980:
981: During the procedure which solves
982: Theorem~\ref{theo3} various other equations with constraints are considered
983: but the monoid $M$ will not change.
984:
985: There will be not enough space to write down the equation $L=R$ in
986: plain form, in general. In fact, there is a provable exponential lower
987: bound for the length $|LR|$ in the worst case which we can meet
988: during the procedure. In order to overcome this difficulty
989: Plandowski's method uses data compression for words in $(\Gamma \cup
990: \Omega)^*$ in terms of exponential expressions.
991:
992:
993: Exponential expressions (their evaluation and their size) are inductively
994: defined:
995: \begin{itemize}
996: \item Every word $w \in \Gamma^*$ denotes an exponential expression.
997: The evaluation $\eval(w)$ is equal to $w$, its size $\| w \|$ is
998: equal to the length $|w|$.
999: \item Let $e$, $e'$ be exponential expressions. Then $e e'$ is an
1000: exponential expression. Its evaluation is the concatenation
1001: $\eval(e e')=\eval(e) \eval(e')$, its size is
1002: $\| e e' \| = \| e \| + \| e' \|$.
1003: \item Let $e$ be an exponential expression and $k \in \N$. Then $(e)^k$
1004: is an exponential expression. Its evaluation is
1005: $\eval((e)^k) = (\eval(e))^k$, its size is
1006: $\| (e)^k \| = \log(k)+ \| e \|$ where $\log(k) = \max \{1, \lceil \log_2(k) \rceil\}$.
1007: \end{itemize}
1008: It is not difficult to show that the
1009: length of $\eval(e)$ is at most exponential in the size of $e$,
1010: a fact which is, strictly speaking, not needed for the proof of
1011: Theorem~\ref{theo3}. What we need however is
1012: the next lemma. Its proof can be done easily by structural
1013: induction and it is omitted.
1014:
1015: \begin{lemma} \label{expfac}
1016: Let $u \in \Gamma^*$ be a factor of a word $w\in \Gamma^*$. Assume
1017: that $w$ can be represented by some exponential expression of size $p$.
1018: Then we find an exponential expression of size at most $p^2$ that
1019: represents $u$.
1020: \end{lemma}
1021:
1022: We say that an exponential expression $e$ is {\em admissible\/}, if
1023: its size $\| e \| $ is bounded by some fixed polynomial in the input
1024: size of $E_0$. The lemma above states that if $e$ is admissible, then
1025: we find admissible exponential expressions for all factors of
1026: $\eval(e)$. But now the admissibility is defined with respect to some
1027: polynomial which is the square of the original polynomial, so, in a
1028: nested way, we can apply this procedure a constant number of times,
1029: only. In our application the nested depth does not go beyond two.
1030:
1031: The next lemma is straightforward
1032: since we allow a polynomial space bound without any
1033: time restriction. Again, the proof is left to the reader.
1034:
1035: \begin{lemma} \label{basiceval}
1036: The following two problems can be
1037: solved in $\PSPACE$.
1038: \smallbreak
1039: INPUT: Exponential expressions $e$ and $e'$.
1040:
1041: QUESTION: Do we have $\eval(e)=\eval(e')$?
1042:
1043: \smallbreak
1044: INPUT: A mapping
1045: $h: \Gamma \to M$ and an exponential expression $e$.
1046:
1047: OUTPUT: The matrix $h(\eval(e)) \in M$.
1048: \end{lemma}
1049:
1050: \begin{remark}
1051: \label{polyeval}%
1052: The computation
1053: above can actually be performed in polynomial
1054: time, but this is not evident for the first question, see \cite{ESA::Plandowski1994} for details.
1055: \end{remark}
1056:
1057: Henceforth we allow that the part $L=R$ of an equation with constraints
1058: may also be given by a pair of exponential expressions $(e_L, e_R)$ with
1059: $\eval(e_L)=L$ and $\eval(e_R)=R$.
1060: We say that $E = (\Gamma, h , \Omega, \rho ; e_L = e_R)$
1061: is {\em admissible\/}, if $e_L e_R$
1062: is admissible,
1063: $|\Gamma \setminus \Gamma_0|$ has polynomial size,
1064: $\Omega \subseteq \Omega_0$, and
1065: $h(a)=h_0(a)$ for $a \in \Gamma \cap \Gamma_0$.
1066:
1067: For two admissible equations with constraints
1068: $E = (\Gamma, h , \Omega, \rho ; e_L=e_R)$
1069: and $E'= (\Gamma, h , \Omega, \rho ; e'_L= e'_R)$
1070: we write $E \equiv E'$,
1071: if $\eval(e_L)=\eval(e'_L)$
1072: and $\eval(e_R)=\eval(e'_R)$
1073: as strings in $(\Gamma \cup \Omega)^*$. This means that they
1074: represent exactly the same equations.
1075:
1076:
1077: \section{Base Changes}
1078: In this section we fix a mapping $h: \Gamma \to M$ which respects
1079: the involution.
1080: Let $(\Gamma',\invol)$ be an alphabet with involution
1081: and let $\beta: \Gamma' \to \Gamma^*$ be some
1082: mapping $\beta$ such that
1083: $\beta(\overline{a}) = \overline{\beta(a)}$ for all $a \in \Gamma'$.
1084: We define $h' : \Gamma' \to M $ such that $h' = h \beta $.
1085: We also extend to a homomorphism
1086: $\beta: (\Gamma' \cup \Omega)^* \to (\Gamma \cup \Omega)^*$ by leaving
1087: the variables invariant.
1088:
1089: Let
1090: $E'=(\Gamma', h' , \Omega, \rho ; L'=R').$
1091: be an equation with constraints. The
1092: {\em base change\/} $\beta_*(E')$ is defined by
1093: $$\beta_*(E') = (\Gamma, h, \Omega, \rho ; \beta(L')=\beta(R')).$$
1094:
1095: We also refer to $\beta: \Gamma' \to \Gamma^*$ as a base change and we
1096: say that $\beta$ is {\em admissible\/}, if $|\Gamma'| $ has polynomial
1097: size and if $\beta(a)$ can be represented by some admissible
1098: exponential expression for all $a \in \Gamma'$.
1099:
1100: \begin{remark}
1101: \label{basepoly}%
1102: If $\beta: \Gamma' \to \Gamma^*$ is an admissible base change and if
1103: $L'=R'$ is given by a pair of admissible exponential expressions,
1104: then we can represent $\beta_*(E')$ by some admissible equation with
1105: constraints. A representation of $\beta_*(E')$ is computable in
1106: polynomial time.
1107: \end{remark}
1108:
1109: \begin{lemma} \label{basechange}
1110: Let $E'$ be an equation with constraints and
1111: $\beta: \Gamma' \to \Gamma^*$ be a base change. If
1112: $\sigma'$ is a solution of $E'$, then
1113: $\sigma=\beta \sigma'$ is a solution of $\beta_*(E')$.
1114: \end{lemma}
1115:
1116: \begin{proof}
1117: Clearly $\sigma(\overline{X})=\overline{\sigma(X)}$ and
1118: $h\sigma(X)=h\beta\sigma'(X)=h'\sigma'(X)=\rho(X)$ for all $X \in \Omega$.
1119: Next by definition $\sigma(a)=a$ for $a\in \Gamma$ and $\beta(X)=X$ for
1120: $X \in \Omega$. Hence $\sigma\beta(a)=\beta\sigma'(a)$ for $a \in \Gamma'$ and
1121: therefore $\sigma\beta=\beta\sigma': (\Gamma' \cup \Omega)^* \to \Gamma^*$.
1122: This means $\sigma\beta(L)=\beta\sigma'(L)=\beta\sigma'(R)=\sigma\beta(R)$ since
1123: $\sigma'(L)=\sigma'(R)$.\qed
1124: \end{proof}
1125:
1126: The lemma above leads to the first rule.\\
1127:
1128: {\bf Rule~1} {\em If $E$ is of the form $\beta_*(E')$
1129: and if we are looking for a solution of $E$, then
1130: it is enough to find a solution for $E'$. Hence, during
1131: a non-deterministic search
1132: we may replace
1133: $E$ by $E'$.\\}
1134:
1135:
1136: \begin{example}\label{ex-beta}
1137: Consider the following equation $E$ with constraints over
1138: $\Gamma = \{a,b,c, \oa, \ob, \oc \}$:
1139: \[
1140: X \ox
1141: = Y \ob \oc \ob \oa \ob \oc \ob Y Z a b c b \oy.
1142: \]
1143: Let there be the constraints for $X$ and $Z$ saying
1144: $X \in \Gamma^{300}\Gamma^*$ and $Z \in \ob \oc \ob \oa \Gamma^* $.
1145: Define $\Gamma' = \{a,b,\oa,\ob\}$ and a base change
1146: $\beta: \Gamma' \to \Gamma^*$
1147: by $\beta(a)=abcb$ and $\beta(b)=bcb$.
1148: Then the equation $E$ is of the form $\beta_*(E')$ where $E'$
1149: is given by
1150: \[
1151: X \ox = Y \oa \ob Y Z a \oy
1152: \]
1153: and the new (and sharper) constraint
1154: for $Z$ is simply $Z \in \oa{\Gamma'}^*$,
1155: for $X$ we may sharpen the constraint to
1156: $X \in {\Gamma'}^{100}{\Gamma'}^*$
1157: According to Rule~1 it is enough to solve $E'$.
1158: The effect of the base change
1159: $\beta$ is that the equation $E'$ is shorter and the
1160: alphabet of constants becomes smaller, since the letter $c$ is not
1161: used anymore. Note also that the length restriction
1162: on $X$ became smaller, too.
1163: However this has a prize; in general, $E=\beta_*({E'})$ might
1164: have a solution, whereas $E'$ is unsolvable. As we will see later,
1165: our guess has been correct in the sense that $E'$ still has a solution.
1166: \end{example}
1167:
1168:
1169: \section{Projections}
1170:
1171: Let $(\Gamma,\invol)$ and $(\Gamma',\invol)$ be alphabets with involution
1172: such that $(\Gamma,\invol) \subseteq (\Gamma',\invol)$. A
1173: {\em projection\/} is a homomorphism $\pi:{{\Gamma'}}^* \to
1174: \Gamma^*$ such that both $\pi(a) = a$ for $a\in\Gamma$ and
1175: $\pi(\overline{a}) = \overline{\pi(a)}$ for all $a\in{\Gamma'}$.
1176: If $h:\Gamma\to M$ is given, then a projection $\pi$
1177: defines also $h':{\Gamma'}\to M$ by $h' = h\pi$.
1178:
1179: Let $E$ be an equation with constraints
1180: $E = (\Gamma , h , \Omega, \rho; L=R).$
1181: Then we can define an equation with constraints $\pi^*(E)$ by
1182: $$\pi^*(E) = ({\Gamma'} , h\pi , \Omega , \rho ; L=R).$$
1183: The difference between $E$ and $\pi^*(E)$ is only in the
1184: alphabets of constants and in the mappings $h$ and $h' = h\pi$.
1185: Note that every projection $\pi: {\Gamma'}^*\to \Gamma^*$
1186: defines a base change $\pi_*$ such that $\pi_*\pi^*(E) = E$.
1187:
1188: \begin{lemma}
1189: \label{projchar}%
1190: Let $E= (\Gamma , h , \Omega , \rho ; L=R)$
1191: and $E' = ({\Gamma'} , h' , \Omega , \rho; L=R)$
1192: be equations with constraints.
1193: Then the following two statements hold.
1194: \begin{enumerate}
1195: \renewcommand{\labelenumi}{\roman{enumi})}
1196: \item There is a projection $\pi: {\Gamma'}^* \to \Gamma^*$ such that
1197: $\pi^*(E) = E'$, if and only if both $h'({\Gamma'}) \subseteq
1198: h(\Gamma^*)$ and for all $a\in{\Gamma'}$ with $a=\overline{a}$
1199: there is some $w \in \Gamma^*$ with $w = \overline{w}$
1200: such that $h'(a) = h(w)$.
1201: \item If we have $\pi^*(E) = E'$ and if $\sigma':\Omega \to
1202: {\Gamma'}^*$ is a solution of $E'$, then we effectively find a
1203: solution $\sigma$ for $E$ such that
1204: $|\sigma(L)| \leq 2|M||\sigma'(L)|$.
1205: \end{enumerate}
1206: \end{lemma}
1207:
1208: \begin{proof}
1209: i) Clearly, the only-if condition is satisfied by the definition of
1210: a projection since then $h' = h\pi$. For the converse, assume that
1211: $h'({\Gamma'}) \subseteq h(\Gamma^*)$ and that $a = \overline{a}$ implies
1212: $h'(a) \in h(\{ w\in\Gamma^* \mid w=\overline{w} \} )$. Then for
1213: each $a \in {\Gamma'}\setminus\Gamma$ we can choose a word
1214: $w_a\in\Gamma^*$ such that $h'(a) = h(w_a)$. We can make the choice
1215: such that $w_{\overline{a}} = \overline{w_a}$ for all $a \in
1216: {\Gamma'}\setminus\Gamma$. If $a\neq \overline{a}$, then we can find
1217: $w_a$ such that $|w_a| < |M|$, since we
1218: can take the shortest word $w_a\in \Gamma^*$ such that $h(w_a) = h'(a)
1219: \in M$. For $a=\overline{a}$ we know that there is some word
1220: $w_a\in\Gamma^*$ with $h'(a) = h(w_a)$ and $w_a=\overline{w_a}$. Hence we
1221: can write $w_a = vb\overline{v}$ with $b\in\Gamma\cup \{1\}$ and
1222: $b=\overline{b}$. For $b\neq 1$ we can demand $|w_a| \leq 2|M|-1$.
1223: For $b=1$ we can demand $|w_a| \leq 2|M|-2$. Thus, we find a projection
1224: $\pi:{\Gamma'}^* \to \Gamma^*$ such that $\pi^*(E) = E'$ and
1225: moreover, $|\pi(a)| < 2|M|$ for all $a\in{\Gamma'}$.
1226:
1227: ii) Using the reasoning in the proof of i) we may assume that
1228: $\pi:{\Gamma'}^* \to \Gamma^*$ satisfies $|\pi(a)| < 2|M|$
1229: for all $a\in{\Gamma'}$. Since $\pi$ defines a base change with
1230: $\pi_*(E') = E$, we know by Lemma~\ref{basechange}
1231: that $\sigma = \pi\sigma'$ is a solution of $E$.
1232: Clearly, $|\sigma(L)| = |\pi\sigma'(L)| \leq 2 |M| |\sigma'(L)|$. \qed
1233: \end{proof}
1234:
1235:
1236:
1237:
1238: \begin{remark}\label{decideproj}
1239: In the following we will meet the problem to decide whether there
1240: is a projection $\pi:{\Gamma'}^* \to \Gamma^*$ such that
1241: $\pi^*(E) = E'$. We actually need not too much space for this
1242: test.
1243: It is not necessary to write down $\pi$. We
1244: can use the criterion in the lemma above and Lemma~\ref{basicops}.
1245: Then we have to store
1246: in the working space only some Boolean matrices of $\B^{2n\times
1247: 2n}$. In particular, if $n$ is a constant (or logarithmically
1248: bounded in the input size), then the test $\exists\pi: \pi^*(E) = E'$ can be
1249: done in polynomial time. However, if $n$ becomes a substantial part
1250: of the input size, then the test might be difficult in the sense
1251: that we might need the full power of $\PSPACE$.
1252: \end{remark}
1253:
1254: The lemma above leads now to the second rule.\\
1255:
1256: {\bf Rule~2} {\em If $\pi$ is a projection
1257: and if we are looking for a solution of $E$, then
1258: it is enough to find a solution for $\pi^*(E)$. Hence, during
1259: a non-deterministic search
1260: we may replace
1261: $E$ by $\pi^*(E)$.\\}
1262:
1263:
1264: \begin{example}\label{ex-pi}
1265: Let us continue with the equation which has been obtained by the
1266: transformation in Example~\ref{ex-beta}.
1267: In order to simplify notations, we will call $E$ the equation
1268: % After renaming, the equation is called $E$ again
1269: % and we have $\Gamma = \{ a,b,\oa, \ob \}$. The equation $E$
1270: % is therefore:
1271: $ X \ox = Y \oa \ob Y Z a \oy$,
1272: and $\Gamma = \{ a,b,\oa, \ob \}$.
1273:
1274: Remember that the constraint
1275: on $X$ demanded a rather long
1276: solution. Therefore we may reintroduce a letter $c$
1277: and put $\Gamma' = \{a,b,c,\oa, \ob, \oc \}$. Then we may define
1278: a projection $\pi: \Gamma' \to \Gamma^*$ by, say,
1279: $\pi(c)=b^{100}$. The equation $E' = \pi^*(E)$ looks as above,
1280: but in $E'$ we may change the constraint for $X$. We may sharpen the new
1281: constraint for $X$ to be $X \in \Gamma^* c \Gamma^*$.
1282: Thus, the solution for $X$ might be very short now.
1283: \end{example}
1284:
1285:
1286: \section{Partial Solutions}
1287:
1288: Let $\Omega' \subseteq \Omega$ be a subset of the variables which is closed
1289: under involution. We assume that there is a mapping $\rho': \Omega'
1290: \to M$ with $\rho'(\overline{x}) = \overline{\rho'(x)}$, but
1291: we do not require that $\rho'$ is the restriction of $\rho: \Omega
1292: \to M$. Consider an equation with constraints
1293: $E = (\Gamma , h , \Omega,\rho; L=R).$
1294: A {\em partial solution} is a mapping $\delta:\Omega \to \Gamma^*
1295: \Omega' \Gamma^* \cup \Gamma^*$ such that the following conditions are
1296: satisfied:
1297: \begin{enumerate}
1298: \renewcommand{\labelenumi}{\roman{enumi})}
1299: \item \parbox{3cm}{$\delta(X) \in \Gamma^* X \Gamma^*$} for all
1300: $X\in\Omega'$,
1301: \item \parbox{3cm}{$\delta(X) \in \Gamma^*$} for all
1302: $X\in\Omega\setminus \Omega'$,
1303: \item \parbox{3cm}{$\delta(\overline{X}) = \overline{\delta(X)}$}
1304: for all $X\in\Omega$.
1305: \end{enumerate}
1306: The mapping $\delta$ is extended to a homomorphism $\delta:(\Gamma
1307: \cup \Omega)^* \to (\Gamma \cup \Omega')^*$ by leaving the
1308: elements of $\Gamma$ invariant. Let
1309: $ E' = (\Gamma , h , \Omega',\rho'; L'=R')$
1310: be another equation with constraints
1311: (using the same $\Gamma$ and $h$). We write $E'
1312: = \delta_*(E)$, if there exists some partial solution $\delta:\Omega
1313: \to \Gamma^* \Omega \Gamma^* \cup \Gamma^*$ such that the following
1314: conditions hold:
1315: $L' = \delta(L)$, $R' = \delta(R)$, $\rho(X) = h(u)\rho'(X)h(v)$ for
1316: $\delta(X) = uXv$, and $\rho(X) = h(w)$ for $\delta(X) =
1317: w\in\Gamma^*$.
1318:
1319: \begin{lemma}
1320: \label{shiftsol}%
1321: In the notation of above, let $E' = \delta_*(E)$ for some partial solution
1322: $\delta: \Omega \to \Gamma^* \Omega \Gamma^* \cup \Gamma^*$.
1323: If $\sigma'$ is a solution of $E'$,
1324: then $\sigma = \sigma'\delta $ is a
1325: solution of $E$. Moreover, we have $\sigma(L) = \sigma'(L')$
1326: and $\sigma(R) = \sigma'(R')$.
1327:
1328:
1329: \end{lemma}
1330:
1331: \begin{proof}
1332: By definition, $\delta$ and $\sigma'$ are extended to homomorphisms
1333: $\delta: (\Gamma\cup\Omega)^* \to (\Gamma\cup\Omega')^*$ and
1334: $\sigma': (\Gamma \cup \Omega')^* \to \Gamma^*$ leaving the
1335: letters of $\Gamma$ invariant. Since $E' = \delta_*(E)$ we have
1336: $\delta(L) = L'$ and $\delta(R) = R'$. Since $\sigma'$ is a
1337: solution, we have $\sigma(L) = \sigma'\delta(L) = \sigma'(L') =
1338: \sigma'(R') = \sigma'\delta(R) = \sigma(R)$ and $\sigma$ leaves the
1339: letters of $\Gamma$ invariant. The solution $\sigma'$ satisfies
1340: $h\sigma'(X) = \rho'(X)$ for all $X\in\Omega'$. Hence, if $\delta(X)
1341: = uXv$, then $\rho(X) = h(u)\rho'(X)h(v) = h(u\sigma'(X)v) =
1342: h\sigma'(uXv) = h\sigma'\delta(X) = h\sigma(X)$. If $\delta(X) =
1343: w\in\Gamma^*$, then $\sigma(X) = \sigma'\delta(X) = w$ and $\rho(X)
1344: = h(w)$, again by the definition of a partial solution.
1345: \qed
1346: \end{proof}
1347:
1348: \begin{lemma}
1349: \label{shifttest}%
1350: The following problem can be solved in $\PSPACE$.
1351: \smallbreak
1352: INPUT: Two equations with constraints
1353: $E = (\Gamma , h , \Omega,\rho; e_L = e_R)$
1354: and $E' = (\Gamma , h , \Omega', \rho'; e_{L'} = e_{R'})$.
1355:
1356: QUESTION: Is there some partial solution $\delta$
1357: such that $\delta_*(E) \equiv E'$?
1358:
1359: \smallbreak
1360: Moreover, if $\delta_*(E) \equiv E'$ is true, then there are
1361: admissible exponential expressions $e_u$, $e_v$ for each $X\in\Omega'$
1362: and an admissible exponential expression $e_w$ for each $X \in
1363: \Omega\setminus\Omega'$ such that
1364: $$\begin{array}{rcll}
1365: \delta(X) & = & \eval(e_u)X\eval(e_v) &\quad \mathrm{ for }\; X\in\Omega', \\
1366: \delta(X) & = & \eval(e_w) & \quad \mathrm{ for }\; X\in\Omega\setminus\Omega'.
1367: \end{array}
1368: $$
1369: \end{lemma}
1370:
1371: \begin{proof}
1372: Let $L = \eval(e_L)$, $R = \eval(e_R)$, $L' = \eval(e_{L'})$, and
1373: $R' = \eval(e_{R'})$. The non-deterministic algorithm works as follows:
1374:
1375: For each
1376: $X\in\Omega'$ we guess admissible exponential expressions $e_u$ and
1377: $e_v$ with $\eval(e_u),\eval(e_v) \in \Gamma^*$. We define an
1378: exponential expressions $e_X = e_uXe_v$ and $\delta(X) =
1379: \eval(e_X)$. For each $X \in \Omega\setminus\Omega'$ we guess an admissible
1380: exponential $e_X$ with $\eval(e_X) \in \Gamma^*$ and $\delta(X) =
1381: \eval(e_X)$.
1382:
1383: Next we verify whether or not $\delta_*(E) \equiv E'$.
1384: During this test we have to create an exponential expression $f_L$
1385: (and $f_R$, resp.) by replacing $X$ in $e_L$ (and $e_R$, resp.) with
1386: the expression $e_X$. This increases the size in the worst case
1387: by a factor of $\max \{ ||e_X|| \mid X\in\Omega \}$.
1388: The other tests whether
1389: $\rho(X) = h(u)\rho'(X)h(v)$ for $\delta(X) = uXv$ and $\rho(X) =
1390: h(w)$ for $\delta(X) = w\in\Gamma^*$ involve admissible exponential
1391: expressions over Boolean matrices and can be done in polynomial time.
1392:
1393: The correctness of the algorithm follows from our general assumption
1394: that all $X\in\Omega$ appear in $LR\overline{LR}$. Therefore, if we
1395: have $\delta_*(E) \equiv E'$, then $\delta(X)$ (or
1396: $\delta(\overline{X})$) appears necessarily as a factor in $L'R' = \delta(LR)$.
1397: Hence $\delta(X)$ has an
1398: exponential expression of polynomial size by Lemma~\ref{expfac}.
1399: Therefore guesses of $e_u$, $e_v$, and $e_w$ as above are possible
1400: without running out of space. \qed
1401: \end{proof}
1402:
1403: \begin{remark}\label{npeval}
1404: Actually, the test for
1405: $\delta_*(E) \equiv E'$ can be performed in non-deterministic
1406: polynomial time by Remark~\ref{polyeval}.
1407: \end{remark}
1408:
1409: The lemma above leads to the third and last rule.\\
1410:
1411: {\bf Rule~3} {\em If $\delta$ is a partial solution
1412: and if we are looking for a solution of $E$, then
1413: it is enough to find a solution for $\delta_*(E)$. Hence, during
1414: a non-deterministic search
1415: we may replace
1416: $E$ by $\delta_*(E)$.\\}
1417:
1418:
1419:
1420: \begin{remark}\label{projtest}
1421: We can think of a partial solution $\delta:\Omega \to \Gamma^*
1422: \Omega' \Gamma^* \cup \Gamma^*$ in the following sense. Assume we
1423: have an idea about $\sigma(X)$ for some $X\in\Omega$. Then we might
1424: guess $\sigma(X)$ entirely. In this case we can define $\delta(X) =
1425: \sigma(X)$ and we have $X\not\in\Omega'$. For some other $X$ we
1426: might guess only some prefix $u$ and some suffix $v$ of $\sigma(X)$.
1427: Then we define $\delta(X) = uXv$ and we have to guess some
1428: $\rho'(X)\in M$ such that $\rho(x): h(u)\rho'(X)h(v)$. If our guess
1429: was correct, then such a matrix $\rho'(X)\in M$ must exist. We have
1430: partially specified the solution and applying Rule~3, we continue
1431: this process by replacing the equation $L=R$ by the new equation
1432: $\delta(L) = \delta(R)$.
1433: \end{remark}
1434:
1435:
1436:
1437: \begin{example}\label{ex-delta}
1438: We continue with our running example.
1439: After renaming, the equation $E$ is given by
1440: \[
1441: X \ox = Y \oa \ob Y Z a \oy,
1442: \]
1443: and
1444: the alphabet of constant is given by $\Gamma = \{ a, b,c, \oa, \ob, \oc \}$.
1445: The constraints are $X\in \Gamma^* c \Gamma^*$
1446: and $Z \in \oa \{a,b,\oa, \ob \}^*$.
1447:
1448: We may guess the partial solution as follows:
1449: $\delta(X)=aX$, $\delta(Y)=Y$, and $\delta(Z)=\oa b$.
1450: The new equation $\delta_*(E)$ is
1451: \[
1452: a X \ox \oa = Y \oa \ob Y \oa b a \oy.
1453: \]
1454: The remaining constraint is that the solution for $X$ has to use
1455: the letter $c$.
1456:
1457:
1458: The process can continue, for example,
1459: we can apply Rule~1 again by defining
1460: another base change $\beta(b) = ba$ to get the equation
1461: \[
1462: a X \ox \oa = Y \ob Y \oa b \oy
1463: \]
1464: over $\Gamma = \{ a,b,c,\oa, \ob, \oc\}$.
1465: Since the last equation has a solution
1466: (e.g., given by $\sigma(X)=b c \oc \ob \ob a b c$ and
1467: $\sigma(Y)=a b c\oc \ob$),
1468: the first equation with constraints in Example~\ref{ex-beta}
1469: has a solution too.
1470: \end{example}
1471:
1472:
1473: \section{The Search Graph and Plandowski's Algorithm}
1474:
1475: In the following we show that there is some fixed polynomial
1476: (which can be calculated from the presentation below) such that
1477: the high-level description of Plandowski's algorithm is as follows:
1478: On input $E_0$ compute the maximal space bound, given by the polynomial,
1479: to be used by the procedure. Then apply non-deterministically
1480: Rules~1, 2, and 3 until an equation with a trivial solution is found.
1481:
1482: From the description above it follows that the
1483: specification of the algorithm just uses Rules~1, 2, 3.
1484: The algorithm is simple but it demands a good heuristics to
1485: explore the search graph.
1486: The hard part is to prove that this schema is correct;
1487: for this we have to be more precise.
1488:
1489: The {\em search graph} is a directed graph:
1490: The nodes are admissible equations with constraints.
1491: For two nodes $E$, $E'$, we define an arc $E \rightarrow E'$, if
1492: there are an admissible base change $\beta$, a
1493: projection $\pi$, and a partial solution $\delta$
1494: such that $\delta_*(\pi^*(E)) \equiv \beta_*(E')$.
1495:
1496: \begin{lemma} \label{searchgrapharc}
1497: The following problem can be decided in $\PSPACE$.
1498:
1499: INPUT: Admissible equations with constraints $E$ and $E'$.
1500:
1501: QUESTION: Is there an arc $E \rightarrow E'$ in the search graph?
1502: \end{lemma}
1503:
1504: \begin{proof}
1505: We first guess some alphabet
1506: $({\Gamma'}',\invol)$ of polynomial size
1507: together with $h'':{\Gamma'}' \to M$. Then we guess some
1508: admissible base change
1509: $\beta: {\Gamma'} \to {\Gamma''}^*$ such that $h'= h''\beta$
1510: and we compute $\beta_*(E')$.
1511:
1512: Next we guess some admissible equation with constraints $E''$
1513: which uses ${\Gamma''}$ and $\Omega$.
1514: We
1515: check using Lemma~\ref{shifttest} that there is
1516: some partial solution $\delta: \Omega \to
1517: {\Gamma''}^* \Omega' {\Gamma''}^* \cup {\Gamma''}^*$
1518: such that
1519: $\delta_*(E'') \equiv \beta_*(E')$.
1520: (Note that every
1521: equation with constraints $E''$
1522: satisfying $\delta_*(E'') \equiv \beta_*(E')$
1523: for some $\delta$ is admissible by Lemma~\ref{expfac}.)
1524: Finally we
1525: check using Remark~\ref{projtest}
1526: and that there is some projection
1527: $ \pi:{\Gamma''} \to \Gamma$
1528: such that $\pi^*(E) \equiv E''$.
1529: We obtain
1530: $\delta_*(\pi^*(E)) \equiv \beta_*(E')$.\qed
1531: \end{proof}
1532:
1533: \begin{remark}\label{arctest}
1534: Following Remarks~\ref{polyeval} and~\ref{npeval} the problem in
1535: Lemma~\ref{searchgrapharc} can be decided in non-deterministic
1536: polynomial time, if the monoid $M$ is not part of the input and
1537: viewed as a constant. If, as in our setting,
1538: $M$ is part of the input, then $\PSPACE$ is the best we can prove,
1539: because the test for the projection becomes difficult.
1540: \end{remark}
1541:
1542: Plandowski's algorithm works as follows:
1543:
1544: \medbreak\nobreak{
1545: {\bf begin}
1546:
1547: \atab$E:=E_0$
1548:
1549: \atab{\bf while} $\Omega \neq \emptyset$ {\bf do}
1550:
1551: \atab\atab Guess an admissible equation $E'$ with constraints
1552:
1553: \atab\atab Verify that $E \rightarrow E'$ is an arc in the search graph
1554:
1555: \atab\atab$E:=E'$
1556:
1557: \atab{\bf endwhile}
1558:
1559: \atab{\bf return} ``$\eval(e_L)=\eval(e_R)$''
1560:
1561: {\bf end}
1562: } \medbreak
1563:
1564: By Rules~1--3 (Lemmata~\ref{basechange}, \ref{projchar}~$ii)$, and \ref{shiftsol}),
1565: if $E \rightarrow E'$ is an arc
1566: in the search graph and $E'$ is solvable, then $E$ is solvable, too.
1567: Thus, if the algorithm returns {\em true\/}, then $E_0$ is
1568: solvable. The proof of Theorem~\ref{theo3}
1569: is therefore reduced to the statement that if $E_0$
1570: is solvable, then the search graph contains a path to some
1571: node without variables and the exponential expressions defining
1572: the equation evaluate to the same word. This existence proof
1573: is the hard part, it
1574: covers the rest of the paper.
1575:
1576: \begin{remark}
1577: \label{doublesize}%
1578: If $E \rightarrow E'$ is due to some $\pi: {\Gamma''}^* \to
1579: \Gamma^*$,
1580: $\delta: \Omega \to
1581: {\Gamma''}^* \Omega' {\Gamma''}^* \cup {\Gamma''}^*$,
1582: and
1583: $\beta: {\Gamma'}^* \to {\Gamma''}^*$, then a solution
1584: $\sigma': \Omega' \to {\Gamma'}^*$ of $E'$ yields the solution
1585: $\sigma = \pi(\beta\sigma')\delta$. Hence we may assume that
1586: the length of a solution has
1587: increased by at most an exponential factor by Lemma~\ref{projchar} $ii)$. Since we are going
1588: to perform the search in a graph of at most exponential size,
1589: we get automatically a doubly exponential upper bound for the length
1590: of a minimal solution by backwards computation on such a path.
1591: This is still the best known upper
1592: bound (although an singly exponential bound is conjectured), see
1593: \cite{pla99stoc}.
1594: \end{remark}
1595:
1596:
1597:
1598:
1599: \section{Free Intervals}
1600:
1601: In this section we introduce the notion of {\em free interval} in order
1602: to cope with long factors in the solution which are not related to
1603: any cut. If there were no constraints, then these factors would not appear
1604: in a minimal solution. In our setting we cannot avoid these factors.
1605:
1606: For a word $w \in \Gamma^*$ we let $\{0, \ldots, |w|\}$ be the set of its
1607: {\em positions\/}. The interpretation is that factors of $w$ are between
1608: positions. To be more specific let $w=a_1 \cdots a_m$,
1609: $a_i \in \Gamma$ for $1 \leq i \leq m$. Then $[\alpha, \beta]$ with
1610: $0 \leq \alpha < \beta \leq m$ is called a \emph{positive interval}
1611: and the factor $w[\alpha,\beta]$ is defined by the word
1612: $w[\alpha,\beta]= a_{\alpha+1} \cdots a_\beta$.
1613:
1614:
1615: It is convenient to have an involution on the set of intervals. Therefore
1616: $[\beta, \alpha]$ is also called an interval (but it is never
1617: positive),
1618: and we define
1619: $w[\beta,\alpha]=\overline{w[\alpha,\beta]}$.
1620: We allow also $\alpha = \beta$ and we define $w[\alpha,\alpha]$
1621: to be the empty word.
1622: For all $0 \leq \alpha, \beta \leq m$ we let
1623: $\overline{[\alpha,\beta]}=[\beta,\alpha]$, then always
1624: $\overline{w[\alpha,\beta]}=w \overline{[\alpha,\beta]}$.
1625:
1626: Let us focus on the word $w_0 \in \Gamma_0^*$ which in our notation is the
1627: solution $w_0 = \sigma(L_0) = \sigma(R_0)$, where
1628: $L_0 = x_1 \cdots x_g$ and $R_0 = x_{g+1} \cdots x_d$,
1629: $x_i \in (\Gamma_0 \cup \Omega_0)$ for $1 \leq i \leq d$. We are going to
1630: define an equivalence relation $\approx$ on the set of intervals of $w_0$.
1631: For this we have to fix some few more notations. We let $m_0 = |w_0|$ and
1632: for $i \in \{1, \ldots, d\}$ we define positions
1633: $\leftp(i) \in \{0, \ldots, m_0-1\}$ and $\rightp(i) \in \{1, \ldots, m_0\}$
1634: by the congruences
1635: \begin{eqnarray*}
1636: \leftp(i) & \equiv & |\sigma(x_1 \cdots x_{i-1})| \mod m_0, \\
1637: \rightp(i) & \equiv & |\sigma(x_{i+1} \cdots x_d)| \mod m_0.
1638: \end{eqnarray*}
1639: This means, the factor $\sigma(x_i)$ starts in $w_0$ at the left position
1640: $\leftp(i)$ and it ends at the right position $\rightp(i)$.
1641: In particular, we have $\leftp(1) = \leftp(g+1) = 0$ and $\rightp(g) =
1642: \rightp(d) =m_0$. The set of $\leftp$ and $\rightp$ positions is
1643: called the set of {\em cuts\/}. Thus, the set of cuts is $\{\,
1644: \leftp(i), \rightp(i) \mid 1 \leq i \leq d \,\}$. There are at most
1645: $d$ cuts. These positions cut the word $w_0$ in at most $d-1$ factors.
1646: For convenience we henceforth assume $2 \leq g < d < m_0$ whenever
1647: necessary. We make also the assumption that $\sigma(x_i) \neq 1$ for
1648: all $1 \leq i \leq d$. This assumption can be realized e.g. by a first
1649: step in Plandowski's algorithm using a partial solution $\delta$ which sends a
1650: variable $X$ to the empty word, if $\sigma(X) =1$ and sends $X$ to
1651: itself otherwise. Another choice to realize this assumption is by a
1652: guess in some preprocessing.
1653:
1654: We have $\sigma(x_i) = w_0[\leftp(i), \rightp(i)]$ and
1655: $\sigma(\overline{x_i}) = w_0[\rightp(i), \leftp(i)]$ for $1 \leq i
1656: \leq d$.
1657: By our assumption, the interval $ [\leftp(i), \rightp(i)]$
1658: is positive.
1659: Let us consider a pair $(i, j)$ such that $i,j \in {1, \ldots, d}$ and
1660: $x_i = x_j$ or $x_i = \overline{x_j}$. For
1661: $\mu, \nu \in \{0, \ldots, \rightp(i)-\leftp(i)\}$ we define a relation
1662: $\sim$ by:
1663:
1664: \begin{eqnarray*}
1665: {[}\leftp(i)+\mu, \leftp(i)+\nu{]} & \sim &
1666: {[}\leftp(j)+\mu, \leftp(j)+\nu{]}, \mathrm{\,if\,} x_i = x_j, \\
1667: {[}\leftp(i)+\mu, \leftp(i)+\nu{]} & \sim &
1668: {[}\rightp(j)-\mu, \rightp(j)-\nu {]}, \mathrm{\,if\,} x_i = \overline{x_j}.
1669: \end{eqnarray*}
1670: Note that $\sim$ is a symmetric relation. Moreover,
1671: $[\alpha, \beta] \sim [\alpha', \beta']$ implies both
1672: $[\beta, \alpha] \sim [\beta', \alpha']$ and
1673: $w_0[\alpha, \beta] = w_0[\alpha', \beta']$. By $\approx$ we denote the
1674: reflexive and transitive closure of $\sim$. Then $\approx$ is an equivalence
1675: relation and again,
1676: $[\alpha, \beta] \approx [\alpha', \beta']$ implies both
1677: $[\beta, \alpha] \approx [\beta', \alpha']$ and
1678: $w_0[\alpha, \beta] = w_0[\alpha', \beta']$.
1679:
1680: Next we define the notion of {\em free interval\/}. An interval
1681: $[\alpha, \beta]$ is called {\em free\/}, if whenever
1682: $[\alpha, \beta] \approx [\alpha', \beta']$, then there is no cut
1683: $\gamma'$ with
1684: $\min\{\alpha', \beta'\} < \gamma' < \max\{\alpha', \beta'\}$. Clearly, the
1685: set of free intervals is closed under involution, i.e., if
1686: $[\alpha, \beta]$ is free, then $[\beta, \alpha]$ is free, too. It is also
1687: clear that $[\alpha, \beta]$ is free whenever $|\beta-\alpha| \leq 1$.
1688:
1689: \begin{example}\label{ex-free}
1690: The last equation in Example~\ref{ex-delta}, namely
1691: \[
1692: a X \ox \oa = Y \ob Y \oa b \oy,
1693: \]
1694: has a solution which yields the word
1695: \[
1696: w_0 =\; \stackrel{0}{|} a \stackrel{1}{|} b c \oc \ob \stackrel{5}{|}
1697: \ob \stackrel{6}{|} a b c \stackrel{9}{|}
1698: \oc \ob \stackrel{11}{|} \oa \stackrel{12}{|} b
1699: \stackrel{13}{|} b c \oc \ob \stackrel{17}{|} \oa \stackrel{18}{|} .
1700: \]
1701: The set of cuts is shown by the bars.
1702: The intervals $[1,5]$, $[13,17]$, and $[6,9]$ are not free,
1703: since $[1,5] \approx [17,13] \approx [7,11]$
1704: and $[6,9] \approx [0,3]$ and $[7,11]$, $[0,3]$
1705: contain cuts.
1706: There is only one equivalence class
1707: of free intervals of length
1708: longer than 1 (up to involution), which is given by
1709: $[1,3] \sim [17,15] \sim [7,9] \sim [11,9] \sim [5, 3] \sim [13,15]$.
1710: \end{example}
1711:
1712: The next lemma says that subintervals of free intervals
1713: are free again.
1714:
1715: \begin{lemma} \label{freesub}
1716: Let $[\alpha, \beta]$ be a free interval and
1717: $\mu, \nu$ such that
1718: $\min\{\alpha,\beta\} \leq \mu,\nu \leq \max\{\alpha,\beta\}$.
1719: %$\mu, \nu \in \{\min\{\alpha,\beta\}, \ldots, \max\{\alpha,\beta\}\}$.
1720: Then the interval $[\mu, \nu]$ is also free.
1721: \end{lemma}
1722:
1723: \begin{proof}
1724: We may assume that $\alpha \leq \mu < \nu \leq \beta$. By
1725: contradiction assume that $[\mu, \nu]$ is not free. Then there is some
1726: $k \geq 0$ and some cut $\gamma'$ such that
1727: $$[\mu,\nu]=[\mu_0,\nu_0] \sim [\mu_1, \nu_1] \sim \cdots \sim [\mu_k, \nu_k]$$
1728: with $\min\{\mu_k,\nu_k\} < \gamma' < \max\{\mu_k,\nu_k\}$. If $k=0$, then
1729: we have a immediate contradiction. For $k \geq 1$ the relation
1730: $[\mu,\nu] \sim [\mu_1,\nu_1]$ is due to some pair $x_i$, $x_j$ with
1731: $x_i = x_j$ or $x_i = \overline{x_j}$. Since $[\alpha, \beta]$ contains
1732: no cut, we can use the same pair to find an interval $[\alpha_1, \beta_1]$
1733: such that $[\alpha, \beta] \sim [\alpha_1, \beta_1]$ and
1734: $\mu_1, \nu_1 \in \{ \min\{\alpha_1,\beta_1\}, \ldots,
1735: \max\{\alpha_1,\beta_1\}\}$. Using induction on $k$ we see that
1736: $[\alpha_1, \beta_1]$ cannot be free. A contradiction,
1737: because then $[\alpha, \beta]$ is not free.\qed
1738: \end{proof}
1739:
1740: Next we introduce the notion of {\em implicit cut\/} for non-free
1741: intervals. For our purpose it is enough to define it for positive intervals.
1742: So, let $0 \leq \alpha < \beta \leq m_0$ such that $[\alpha, \beta]$ is not
1743: free. A position $\gamma$ with $\alpha < \gamma < \beta$ is called an
1744: {\em implicit cut\/} of $[\alpha, \beta]$, if we meet the following
1745: situation. There is a cut $\gamma'$ and an interval $[\alpha', \beta']$ such
1746: that
1747: \begin{eqnarray*}
1748: \min\{\alpha', \beta'\} \, < & \gamma' & < \, \max\{\alpha', \beta'\}, \\
1749: {[}\alpha, \beta {]} & \approx & {[}\alpha', \beta'{]}, \\
1750: \gamma-\alpha & = & |\gamma' - \alpha'|.
1751: \end{eqnarray*}
1752: The following observation will be used throughout. If we have
1753: $\alpha \leq \mu < \gamma < \nu \leq \beta$ and $\gamma$ is an implicit cut of
1754: $[\alpha, \beta]$, then $\gamma$ is also an implicit cut of $[\mu, \nu]$.
1755: In particular, neither $[\mu, \nu]$ nor $[\nu, \mu]$ is a free
1756: interval.\footnote{However,
1757: if $\gamma$ is an implicit cut of $[\mu,\nu]$, then it might happen
1758: that $\gamma$ is no implicit cut of $[\alpha, \beta]$, although
1759: $[\alpha, \beta]$ is certainly not free.}
1760:
1761: \begin{lemma} \label{mfo}
1762: Let $0 \leq \alpha \leq \alpha' < \beta \leq \beta' \leq m_0$ such that
1763: $[\alpha, \beta]$ and $[\alpha', \beta']$ are free intervals. Then the
1764: interval $[\alpha, \beta']$ is free, too.
1765: \end{lemma}
1766:
1767: \begin{proof}
1768: Assume by contradiction that $[\alpha, \beta']$ is not free. Then it contains
1769: an implicit cut $\gamma$ with $\alpha < \gamma < \beta'$. By the observation
1770: above: If $\gamma < \beta$, then $\gamma$ is an implicit cut of $[\alpha,
1771: \beta]$ and $[\alpha, \beta]$ is not free. Otherwise, $\alpha' < \gamma$ and
1772: $\alpha', \beta'$ is not free. \qed
1773: \end{proof}
1774:
1775: We now consider the maximal elements. A
1776: free interval $[\alpha, \beta]$ is called {\em maximal free\/}, if there is
1777: no free interval $[\alpha', \beta']$ such that both
1778: $\alpha' \leq \min\{\alpha, \beta\} \leq \max \{\alpha, \beta\} \leq \beta'$
1779: and $\beta'-\alpha' > |\beta-\alpha|$. With this notion Lemma~\ref{mfo}
1780: states that maximal free intervals do not overlap.
1781:
1782: \begin{lemma} \label{freecut}
1783: Let $[\alpha, \beta]$ be a maximal free interval. Then there are intervals
1784: $[\gamma, \delta]$ and $[\gamma', \delta']$ such that
1785: $[\alpha, \beta] \approx [\gamma, \delta] \approx [\gamma', \delta']$ and
1786: $\gamma$ and $\delta'$ are cuts.
1787: \end{lemma}
1788:
1789: \begin{proof}
1790: We may assume that $[\alpha, \beta]$ is a positive interval, i.e.,
1791: $\alpha < \beta$. We show the existence of $[\gamma, \delta]$ where
1792: $[\alpha, \beta] \approx [\gamma, \delta]$ and $\gamma$ is a cut. The
1793: existence of $[\gamma', \delta']$ where
1794: $[\alpha, \beta] \approx [\gamma', \delta']$ and $\delta'$ is a cut follows
1795: by a symmetric argument.
1796:
1797: If $\alpha=0$, then $\alpha$ itself is a cut and we can choose
1798: $\delta=\beta$. Hence let $1 \leq \alpha$ and consider the positive interval
1799: $[\alpha-1,\beta]$. This interval is not free, but the only possible
1800: position for an implicit cut is $\alpha$. Thus for some cut $\gamma$ we have
1801: $[\alpha-1, \beta] \approx [\alpha', \beta']$ with $\min \{\alpha',
1802: \beta'\} < \gamma < \max\{\alpha', \beta'\}$ and $|\gamma-\alpha'|=1$. A
1803: simple reflection shows that we have
1804: $[\alpha-1, \alpha] \approx [\alpha',\gamma]$ and
1805: $[\alpha, \beta] \approx [\gamma, \beta']$. Hence we can choose
1806: $\delta=\beta'$. \qed
1807: \end{proof}
1808:
1809: \begin{proposition} \label{nfi}
1810: Let $\Gamma$ be the set of words $w \in \Gamma_0^*$ such that there is a
1811: maximal free interval $[\alpha,\beta]$ with $w=w_0[\alpha,\beta]$. Then
1812: $\Gamma$ is a subset of $\Gamma_0^+$ of size at most $2d-2$. The set
1813: $\Gamma$ is closed under involution.
1814: \end{proposition}
1815:
1816: \begin{proof}
1817: Let $[\alpha,\beta]$ be maximal free. Then $|\beta-\alpha| \geq 1$ and
1818: $[\beta, \alpha]$ is maximal free, too. Hence $\Gamma \subseteq \Gamma_0^+$
1819: and $\Gamma$ is closed under involution. By Lemma~\ref{freecut} we may
1820: assume that $\alpha$ is a cut. Say $\alpha<\beta$. Then $\alpha \neq m_0$
1821: and there is no other maximal free interval $[\alpha, \beta']$ with
1822: $\alpha<\beta'$ because of Lemma~\ref{mfo}. Hence there are at most $d-1$
1823: such intervals $[\alpha, \beta]$. Symmetrically, there are at most $d-1$
1824: maximal free intervals $[\alpha, \beta]$ where $\beta<\alpha$ and $\alpha$
1825: is a cut.\qed
1826: \end{proof}
1827:
1828: For a moment let $\Gamma_0'=\Gamma_0 \cup \Gamma$ where
1829: $\Gamma \subseteq \Gamma_0^+$ is the set defined in Proposition~\ref{nfi}.
1830: The inclusion $\Gamma_0' \subseteq \Gamma_0^+$ defines a natural
1831: projection $\pi: \Gamma_0' \to \Gamma_0^*$ and a mapping
1832: $h_0': \Gamma_0' \to M$ by $h_0'=h_0 \pi$.
1833: Consider the equation with constraints $\pi^*(E)$, this
1834: is a node in the search graph, because
1835: the size of $\Gamma$ is linear in $d$.
1836:
1837: The reason to switch from $\Gamma_0$ to $\Gamma_0'$ is that, due to the
1838: constraints, the word $w_0$ may have long free intervals, even in a
1839: minimal solution.
1840: Over $\Gamma_0'$ long free intervals can be avoided.
1841: Formally, we replace $w_0$ by a solution $w_0'$ where
1842: $w_0' \in \Gamma^*$. The definition of $w_0'$ is based on a factorization
1843: of $w_0$ in maximal free intervals. There is a unique sequence
1844: $0=\alpha_0<\alpha_1<\cdots<\alpha_k=m_0$ such that
1845: $[\alpha_{i-1},\alpha_i]$ is a maximal free interval for
1846: each $1 \leq i \leq k$
1847: and
1848: $$w_0=w_0[\alpha_0,\alpha_i] \cdots w_0[\alpha_{k-1},\alpha_k].$$
1849: Note
1850: that all cuts occur as some $\alpha_p$, therefore we can think of the
1851: factors $w_0[\alpha_{i-1},\alpha_i]$ as letters in $\Gamma$ for $1
1852: \leq i \leq k$. Moreover, all constants which appear in $L_0R_0$ are
1853: elements of $\Gamma$.
1854: We replace $w_0$ by the word $w_0' \in \Gamma^*$.
1855: Then we can define $\sigma: \Omega \to \Gamma^*$ such that both
1856: $\sigma(L_0)=\sigma(R_0)=w_0'$ and $\rho_0 = h_0'\sigma$. In other
1857: terms, $\sigma$ is a solution of $\pi^*(E_0)$. We have $w_0=\pi(w_0')$
1858: and $\pexp(w_0') \leq \pexp(w_0)$. The crucial point is that $w_0'$
1859: has no long free intervals anymore. With respect to $w_0'$ and
1860: $\Gamma_0'$ all maximal free intervals have length exactly one.
1861:
1862: In the next step we show that
1863: we can reduce the alphabet of constants to be $\Gamma$.
1864: The inclusion of $\Gamma$ in ${\Gamma'}_0 $
1865: defines an
1866: admissible base change $\beta: \Gamma \to {\Gamma'}_0 $.
1867: Consider
1868: $E_0' = (\Gamma , h , \Omega_0 , \rho_0 ; L_0=R_0)$
1869: where $h$ is the restriction of the mapping $h_0'$.
1870: Then we have $\pi^*(E_0) = \beta_*(E_0')$.
1871: The search graph contains an arc from $E_0$ to $E_0'$,
1872: since we may choose $\delta$ to be the identity.
1873: The equation with constraints $E_0'$ has a solution
1874: $\sigma$ with $\sigma(L_0)= w_0'$
1875: and $\pexp(w_0') \leq \pexp(w_0)$.
1876:
1877: In order to avoid too many notations we identify $E_0$ and $E_0'$,
1878: hence we also assume $w_0=w_0'$.
1879: However, as a reminder that we have changed
1880: the alphabet of constants (recall that some words became letters),
1881: we prefer to use the notation $\Gamma $ rather than
1882: $\Gamma_0$.
1883: Thus, in what follows we shall make the following assumptions:
1884: \begin{eqnarray*}
1885: E_0 & = & (\Gamma , h , \Omega_0 , \rho_0 ; L_0=R_0),\\
1886: L_0 & = & x_1 \cdots x_g \mbox{ and } g \geq 2, \\
1887: R_0 & = & x_{g+1} \cdots x_d \mbox{ and } d>g, \\
1888: |\Gamma| & \leq & 2d-2, \\
1889: |\Omega_0 | & \leq & 2d, \\
1890: M & \subseteq & \B^{2n \times 2n}.
1891: \end{eqnarray*}
1892:
1893:
1894: Moreover: All variables $X$ occur in $L_0R_0 \overline{L_0R_0}$.
1895: There is a solution $\sigma$ such that
1896: $w_0=\sigma(L_0)=\sigma(R_0)$ with $\sigma(X_i) \neq 1$ for
1897: $1 \leq i \leq d$ and $\rho_0 = h\sigma =h_0\sigma$. We have $|w_0|=m_0$
1898: and $\pexp(w_0) \in 2^{\OO(d+n\log n)}$. All maximal free intervals have length
1899: exactly one, i.e., every positive interval $[\alpha, \beta]$ with
1900: $\beta-\alpha>1$ contains an implicit cut.
1901:
1902: It is because of the last sentence that we have worked out
1903: the details about free intervals.
1904: This difficulty is due to the constraints. Without them
1905: the reasoning would have been much simpler.
1906: But the good news are that from now on, the presence of
1907: constraints will not interfere very much.
1908:
1909:
1910: \begin{example}\label{ex-d}
1911: Following Example~\ref{ex-free}, we use the same equation
1912: $ a X \ox \oa = Y \ob Y \oa b \oy$ and we consider the solution $w_0$.
1913:
1914: The new solution is defined by replacing in $w_0$ each factor
1915: $bc$ by a new letter $d$ which represents a maximal free interval.
1916: The new $w_0$ has the form
1917: \[
1918: w_0 =\; \stackrel{0}{|} a \stackrel{1}{|} d \od \stackrel{3}{|}
1919: \ob \stackrel{4}{|} a d \stackrel{6}{|}
1920: \od \stackrel{7}{|} \oa \stackrel{8}{|} b
1921: \stackrel{9}{|} d \od \stackrel{11}{|} \oa \stackrel{12}{|}.
1922: \]
1923: Now all maximal intervals have length one.
1924: \end{example}
1925:
1926:
1927: \section{Critical Words and Blocks}
1928:
1929: In the following $\ell$ denotes an integer which varies between $1$ and
1930: $m_0$. For each $\ell$ we define the set of critical words $C_\ell$ by
1931: $$C_\ell = \{\,w_0[\gamma-\ell,\gamma+\ell], w_0[\gamma+\ell,\gamma-\ell] \mid
1932: \gamma {\rm\,is\,a\,cut\,and\,} \ell \leq \gamma \leq m_0 - \ell\,\}.$$
1933: We have $1 \leq |C_\ell| \leq 2d-4$ and $C_\ell$ is closed under involution.
1934: Each word $u \in C_\ell$ has length $2\ell$, it can be written in the form
1935: $u=u_1 u_2$ with $|u_1|=|u_2|=\ell$.
1936: Then $u_1$ (resp. $\overline{u_2}$) appears as a suffix,
1937: left of some cut and $u_2$ (resp. $\overline{u_1}$) appears as a prefix,
1938: right of the same cut.
1939:
1940: A triple $(u,w,v) \in (\{1\} \cup \Gamma^\ell) \times \Gamma^+ \times
1941: (\{1\} \cup \Gamma^\ell)$
1942: is called a {\em block\/} if first, up to a possible prefix or suffix
1943: no other factor of the word $uwv$ is a critical word, second, $u \neq
1944: 1$
1945: if and only if
1946: a prefix of $uwv$ of length $2\ell$ belongs to $C_\ell$, and third,
1947: $v \neq 1$ if and only if a suffix of $uwv$ of length $2\ell$ belongs to $C_\ell$.
1948: The set of blocks is denoted by $B_\ell$. It is viewed (as a possibly
1949: infinite) alphabet where the involution is defined by
1950: $\overline{(u,w,v)}=(\overline{v}, \overline{w}, \overline{u})$. We can
1951: define a homomorphism $\pi_\ell: B_\ell^* \to \Gamma^*$ by
1952: $\pi_\ell(u,w,v)=w \in \Gamma^+$ being extended
1953: to a projection $\pi_\ell: (B_\ell \cup \Gamma)^* \to
1954: \Gamma^*$
1955: by leaving $\Gamma$ invariant. We define $h_\ell:(B_\ell \cup \Gamma) \to M$
1956: by $h_\ell = h \pi_\ell$. In the following we shall consider finite subsets
1957: $\Gamma_\ell \subseteq B_\ell \cup \Gamma$ which are closed under involution. Then by
1958: $\pi_\ell: \Gamma_\ell^* \to \Gamma^*$ and $h_\ell: \Gamma_\ell^* \to M$
1959: we understand the restrictions of the respective homomorphisms.
1960:
1961: For every non-empty word $w \in \Gamma^+$ we define its
1962: {\em $\ell$-factorization\/} as follows. We write
1963: $$F_\ell(w) = \Fl 1k \in B_\ell^+$$
1964: such that $w=w_1 \cdots w_k$ and for $1 \leq i \leq k$ the following
1965: conditions are satisfied:
1966: \begin{itemize}
1967: \item $v_i$ is a prefix of $w_{i+1} \cdots w_k$,
1968: \item $v_i=1$ if and only if $i=k$,
1969: \item $u_i$ is a suffix of $w_1 \cdots w_{i-1}$,
1970: \item $u_i=1$ if and only if $i=1$.
1971: \end{itemize}
1972: Note that the $\ell$-factorization of a word $w$ is unique. For
1973: $k\geq2$ we
1974: have $|w_1|\geq \ell$ and $|w_k| \geq \ell$, but all other $w_i$ may
1975: be short. If no critical word appears as a factor of $w$, then
1976: $F_\ell(w) = (1,w,1)$. In particular, this is the case for
1977: $|w|<2\ell$. If we have $w=puvq$ with $|u|=|v|=\ell$ and $uv \in
1978: C_\ell$, then there is a unique $i \in \{1, \ldots, k-1\}$ such that
1979: $u=u_{i+1}$, $v=v_i$, and $pu=w_1 \cdots w_i$, $vq= w_{i+1} \cdots
1980: w_k$. Thus, $F_\ell(w)$ contains a factor $(u_i, w_i, v) (u, w_{i+1},
1981: v_{i+1})$ where $v$ is a prefix of $w_{i+1}v_{i+1}$ and $u$ is a
1982: suffix of $u_iw_i$. For example, the $\ell$-factorization of $uv \in
1983: C_\ell$ with $|u|=|v|=\ell$ is
1984: $$F_\ell(uv)=(1,u,v)(u,v,1).$$
1985:
1986: We define the $\head$, $\body$, and $\tail$ of a word $w$ based on its
1987: $\ell$-factorization
1988: $$F_\ell(w)= \Fl 1k$$
1989: in $B_\ell^*$ and $\Gamma^*$ as follows:
1990: \begin{eqnarray*}
1991: \Head_\ell(w) & = & \uwv 1 \in B_\ell, \\
1992: \head_\ell(w) & = & w_1 \in \Gamma^+, \\
1993: \Body_\ell(w) & = & \Fl 2{k-1} \in B_\ell^*, \\
1994: \body_\ell(w) & = & w_2 \cdots w_{k-1} \in \Gamma^*, \\
1995: \Tail_\ell(w) & = & \uwv k \in B_\ell, \\
1996: \tail_\ell(w) & = & w_k \in \Gamma^+.
1997: \end{eqnarray*}
1998: For $k \geq 2$ (in particular, if $\body_\ell(w) \neq 1$) we have
1999: \begin{eqnarray*}
2000: F_\ell(w) & = & \Head_\ell(w) \Body_\ell(w) \Tail_\ell(w),\\
2001: w & = & \head_\ell(w) \body_\ell(w) \tail_\ell(w).
2002: \end{eqnarray*}
2003: Moreover, $u_2$ is a
2004: suffix of $w_1$ and $v_{k-1}$ is a prefix of $w_k$.
2005:
2006: Assume $\body_\ell(w) \neq 1$ and let $u,v\in \Gamma^*$ be any words.
2007: Then we can view $w$ in the context $uwv$ and $\Body_\ell(w)$ appears
2008: as a proper factor in the $\ell$-factorization of $uwv$. More
2009: precisely, let
2010: $$F_\ell(uwv) = \Fl 1k.$$
2011: Then there are unique $1 \leq p <q \leq k$ such that:
2012: \begin{eqnarray*}
2013: F_\ell(uwv) & = & \Fl 1p \Body_\ell(w) \Fl qk,\\
2014: w_1 \cdots w_p & = & u \, \head_\ell(w), \\
2015: w_q \cdots w_k & = & \tail_\ell(w) v
2016: \end{eqnarray*}
2017: Finally, we note that the above definitions are compatible with the
2018: involution. We have $ F_\ell(\overline{w}) = \overline{F_\ell(w)}$, $
2019: \Head_\ell(\overline{w}) = \overline{\Tail_\ell(w)}$, and
2020: $\Body_\ell(\overline{w}) = \overline{\Body_\ell(w)}$.
2021:
2022:
2023: \section{The $\ell$-Transformation}
2024:
2025: Our equation with constraints is
2026: $E_0 = (\Gamma, h, \Omega_0, \rho_0; x_1 \cdots x_g = x_{g+1} \cdots x_d).$
2027: We start with
2028: the $\ell$-factorization of $w_0=\sigma(x_1 \cdots x_g) =
2029: \sigma(x_{g+1} \cdots x_d)$. Let
2030: $$F_\ell(w_0) = \Fl 1k.$$
2031: A sequence $S = \Fl pq$ with $1 \leq p \leq
2032: q \leq k$ is called an {\em $\ell$-factor\/}. We say that $S$ is a
2033: \emph{cover} of a positive interval $[\alpha,\beta]$, if both $|w_1
2034: \cdots w_{p-1}| \leq \alpha$ and $|w_{q+1} \cdots w_k|\leq m_0-\beta$.
2035: Thus, $w_0[\alpha,\beta]$ becomes a factor of $w_p \cdots w_q$.
2036: It is
2037: a {\em minimal cover\/}, if neither $\Fl {p+1}{q}$ nor $\Fl
2038: p{q-1}$ is a cover of $[\alpha,\beta]$. The minimal cover exists and
2039: it is unique.
2040:
2041: We let $\Omega_\ell = \{\,X \in \Omega_0 \mid
2042: \body_\ell(\sigma(X))\neq 1\,\}$, and we are going to define a new
2043: left-hand side $L_\ell \in (B_\ell \cup \Omega_\ell)^*$ and a new
2044: right-hand side $R_\ell \in (B_\ell \cup \Omega_\ell)^*$. For $L_\ell$
2045: we consider those $1 \leq i \leq g$ where $\body_\ell(\sigma(x_i))
2046: \neq 1$. Note that this implies $x_i \in \Omega_\ell$ since $\ell \geq
2047: 1$ and then the $\body$ of a constant is always empty. Recall the
2048: definition of $\leftp(i)$ and $\rightp(i)$, and define
2049: $\alpha=\leftp(i)+|\head_\ell(\sigma(x_i))|$ and $\beta = \rightp(i) -
2050: |\tail_\ell(\sigma(x_i))|$. Then we have $w_0[\alpha,\beta]=
2051: \body_\ell(\sigma(x_i))$. Next consider the $\ell$-factor $S_i = \Fl
2052: pq$ which is the minimal cover of $[\alpha,\beta]$. Then we have $1<p
2053: \leq q < k$ and $w_p \cdots w_q = w_0[\alpha,\beta] =
2054: \body_\ell(\sigma(x_i))$.
2055: The definition of $S_i$ depends only
2056: on $x_i$, but not on the choice of the index $i$.
2057:
2058: We replace the
2059: $\ell$-factor $S_i$ in $F_\ell(w_0)$ by the variable $x_i$. Having
2060: done this for all $1 \leq i \leq g$ with $\body_\ell(\sigma(x_i)) \neq
2061: 1$ we obtain the left-hand side $L_\ell \in (B_\ell \cup
2062: \Omega_\ell)^*$ of the $\ell$-transformation $E_\ell$. For $R_\ell$ we
2063: proceed analogously by replacing those $\ell$-factors $S_i$ where
2064: $\body_\ell(\sigma(x_i)) \neq 1$ and $g+1 \leq i \leq d$.
2065:
2066: For $E_\ell$ we cannot use the alphabet $B_\ell$, because it might be too large or
2067: even infinite. Therefore we let $\Gamma_{\ell'}$ be the smallest subset
2068: of $B_\ell$ which is closed under involution and which satisfies
2069: $L_\ell R_\ell \in (\Gamma_{\ell'} \cup \Omega_\ell)^*$. We let
2070: $\Gamma_\ell = \Gamma_{\ell'} \cup \Gamma$. The projection $\pi_\ell :
2071: \Gamma_\ell^* \to \Gamma^*$ and the mapping $h_\ell : \Gamma_\ell \to M$ are
2072: defined by the restriction of $\pi_\ell: B_\ell \to \Gamma^*$,
2073: $\pi_\ell(u,w,v)=w$ and $h_\ell(u,w,v)=h(w) \in M$ and by
2074: $\pi_\ell(a)=a$ and $h_\ell(a)=h(a)$ for $a \in \Gamma$.
2075:
2076: Finally, we define the mapping $\rho_\ell : \Omega_\ell \to M$ by
2077: $\rho_\ell(X) = h(\body_\ell(\sigma(X)))$. This completes the
2078: definition of the $\ell$-transformation:
2079: $$E_\ell = (\Gamma_\ell , h_\ell, \Omega_\ell, \rho_\ell; L_\ell = R_\ell).$$
2080:
2081: \begin{remark}
2082: One can verify that
2083: $\sigma_\ell: \Omega_\ell \to \Gamma_\ell^*$,
2084: $\sigma_\ell(X) = \phi_\ell(\Body_\ell(\sigma(X)))$ defines a solution of
2085: $E_\ell$, where $\phi_\ell$ is the identity on $\Gamma_\ell$ and $\pi_\ell$
2086: on $B_\ell \setminus \Gamma_{\ell'}$. Although, up to the trivial case $\ell=m_0$,
2087: we make no explicit use of this fact.
2088: \end{remark}
2089:
2090:
2091: \begin{example}
2092: We continue with our example
2093: $a X \ox \oa = Y \ob Y \oa b \oy$ and the solution $\sigma$ which has
2094: been given by
2095: \[
2096: w_0 =\; \mid a \mid d \od \mid
2097: \ob \mid a d \mid
2098: \od \mid \oa \mid b
2099: \mid d \od \mid \oa \mid,
2100: \]
2101: where the bars show the cuts.
2102:
2103: Up to involution,
2104: the set $C_{1}$ is given by $\{ ad, bd, \oa b, d \od \}$ and
2105: $C_2$ is given by $\{ d\od \ob a, \od \ob a d, a d \od \oa, d \od \oa b \}$.
2106: The 1-factorization of $w_0$ can be obtained letter by letter.
2107: The 2-factorization of $w_0$ is given by the following sequence:
2108: \[
2109: (1,a d \od, \ob a) (d \od, \ob, ad) (\od \ob, a d, \od \oa)
2110: (a d, \od, \oa b) ( d \od, \oa, bd) (\od \oa, b, d \od)
2111: (\oa b, d \od a,1).
2112: \]
2113:
2114: Recall $\sigma(X)= d \od \ob a d $ and $\sigma(Y)=a d \od$.
2115: Hence their 2-factorizations are
2116: $ (1,a d \od, \ob a) (d \od, \ob, ad) (\od \ob, a d, 1)$ and
2117: $(1, a d \od, 1)$, respectively.
2118:
2119: By renaming letters, the 2-factorization of $w_0$ becomes
2120: $a \ob c d e b \oa$ and the equation $E$ reduces to
2121: $E_2: aXcdeX\oa = a \ob c d e b \oa$ since the body
2122: of $\sigma(Y)$ is empty.
2123:
2124: The reader can check that the 3-factorization of $w_0$ after
2125: renaming is the very same word as the 2-factorization, but the
2126: 3-factorization of $\sigma(X)$ is now one letter,
2127: $(1, d \od \ob a d, 1)$,
2128: so $E_3$
2129: becomes a trivial equation. Plandowski's algorithm will return
2130: {\em true} at this stage.
2131: \end{example}
2132:
2133:
2134: \begin{remark} \label{extremal}
2135: i) In the extreme case $\ell=m_0$, the $\ell$-transformation becomes
2136: trivial. Let $a=(1,w_0,1)$. Then $\overline{a}=(1,\overline{w_0},1)$ and
2137: $\Gamma_{m_0} = \{a,\overline{a}\} \cup \Gamma$. Moreover, we have
2138: $L_{m_0} = R_{m_0} = a$, and $h_{m_0}(a) = h(w_0) \in M$. Since
2139: $\Omega_{m_0}= \emptyset$, the equation with constraints $E_{m_0}$ has
2140: trivially a solution. It is clear that $E_{m_0}$ is a node in the search
2141: graph, and if we reach $E_{m_0}$, then the algorithm will return
2142: {\em true\/}.
2143:
2144: ii) The other extreme case is $\ell=1$. The situation again is simple,
2145: but the precise definition is technically more involved.
2146: Consider a block $(u,w,v)$ which appears in $F_1(w_0)$. Then
2147: $w=w_0[\alpha, \beta]$ for some $\beta-\alpha \geq 1$. We cannot have
2148: $\beta - \alpha \geq 2$, because then $[\alpha, \beta]$ would have
2149: an implicit cut $\gamma$, but $w_0[\gamma-1, \gamma+1] \in C_1$
2150: and no critical word is a factor of $w$. An immediate
2151: consequence is $|\Gamma_1| \leq (|\Gamma|+1)^3 \in \OO(d^3)$. Let
2152: $X \in \Omega_0$. Then $\Body_1(\sigma(X)) \neq 1$ if and only if
2153: $|\sigma(X)| \geq 3$. Thus, for $X \in \Omega_1$ we have
2154: $\sigma(X) = bcu =vde$ with $b,c,d,e \in \Gamma$ and $u,v \in \Gamma^+$.
2155: It follows:
2156: $$F_1(\sigma(X)) = (1,b,c)(b,c,v_2)\cdots(u_{|v|+1},d,e)(d,e,1).$$
2157: For example, for $|v|=1$ this means $b=u_{|v|+1}$, $c=d$, and $v_2=e$.
2158:
2159: We can describe
2160: $L_1 \in \Gamma_1^*$ as follows:
2161:
2162: For $1 \leq i \leq g$ let $w_i=\sigma(x_i)$
2163: and $a_i$ the last letter of $\sigma(x_{i-1})$ if $i>1$ and $a_1=1$.
2164: Let $f_i$ the first letter of $\sigma(x_{i+1})$ if $i<g$ and $f_g=1$. Let
2165: $b_i$ the first letter of $w_i$ and $e_i$ the last letter of $w_i$.
2166:
2167: For $|w_i|=1$ we replace $x_i$ by the $1$-factor $(a_i,b_i,f_i)$.
2168:
2169: For $|w_i|=2$ we replace $x_i$ by the $1$-factor $(a_i,b_i,e_i)(b_i,e_i,f_i)$.
2170:
2171: For $|w_i|\geq3$ we let $c_i$ be the second letter of $w_i$ and $d_i$ its
2172: second last. In this case we replace $x_i$ by $(a_i,b_i,c_i)x_i(d_i,e_i,f_i)$.
2173:
2174: The definition of $R_1$ is analogous. Thus, we obtain
2175: $|L_1R_1| \leq 3|L_0 R_0| = 3d$, and $E_1$ is admissible. We also see that
2176: there was an overestimation of the size of $|\Gamma_1|$. For each $x_i$ we
2177: need at most two constants together with their involutions. Since
2178: $\Gamma_1$ contains also $\Gamma$, we obtain
2179: $|\Gamma_1|\leq 6d$.
2180: \end{remark}
2181:
2182: By the remark above, $E_1$ and $E_{m_0}$ are admissible and hence
2183: nodes of the search graph. The goal is to reach $E_{m_0}$
2184: via $E_1$ when starting with $E_0$. For the
2185: moment it is even not clear that the $\ell$-transformations with $1 <
2186: \ell < m_0$ belongs to the search graph. We prove this statement in
2187: the next section.
2188:
2189: \section{The $\ell$-transformation $E_\ell$ is admissible}
2190:
2191: \begin{proposition} \label{ladm}
2192: There is a polynomial $p$ (of degree at most 4) such that each $E_\ell$
2193: is admissible for all $\ell \geq 1$.
2194: \end{proposition}
2195:
2196: \begin{proof}
2197: It is enough to show that $L_\ell$ and $R_\ell$ can be represented by
2198: exponential expressions of size $\OO(d^2(d+n\log n))$. Then $\Gamma_\ell$ can have
2199: size at most $\OO(d^2(d+n\log n))$ and the assertion follows. We will estimate the
2200: size of an exponential expression for $L_\ell$, only.
2201:
2202: We start again with the $\ell$-transformation of
2203: $$F_\ell(w_0) = \Fl 1k.$$
2204: If $k$ is small there is nothing to do since $|L_\ell| \leq |F_\ell(w_0)|$.
2205: An easy reflection shows that $|L_\ell|$ can become large, only if there is
2206: some $1 \leq i \leq g$ such that $\head_\ell(\sigma(x_i))$ or
2207: $\tail_\ell(\sigma(x_i))$ is long. By symmetry we treat the case
2208: $\head_\ell(\sigma(x_i))$ only and we fix some notation. We let
2209: $1 \leq i \leq g$, $\alpha = \leftp(i)$, and
2210: $\beta = \alpha+|\head_\ell(\sigma(x_i))|$. Let
2211: $$\Fl{p-1}{q+1}$$
2212: be a minimal cover of $[\alpha,\beta]$. We may assume that $q-p$ is large.
2213: It is enough to find an exponential expression for the
2214: $\ell$-factor
2215: $$\Fl{p}{q}$$
2216: having size in $\OO(d(d+n\log n))$, because we want the whole expression
2217: to have size in $\OO(d^2(d+n\log n))$.
2218:
2219: Note that $w_p \cdots w_q$ is a proper factor of $\head_\ell(\sigma(x_i))$.
2220: Hence no critical word of $C_\ell$ can appear as a factor inside
2221: $w_p \cdots w_q$. This means there is some $p \leq s \leq q$ such that
2222: both $|w_p \cdots w_{s-1}| < \ell$ and $|w_{s+1} \cdots w_q| < \ell$. Indeed,
2223: if $|w_p \cdots w_{q-1}| < \ell$, then we choose $s=q$. Otherwise we let
2224: $p\leq s \leq q$ be minimal such that $|w_p \cdots w_s| \geq \ell$. Then
2225: $|w_{s+1} \cdots w_q| \geq \ell$ is impossible because
2226: $u_{s+1}v_s \in C_\ell$ would appear as a factor in $w_p \cdots w_q$. We can
2227: write
2228: $$ \Fl pq = S_1 \uwv s S_2;$$
2229: and since $\uwv s \in \Gamma_\ell$ is a letter, it is enough to find
2230: exponential expressions for $S_i$, $i=1,2$, of size $\OO(d(d+n\log n))$ each.
2231: As a conclusion it is enough to prove the following lemma. \qed
2232: \end{proof}
2233:
2234: The statement of the next lemma is slightly more general as we need it
2235: above. There we need the lemma for $c = 1$, but later we
2236: will apply the lemma with values $c \leq 32 d$.
2237:
2238: \begin{lemma} \label{short}
2239: Let $c > 0$ be a number and
2240: $$S=\Fl{1}{k} \in B_\ell^*$$
2241: be a sequence which appears as some $\ell$-factor in $F_\ell(w_0)$. If we
2242: have $k \leq 3$ or $|w_2 \cdots w_{k-1}| \leq c\ell$, then we can represent
2243: the sequence by some exponential expression of size $\OO(cd(d+n\log n))$.
2244: \end{lemma}
2245:
2246: \begin{proof}
2247: We show that there is an exponential expression of size
2248: $\OO(d(d+n\log n))$ under the assumption $|w_1 \cdots w_k|<\ell$.
2249: This is enough, because we always can write $S$ as $a_0S_1 a_1
2250: \cdots S_{c'} a_{c'}$, where $c'\leq c $, the $a_i$ are letters, and
2251: each $S_i$ satisfies the assumption. Note that the assumption
2252: implies $u_1 \neq 1 \neq v_k$
2253: and we may define $u_{k+1}$ as the suffix
2254: of length $\ell$ of $u_1w_1 \cdots w_k$. For $1 \leq i \leq k$ let
2255: $z_i=u_{i+1}v_i$. Then $z_i \in C_\ell$ is a critical word which
2256: appears as a factor in $z = u_1 w_1 w_2 \cdots w_k v_k$. If the
2257: words $z_i$, $1 \leq i <k$ are pairwise different, then $k-1 \leq
2258: |C_\ell| \in \OO(d)$ and we are done. Hence we may assume that
2259: there are repetitions. Let $j$ be the smallest index such that a
2260: critical word is seen for the second time and let $i<j$ be the first
2261: appearance of $z_j$. This means for $1 \leq i < j$ the words $z_1,
2262: \cdots, z_{j-1}$ are pairwise different and $z_i=z_j$. Now, $|w_1
2263: \cdots w_k|<\ell$ and $|z_i|=2\ell$, hence $z_i$ and $z_j$ overlap
2264: in $z$. We can choose $r$ maximal such that $u_1 w_1 \cdots w_i
2265: (w_{i+1} \cdots w_j)^rv_j$ is a prefix of the word $z$. (Note that
2266: the last factor $v_j$ insures that the prefix ends with $z_j$). For
2267: some index $s>j$ we can write
2268: $$
2269: z=u_1 w_1 \cdots w_i (w_{i+1} \cdots w_j)^r w_s \cdots w_k v_k.$$
2270: We claim that $z_i \not \in \{z_s, \ldots, z_k\}$. Indeed,
2271: let $t$ be maximal such that $z_i = z_t$ and assume that $j\not= t$. Then both
2272: $|w_{i+1} \cdots w_{j}|$ and $|w_{j+1} \cdots w_{t}|$ are periods of
2273: $z_i$, but $|w_{i+1} \cdots w_{t}| \leq |z|$. Hence by Fine and
2274: Wilf's Theorem \cite{Lothaire83} we obtain that the greatest common divisor
2275: of $|w_{i+1} \cdots w_{j}|$ and $|w_{j+1} \cdots w_{t}|$
2276: is a period, too. Due to the definition of an $\ell$-factorization
2277: ($z_j$ was the first repetition) the length $|w_{j+1} \cdots w_{t}|$
2278: is therefore a multiple of $|w_{i+1} \cdots w_{j}|$ and
2279: we must have $t = s-1$. This shows the claim. Moreover, we have
2280: \begin{eqnarray*}
2281: & & \Fl 1k \\
2282: & = & \Fl 1i [\Fl {i+1} j]^r\, S'
2283: \end{eqnarray*}
2284: where $S' = \Fl sk$ for $ s = i +1 + r(j-i)$.
2285: We have $r \leq \pexp(w_0)$, hence $r \in 2^{\OO(d+n\log n)}$. It follows that
2286: $$\Fl 1i[\Fl {i+1}j]^r$$
2287: is an exponential expression of size $j+
2288: \log(r) \in \OO(d+n\log n)$. More precisely, for some suitable
2289: constant $\widetilde c$ its size is at most $\widetilde c(d+n\log n)$.
2290: The constant $\widetilde c$ depends only on the constant which is
2291: hidden when writing $\exp(w_0) \in 2^{\OO(d+n\log
2292: n)}$. By induction on the size of the set $\{z_1, \ldots, z_k\}$ we
2293: may assume that $S'= \Fl sk$ has an exponential expression of size at
2294: most $|\{z_s, \ldots, z_k\}| \widetilde c (d+n)$. Hence the
2295: exponential expression for $S$ has size at most
2296: $$\widetilde c (d+n\log n ) + |\{z_s, \ldots, z_k\}|\widetilde c
2297: (d+n\log n) \leq |\{z_1, \ldots, z_k\}|\widetilde c (d+n\log n).$$
2298: Thus, the size is in $\OO(d(d+n\log n))$. \qed
2299: \end{proof}
2300:
2301: At this stage we know that all $\ell$-transformations are admissible
2302: (with respect to some suitable polynomial of degree 4). Thus $E_1, \ldots, E_{m_0}$
2303: are nodes of the search graph. Next we show that the search graph contains
2304: arcs $E_0 \rightarrow E_1$ and $E_\ell \rightarrow E_{{\ell'}}$ for
2305: $1 \leq \ell < {\ell'} \leq 2\ell$. Hence the graph contains a path
2306: (of logarithmic length in $m_0$) from $E_0$ to $E_{m_0}$. The
2307: non-deterministic procedure is able to find this path and on input
2308: $E_0$ Plandowski's algorithm gives the correct answer.
2309:
2310: In order to establish the existence of arcs from $E_\ell$ to
2311: $E_{{\ell'}}$ for $0 \leq \ell < {\ell'} \leq \max \{1, 2\ell\}$ we shall
2312: define intermediate equations $E_{\ell,{\ell'}}$ such that there is an
2313: admissible base change $\beta$, a projection $\pi$, and a partial solution $\delta$
2314: with
2315: $$\delta_*(\pi^*(E_\ell)) \equiv E_{\ell,{\ell'}} \equiv \beta_*(E_{{\ell'}}).$$
2316:
2317: \section{The arc from $E_0$ to $E_1$}
2318:
2319: Recall the definition of
2320: $E_1=(\Gamma_1 , h_1, \Omega_1, \rho_1; L_1 = R_1).$
2321: The letters of $\Gamma_1$ can be
2322: written either as $(a,b,c)$ or as $b$ with $a,c \in \Gamma \cup \{1\}$
2323: and $b\in \Gamma$. We define a projection which is used here as a base
2324: change $\beta: \Gamma_1 \to \Gamma$ by $\beta(a,b,c)=b$ and leaving
2325: the letters of $\Gamma$ invariant. Clearly, $h_1=h\beta$, and $\beta$
2326: defines an admissible base change. Define $E_{0,1}=\beta_*(E_1)$. Then
2327: we have $L_{0,1}=\beta(L_1)$ and $R_{0,1}=\beta({R_1})$ where $\beta:
2328: (\Gamma_1 \cup \Omega_1)^* \to (\Gamma \cup \Omega_1)^*$ is the extension
2329: with $\beta(X)=X$ for all $X \in \Omega_1$. We have $\Gamma_{0,1} =
2330: \Gamma$
2331:
2332: It is now obvious how to define the partial solution
2333: $\delta: \Omega_0 \to \Gamma \Omega_1 \Gamma \cup \Gamma^*$
2334: such that $\delta_*(E_0) = E_{0,1}$. If $|\sigma(X)| \leq 2$, then we let
2335: $\delta(X) = \sigma(X)$. For $|\sigma(X)|\geq 3 $ we write $\sigma(X)=aub$
2336: with $a,b \in \Gamma$ and $u\in \Gamma^+$. Then we have
2337: $X \in \Omega_1 = \Omega_{0,1}$ and we define $\delta(X)=aXb$ and
2338: $\rho_{0,1}(X)=h(u)$. For $X \in \Omega_1$ we have
2339: $\rho_1(X)=h(\body_1(\sigma(X)))$, hence $\rho_{0,1}=\rho_1$, too.
2340: This shows that, indeed, $\delta_*(E_0)=\beta_*(E_1)$.
2341: Formally, we can write this as $\delta_*(\pi^*(E_0)) =\beta_*(E_1)$,
2342: where $\pi$ is the identity. Hence there is an arc from $E_0$ to
2343: $E_1$.
2344:
2345: \section{The equations $E_{\ell,{\ell'}}$ for $1\leq\ell<{\ell'}\leq 2\ell$}
2346:
2347: In this section we define for each $1\leq\ell<{\ell'}\leq 2\ell$
2348: an intermediate equation with constraints
2349: $$ \beta_*(E_{\ell'}) =
2350: E_{\ell,{\ell'}}=(\Gamma_{\ell,{\ell'}}, h_{\ell,{\ell'}}, \Omega_{{\ell'}}, \rho_{{\ell'}} ; L_{\ell,{\ell'}} = R_{\ell,{\ell'}})$$
2351: by some base change $\beta : \Gamma_{{\ell'}} \to (B_\ell \cup \Gamma)^*$, then we show
2352: that $\beta$ is admissible.
2353:
2354:
2355: Recall $\Gamma \subseteq \Gamma_{\ell'} \subseteq B_{\ell'} \cup \Gamma$.
2356: The base change $\beta$ leaves
2357: the letters of $\Gamma$ invariant.
2358: Consider some $(u,w,v) \in \Gamma_{{\ell'}}\setminus \Gamma$. It is enough to define
2359: $\beta(u,w,v)$ or $\beta(\overline{v},\overline{w},\overline{u})$.
2360: Hence we may assume that $(u,w,v)$ appears as a letter in the
2361: ${\ell'}$-factorization $F_{{\ell'}}(w_0)$. Therefore we find a positive
2362: interval $[\alpha,\beta]$ such that $w=w_0[\alpha,\beta]$ and such
2363: that the following two conditions are satisfied:
2364:
2365: 1) We have $u=1$ and $\alpha=0$ or
2366: $|u| = {\ell'}$, $\alpha \geq {\ell'}$, and $u = w_0[\alpha-{\ell'},\alpha]$.
2367:
2368: 2) We have $v=1$ and $\beta=m_0$ or $|v| = {\ell'}$, $\beta \leq m_0-{\ell'}$,
2369: and $v = w_0[\beta, \beta+{\ell'}]$.
2370:
2371: Let $\Fl pq$ be the $\ell$-factor which is the minimal cover of $[\alpha,\beta]$
2372: with respect to the $\ell$-factorization $F_\ell(w_0)$. Since
2373: $\ell \leq {\ell'}$ we have $w_p \cdots w_q= w$. Moreover, the word $u_p$
2374: is a suffix of $u$ and $v_q$ is a prefix of $v$. We define
2375: $$\beta(u,w,v) = \Fl pq \in B_\ell^+.$$
2376: The definition does not depend on the choice of $[\alpha,\beta]$ as long
2377: as $0 \leq \alpha < \beta \leq m_0$ and 1) and 2) are satisfied. We have
2378: $\overline{\beta(u,w,v)} = \beta(\overline{v},\overline{w},\overline{u})$
2379: and $h_\ell\beta = h_{{\ell'}}$. Now let
2380: $\Gamma_{\ell,{\ell'}} \subseteq B_\ell \cup \Gamma$ be the smallest subset such that
2381: $\beta(\Gamma_{{\ell'}}) \subseteq \Gamma_{\ell,{\ell'}}^*$. Then
2382: $\Gamma_{\ell, {\ell'}}$ contains $\Gamma$ and it is closed under involution (since $\Gamma_{{\ell'}}$
2383: has this property). A crucial, but easy reflection shows that
2384: $\Gamma_\ell \subseteq \Gamma_{\ell, {\ell'}}$.
2385: This will become essential later.
2386:
2387: We view $\beta$ as a homomorphism $\beta: \Gamma_{\ell'}^* \to
2388: \Gamma_{\ell, {\ell'}}^*$ and define $E_{\ell, {\ell'}} =
2389: \beta_*(E_{{\ell'}})$. Let us show that $\beta$ defines an admissible
2390: base change. Since $E_{{\ell'}}$ is already known to be admissible with
2391: respect to some polynomial of degree 4, it is enough to find some admissible
2392: exponential expression (again with respect to some polynomial of degree 4)
2393: for the $\ell$-factor
2394: $$\beta(u,w,v)= \Fl pq$$ where $(u,w,v) \in \Gamma_{{\ell'}}\setminus
2395: \Gamma$.
2396: We use the same notations as above. Thus, for
2397: some positive interval $[\alpha,\beta]$ we have
2398: $w_p \cdots w_q=w_0[\alpha,\beta]$, the word $u$ is a suffix of
2399: $w_0[0,\alpha]$, and $v$ is a prefix of $w_0[\beta,m_0]$. If $q-p$ is small,
2400: there is nothing to do. By Lemma~\ref{short} we may also assume that
2401: $\beta-\alpha > 32 d \ell$. We are to define inductively a sequence of
2402: positions
2403: $$\alpha=\alpha_0<\alpha_1<\cdots<\alpha_i<\cdots<\beta_i<\cdots<\beta_1<\beta_0=\beta.$$
2404: Each time we let $W_i=w_0[\alpha_i,\beta_i]$. Thus, $W_0=w_p \cdots w_q$.
2405: Assume that $W_i=w_0[\alpha_i,\beta_i]$ is already defined
2406: such that $\beta_i-\alpha_i \geq 2$.
2407: The interval $[\alpha_i,\beta_i]$ is not free. Hence, there is some
2408: implicit cut $\gamma_i$ with $\alpha_i < \gamma_i <\beta_i$. The word
2409: $W_i$ is a factor of $w$, hence no factor of $W_i$ belongs to the set of
2410: critical words $C_{{\ell'}}$. This implies $\beta_i-\gamma_i<{\ell'}$ or
2411: $\gamma_i-\alpha_i<{\ell'}$. If we have $\beta_i-\gamma_i<{\ell'}$ then we let
2412: $\alpha_{i+1}=\alpha_i$ and $\beta_{i+1}=\gamma_i$. In the other case we
2413: let $\alpha_{i+1}=\gamma_i$ and $\beta_{i+1}=\beta_i$. Thus $W_{i+1}$ is
2414: defined such that $W_{i+1}$ is a proper factor of $W_i$ with
2415: $|W_i| - |W_{i+1}| < {\ell'}$.
2416:
2417: We need some additional book keeping. We define $r_i \in \{\leftp,\rightp\}$
2418: by $r_i=\rightp$ if $\beta_i=\beta_{i+1}$ and $r_i=\leftp$ otherwise
2419: (i.e., $\alpha_i=\alpha_{i+1}$). Furthermore the implicit cut $\gamma_i$
2420: corresponds to some real cut $\gamma_i'$ and $\alpha_i'<\gamma_i'<\beta_i'$
2421: such that $W_i=w_0[\alpha_i',\beta_i']$ or $W_i=w_0[\beta_i',\alpha_i']$.
2422: We define $s_i \in \{+,-\}$ by $s_i=+$ if $W_i=w_0[\alpha_i',\beta_i']$ and
2423: $s_i=-$ otherwise (in particular, $s_i=-$ implies
2424: $\overline{W_i} = w_0[\alpha_i',\beta_i']$). The triple $(\gamma_i',r_i,s_i)$
2425: is denoted by $\gamma(i)$. There are at most $4(d-2)$ such triples and
2426: $\gamma(i)$ is defined whenever $W_{i+1}$ is defined. We stop the induction
2427: procedure after the first repetition. Thus we find $0 \leq i < j < 4d$
2428: such that $\gamma(i)=\gamma(j)$. We obtain a sequence
2429: $W_0, W_1, \ldots, W_i, \ldots, W_j$ where each word is a proper factor of the
2430: preceding one. We have $|W_0|-|W_j|<4d{\ell'} \leq 8d\ell$ and due to
2431: $|W_0|>32 d\ell$ the sequence above really exists, moreover $|W_j| >8d\ell$.
2432:
2433: Next, we show that $W_j$ has a non-trivial overlap with itself. We treat the
2434: case $\gamma(i)=\gamma(j)=(\gamma,\rightp,+)$ only.
2435: The other three cases $(\gamma,\rightp,-)$, $(\gamma,\leftp,+)$,
2436: and $(\gamma,\leftp,-)$ can be treated analogously.
2437: For some $\alpha' < \gamma <\beta'$ we have $W_i=w_0[\alpha',\beta']$
2438: and $W_{i+1}=w_0[\gamma,\beta']$. Thus, for some
2439: $\gamma \leq \mu < \nu \leq \beta'$ we have $W_j=w_0[\mu,\nu]$ and we can
2440: assume that $\mu-\gamma<(j-i){\ell'}\leq 4d{\ell'}-{\ell'} \leq 8d\ell-{\ell'}$.
2441: On the other hand we have $\gamma(j)=(\gamma,\rightp,+)$, too. Hence
2442: for some $\mu'<\gamma<\nu'$ with $\gamma-\mu'<{\ell'}$ we have
2443: $W_j = w_0[\mu',\nu']$, too. Therefore $0 <\mu-\mu'<8d\ell$ and
2444: $W_j$ has some non-trivial overlap. We can write $W_j=W^e W'$ such that
2445: $1 \leq |W| <8d\ell$ and $W'$ is a prefix of $W$.
2446:
2447: Putting everything together, we arrive in all cases at a factorization
2448: $W_0=UW^eV$ with $e \leq \pexp(w_0)$, $1 \leq |W| <8d\ell$, and
2449: $|U|+|V|<16d\ell$. However, we have not finished yet. Recall that we are
2450: looking for an admissible exponential expression for
2451: $$\beta(u,w,v) = \Fl pq.$$
2452: Due to $|W_0|>\ell$ we can choose $r$ minimal, $p<r \leq q+1$, and $s$
2453: maximal $p-1 \leq s < q$ such that $|w_p \cdots w_{r-1}|>|U|+\ell$
2454: and $|w_{s+1} \cdots w_q| > |V|+\ell$. By Lemma~\ref{short} we may assume
2455: $r<s$ and it is enough to find an exponential expression for
2456: $$S=\Fl rs.$$
2457: Note that the word $u_r w_r w_{r+1} \cdots w_s v_s$ is a factor of
2458: $W^e$.
2459: Again, we may assume that $w_r w_{r+1} \cdots w_s > 32 d\ell$.
2460: By switching to some conjugated word $W'$ if necessary, we may assume that
2461: $u_r w_r w_{r+1}\cdots w_s v_s$ is a prefix of $W^e$. Moreover, by
2462: symmetry we may choose a positive interval $[\alpha,\beta]$ such that
2463: $w_0[\alpha,\beta]=u_r w_r w_{r+1} \cdots w_s v_s$. Clearly, we
2464: have $w_0[i,j] = w_0[i+|W|,j+|W|]$ for all $\alpha \leq i < j \leq \beta-|W|$.
2465: In particular, the critical word $w_0[\alpha, \alpha+2\ell]$ appears as
2466: $w_0[\alpha+|W|, \alpha+|W|+2\ell]$ again. This means that there is some
2467: $r \leq t < s$ such that $|w_r \cdots w_t|=|W|$. More precisely, we can
2468: choose $r\leq t < t' \leq s$ and a maximal $e'\leq e$ such that
2469: $$S = \bigl( \Fl rt \bigr)^{e'}\Fl {t'}s.$$
2470: Since it holds $e'\leq \pexp(w_0)$, $|w_r \cdots w_t|=|W|$, and
2471: $|w_{t'}\cdots w_s|\leq |W|$, the existence of an admissible
2472: exponential expression for $\beta(u,w,v)$
2473: follows. Hence $\beta$ is an admissible
2474: base change.
2475:
2476:
2477: \section{Passing from $E_\ell$ to $E_{\ell,{\ell'}}$ for $1\leq \ell <
2478: {\ell'} \leq 2\ell$}
2479:
2480: In the final step we have to show that there exists some projection $\pi:
2481: \Gamma_{\ell,{\ell'}}^* \to \Gamma_\ell^*$ and some partial solution
2482: $\delta:\Omega_{\ell} \to \Gamma_{\ell,{\ell'}}^* \Omega_{{\ell'}}
2483: \Gamma^*_{\ell,{\ell'}} \cup \Gamma^*_{\ell,{\ell'}}$ such that
2484: $\delta_*(\pi^*(E_\ell)) \equiv E_{\ell,{\ell'}}$. We don't
2485: have to care about admissibility anymore.
2486:
2487: For the projection we have to consider a letter in
2488: $\Gamma_{\ell,{\ell'}} \setminus \Gamma_\ell$. Such a letter has the
2489: form $(u,w,v)\in B_\ell$ and we may define $\pi(u,w,v) = w$ since
2490: $\Gamma \subseteq \Gamma_\ell$.
2491:
2492: Clearly
2493: $\pi(\overline{(u,w,v)}) = \overline{\pi(u,w,v)}$ and
2494: $h_{\ell,{\ell'}}(u,w,v) = h_{{\ell'}}(u,w,v) = h(w) =
2495: h_\ell(\pi(u,w,v))$ are verified. Thus $\pi: \Gamma_{\ell,{\ell'}}^*
2496: \to \Gamma_\ell^*$ defines a projection such that
2497: $$\pi^*(E_\ell) = (\Gamma_{\ell,{\ell'}}, h_{\ell,{\ell'}},
2498: \Omega_{\ell}, \rho_\ell; L_\ell = R_\ell).$$
2499: We have to define a partial solution $\delta: \Omega_{\ell} \to
2500: \Gamma_{\ell,{\ell'}}^* \Omega_{{\ell'}} \Gamma^*_{\ell,{\ell'}} \cup
2501: \Gamma^*_{\ell,{\ell'}}$ such that $\delta(L_\ell) = \beta(L_{{\ell'}})$
2502: and $\delta(R_\ell) = \beta(R_{{\ell'}})$. For this, we have to consider a
2503: variable $X\in\Omega$ with $\body_\ell(\sigma(X)) \neq 1$.
2504: By symmetry, we may
2505: assume that $X = x_i$ for some $1 \leq i \leq g$. Hence $\sigma(X) =
2506: w_0[\leftp(i),\rightp(i)]$.
2507:
2508: Let $\alpha = \leftp(i) + |\head_\ell(\sigma(X))|$ and $\beta =
2509: \rightp(i) - |\tail_\ell(\sigma(X))|$. Then $\leftp(i) + \ell \leq
2510: \alpha < \beta \leq \rightp(i)-\ell$. Let $(u_p,w_p,v_p) \cdots
2511: (u_q,w_q,v_q)$ be the minimal cover of $[\alpha,\beta]$ with respect
2512: to the $\ell$-factorization. We have $w_p\cdots w_q =
2513: \body_\ell(\sigma(X))$.
2514:
2515: For $\body_{{\ell'}}(X) = 1$ we have $X\in\Omega_\ell \setminus
2516: \Omega_{{\ell'}}$ and we define $$\delta(X) = (u_p,w_p,v_p) \cdots
2517: (u_q,w_q,v_q).$$ Then $\delta(X)\in B_\ell^*$ and $h_\ell \delta(X) =
2518: \rho_\ell(X)$ since $\rho_\ell(X) = h(\body_\ell( \sigma(X)))$. It is
2519: also clear that the definition does not depend on the choice of $i$,
2520: and we have $\delta(\overline{X}) = \overline{\delta(X)}$.
2521:
2522: Recall the definition of $L_{{\ell'}}$. Since $\body_{{\ell'}}(\sigma(X))
2523: = 1$, there is a factor $f_1\cdots f_r$ of $L_{{\ell'}}$ which belongs
2524: to $\Gamma_{{\ell'}}^*$ and $f_1\cdots f_r$ covers $[\alpha,\beta]$ with
2525: respect to the ${\ell'}$-factorization $F_{{\ell'}}(w_0)$. It follows
2526: that $\delta(X)$ is a factor of $\beta(f_1\cdots f_r)$, hence
2527: $\delta(X) \in \Gamma_{\ell,{\ell'}}^*$ by definition of
2528: $\Gamma_{\ell,{\ell'}}$.
2529:
2530: For $\body_{{\ell'}}(X) \neq 1$ we have $X\in\Omega_{{\ell'}}$ and we find
2531: positions $\mu < \nu$ such that $\mu = \leftp(i) +
2532: |\head_{{\ell'}}(\sigma(X))|$ and $\nu = \rightp(i) -
2533: |\tail_{{\ell'}}(\sigma(X))|$.
2534:
2535: For some $p \leq r \leq s \leq q$ we have $w_0[\alpha,\mu] = w_p
2536: \cdots w_{r-1}$, $w_0[\nu,\beta] = w_{s+1} \cdots w_q$, and
2537: $\body_{{\ell'}}(\sigma(X)) = w_r \cdots w_s$. We define
2538: \begin{displaymath}
2539: \delta(X) = (u_p,w_p,v_p) \cdots (u_{r-1},w_{r-1},v_{r-1}) X
2540: (u_{s+1},w_{s+1},v_{s+1}) \cdots (u_q,w_q,v_q).
2541: \end{displaymath}
2542: As above, we can verify that $\delta(X) = UXV$ with $U,V \in
2543: \Gamma_{\ell,{\ell'}}^*$ such that $\delta(\overline{X}) =
2544: \overline{V}\,\overline{X}\,\overline{U}$ and $\rho_\ell(X) =
2545: h_{\ell,{\ell'}}(U) \rho_{{\ell'}}(X) h_{\ell,{\ell'}}(V)$.
2546: Finally, $\delta(L_\ell) = L_{{\ell'}}$ and $\delta(R_\ell) =
2547: R_{{\ell'}}$. Hence $\delta_*(\pi^*(E_\ell)) = \beta_*(E_{{\ell'}})$.
2548: This proves Theorem~\ref{theo3}.
2549:
2550:
2551: \section{Conclusion}
2552: In this paper we were dealing with the existential theory, only. For
2553: free groups it is also known that the positive theory without
2554: constraints is decidable, see \cite{mak84}. Thus, one can allow also
2555: a mixture of existential and universal quantifiers, if there
2556: are no negations at all. Since a negation can be replaced with
2557: the help of an extra variable and some positive rational constraint,
2558: one might be tempted to prove that
2559: the
2560: positive theory of equations with rational constraints in free groups
2561: is decidable. But such a program must fail: Indeed,
2562: by \cite{marchenkov82} and \cite{durnev95} it is known that the
2563: positive $\forall\exists^{3}$-theory of word equations is unsolvable.
2564: Since $\Sigma^*$ is a rational
2565: subset of the free group
2566: $F(\Sigma)$, this theory can be encoded in the positive theory
2567: of equations with rational constraints in free groups, and the
2568: later is undecidable, too. On the other hand, a
2569: negation leads to a positive constraint of a very restricted type, so
2570: the interesting question remains under which type of constraints the
2571: positive theory becomes decidable.
2572:
2573: \paragraph{Acknowledgments}
2574: The research was partly supported by the German Research Foundation
2575: {\em Deutsche Forschungsgemeinschaft, DFG}. In addition, C.~Guti\'errez thanks
2576: Centro de Modelamiento Matem\'atico, FONDAP Ma\-te\-m\'a\-ti\-cas Discretas,
2577: for financial support.
2578:
2579:
2580: %%%%%%%%%%%%%%%%%%%%%%
2581: \bibliographystyle{plain}
2582:
2583: \newcommand{\IJ}{IJ}\newcommand{\Ju}{Ju}\newcommand{\Th}{Th}\newcommand{\Yu}{Y%
2584: u}\newcommand{\HHHH}{}\newcommand{\VVVV}{}\newcommand{\NNNN}{}
2585: \begin{thebibliography}{10}
2586:
2587: \bibitem{ben69}
2588: Mich{\`e}le Benois.
2589: \newblock Parties rationelles du groupe libre.
2590: \newblock {\em C. R. Acad. Sci. Paris, S{\'e}r. A}, 269:1188--1190, 1969.
2591:
2592: \bibitem{berstel79}
2593: Jean Berstel.
2594: \newblock {\em Transductions and context-free languages}.
2595: \newblock Teubner Studienb{\"u}cher, Stuttgart, 1979.
2596:
2597: \bibitem{die98lothaire}
2598: Volker Diekert.
2599: \newblock Makanin's {A}lgorithm.
2600: \newblock In M.~Lothaire, editor, {\em Algebraic Combinatorics on Words}.
2601: Cambridge University Press, 2001.
2602: \newblock To appear. A preliminary version is on the web:\\ http:
2603: //www-igm.univ-mlv.fr/~berstel/Lothaire/index.html.
2604:
2605: \bibitem{dgh2001}
2606: Volker Diekert, Claudio Guti{\'{e}}rrez, and Christian Hagenah.
2607: \newblock The existential theory of equations with rational constraints in free
2608: groups is {PSPACE}-complete.
2609: \newblock In A.~Ferreira and H.~Reichel, editors, {\em Proc.\ of the 18th STACS
2610: (STACS'01), Dresden}, Lecture Notes in Computer Science 2010,
2611: pages 170--182. Springer, 2001.
2612:
2613: \bibitem{dl2001}
2614: Volker Diekert and Markus Lohrey.
2615: \newblock A note on the existential theory in plain groups.
2616: \newblock {\em International Journal of Algebra and Computation}, 2001.
2617: \newblock To appear.
2618:
2619: \bibitem{dmm99tcs}
2620: Volker Diekert, {\Yu}ri Matiyasevich, and Anca Muscholl.
2621: \newblock Solving word equations modulo partial commutations.
2622: \newblock {\em Theoretical Computer Science}, 224:215--235, 1999.
2623: \newblock Special issue of LFCS'97.
2624:
2625: \bibitem{durnev95}
2626: Valery~G. Durnev.
2627: \newblock Undecidability of the positive $\forall\exists^{3}$-theory of a free
2628: semi-group.
2629: \newblock {\em Sib. Mat. Zh.}, 36(5):1067--1080, 1995.
2630: \newblock In Russian; English translation: {\em Sib. Math. J., 36\/}(5),
2631: 917--929, 1995.
2632:
2633: \bibitem{gv97icalp}
2634: Yuri Gurevich and Andrei Voronkov.
2635: \newblock Monadic simultaneous rigid {E}-unification and related problems.
2636: \newblock In P.~Degano, R.~Gorrieri, and A.~Marchetti-Spaccamela, editors, {\em
2637: Proc. 24th ICALP (ICALP'97), Bologna (Italy) 1997}, number 1256 in Lecture
2638: Notes in Computer Science, pages 154--165. Springer, 1997.
2639:
2640: \bibitem{gut98focs}
2641: Claudio Guti{\'e}rrez.
2642: \newblock Satisfiability of word equations with constants is in exponential
2643: space.
2644: \newblock In {\em Proc.~of the 39th Ann.~Symp. on Foundations of Computer
2645: Science, FOCS'98}, pages 112--119, Los Alamitos, California, 1998. IEEE
2646: Computer Society Press.
2647:
2648: \bibitem{gut2000stoc}
2649: Claudio Guti{\'e}rrez.
2650: \newblock Satisfiability of equations in free groups is in {PSPACE}.
2651: \newblock In {\em 32nd Ann.~ACM Symp. on Theory of Computing (STOC'2000)},
2652: pages 21--27. ACM Press, 2000.
2653:
2654: \bibitem{hagenahdiss2000}
2655: Christian Hagenah.
2656: \newblock {\em Gleichungen mit regul{\"a}ren {R}andbedingungen {\"u}ber freien
2657: {G}ruppen}.
2658: \newblock Ph.{D}.-thesis, Institut f{\"u}r {I}nformatik, {U}niversit{\"a}t
2659: {S}tuttgart, 2000.
2660:
2661: \bibitem{hu79}
2662: John~E. Hopcroft and Jeffrey~D. Ullman.
2663: \newblock {\em Introduction to Automata Theory, Languages, and Computation}.
2664: \newblock Addison-Wesley, 1979.
2665:
2666: \bibitem{kp96}
2667: Antoni Ko{\'s}cielski and Leszek Pacholski.
2668: \newblock Complexity of {M}akanin's algorithm.
2669: \newblock {\em Journal of the Association for Computing Machinery},
2670: 43(4):670--684, 1996.
2671: \newblock Preliminary version in {\em Proc.~of the 31st Annual IEEE Symposium
2672: on Foundations of Computer Science}, Los Alamitos, 1990, 824--829.
2673:
2674: \bibitem{kp98}
2675: Antoni Ko{\'s}cielski and Leszek Pacholski.
2676: \newblock {M}akanin's algorithm is not primitive recursive.
2677: \newblock {\em Theoretical Computer Science}, 191:145--156, 1998.
2678:
2679: \bibitem{koz77}
2680: Dexter Kozen.
2681: \newblock Lower bounds for natural proof systems.
2682: \newblock In {\em Proc.~of the 18th Ann.~Symp. on Foundations of Computer
2683: Science, FOCS~77}, pages 254--266, Providence, Rhode Island, 1977. IEEE
2684: Computer Society Press.
2685:
2686: \bibitem{Lothaire83}
2687: M.~Lothaire.
2688: \newblock {\em Combinatorics on Words}, volume~17 of {\em Encyclopaedia of
2689: Mathematics and its Applications}.
2690: \newblock Addison Wesley, 1983.
2691: \newblock Reprinted by {\em Cambridge University Press}, 1997.
2692:
2693: \bibitem{mak77}
2694: Gennadi{\'{\i}}~Semyonovich Makanin.
2695: \newblock The problem of solvability of equations in a free semigroup.
2696: \newblock {\em Math. Sbornik}, 103:147--236, 1977.
2697: \newblock English transl. in Math. USSR Sbornik 32 (1977).
2698:
2699: \bibitem{mak83a}
2700: Gennadi{\'{\i}}~Semyonovich Makanin.
2701: \newblock Equations in a free group.
2702: \newblock {\em Izv. Akad. Nauk SSR}, Ser. Math. 46:1199--1273, 1983.
2703: \newblock English transl. in Math. USSR Izv. 21 (1983).
2704:
2705: \bibitem{mak84}
2706: Gennadi{\'{\i}}~Semyonovich Makanin.
2707: \newblock Decidability of the universal and positive theories of a free group.
2708: \newblock {\em Izv. Akad. Nauk SSSR}, Ser. Mat. 48:735--749, 1984.
2709: \newblock In Russian; English translation in: {\em Math.~USSR Izvestija, 25},
2710: 75--88, 1985.
2711:
2712: \bibitem{marchenkov82}
2713: S.~S. Marchenkov.
2714: \newblock Unsolvability of positive $\forall\exists$-theory of a free
2715: semi-group.
2716: \newblock {\em Sib. Mat. Zh.}, 23(1):196--198, 1982.
2717: \newblock In Russian.
2718:
2719: \bibitem{mar77}
2720: George Markowsky.
2721: \newblock Bounds on the index and period of a binary relation on a finite set.
2722: \newblock {\em Semigroup Forum}, 13:253--259, 1977.
2723:
2724: \bibitem{merz66}
2725: {\Yu}ri~I. Merzlyakov.
2726: \newblock Positive formulae over free groups.
2727: \newblock {\em ALgebra i Logika}, 5(4):25--42, 1966.
2728: \newblock English translation.
2729:
2730: \bibitem{pap94}
2731: Christos~H. Papadimitriou.
2732: \newblock {\em Computatational Complexity}.
2733: \newblock Addison Wesley, 1994.
2734:
2735: \bibitem{ESA::Plandowski1994}
2736: Wojciech Plandowski.
2737: \newblock Testing equivalence of morphisms on context-free languages.
2738: \newblock In Jan van Leeuwen, editor, {\em Algorithms---{ESA}~'94, Second
2739: Annual European Symposium}, volume 855 of {\em Lecture Notes in Computer
2740: Science}, pages 460--470, Utrecht, The Netherlands, 1994. Springer.
2741:
2742: \bibitem{pla99stoc}
2743: Wojciech Plandowski.
2744: \newblock Satisfiability of word equations with constants is in {NEXPTIME}.
2745: \newblock In {\em Proceedings 31st Annual ACM Symposium on Theory of Computing,
2746: STOC'99}, pages 721--725. ACM Press, 1999.
2747:
2748: \bibitem{pla99focs}
2749: Wojciech Plandowski.
2750: \newblock Satisfiability of word equations with constants is in {PSPACE}.
2751: \newblock In {\em Proc.~of the 40th Ann.~Symp. on Foundations of Computer
2752: Science, FOCS~99}, pages 495--500. IEEE Computer Society Press, 1999.
2753:
2754: \bibitem{pr98icalp}
2755: Wojciech Plandowski and Wojciech Rytter.
2756: \newblock Application of {L}empel-{Z}iv encodings to the solution of word
2757: equations.
2758: \newblock In Kim~G. Larsen et~al., editors, {\em Proc. 25th ICALP (ICALP'98),
2759: Aalborg (Denmark) 1998}, number 1443 in Lecture Notes in Computer Science,
2760: pages 731--742. Springer, 1998.
2761:
2762: \bibitem{raz84}
2763: Alexander~A. Razborov.
2764: \newblock On systems of equations in a free group.
2765: \newblock {\em Izv. Akad. Nauk SSSR}, Ser. Mat. 48:779--832, 1984.
2766: \newblock In Russian; English translation in: {\em Math.~USSR Izvestija, 25},
2767: 115--162, 1985.
2768:
2769: \bibitem{sch91}
2770: Klaus~U. Schulz.
2771: \newblock {M}akanin's algorithm for word equations --- {T}wo improvements and a
2772: generalization.
2773: \newblock In Klaus~U. Schulz, editor, {\em Word Equations and Related Topics},
2774: number 572 in Lecture Notes in Computer Science, pages 85--150. Springer,
2775: 1991.
2776:
2777: \bibitem{gs78}
2778: Joachim von~zur Gathen and Malte Sieveking.
2779: \newblock A bound on solutions of linear integer equalities and inequalities.
2780: \newblock {\em Proc. Amer. Math. Soc.}, 72(1):155--158, october 1978.
2781:
2782: \end{thebibliography}
2783:
2784: \end{document}
2785:
2786:
2787:
2788: