Solutions to twisted word equations and equations in virtually free groups
Volker Diekert, Murray Elder

TL;DR
This paper proves that the set of solutions to twisted word equations in virtually free groups can be described as an EDT0L language and computed within PSPACE, extending previous work with concrete complexity bounds.
Contribution
It establishes that all solutions form an EDT0L language and provides PSPACE algorithms for solving and analyzing these equations, improving upon prior results with explicit complexity bounds.
Findings
Solutions form an EDT0L language
Solution set decision problems are in PSPACE
Algorithms can be implemented in NSPACE(n^2 log n) for certain cases
Abstract
It is well known that the problem solving equations in virtually free groups can be reduced to the problem of solving twisted word equations with regular constraints over free monoids with involution. In this paper we prove that the set of all solutions of a twisted word equation is an EDT0L language whose specification can be computed in . Within the same complexity bound we can decide whether the solution set is empty, finite, or infinite. In the second part of the paper we apply the results for twisted equations to obtain in an EDT0L description of the solution set of equations with rational constraints for finitely generated virtually free groups in standard normal forms with respect to a natural set of generators. If the rational constraints are given by a homomorphism into a fixed (or "small enough") finite monoid, then our algorithms can be…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Solutions to twisted word equations and equations in virtually free groups
Volker Diekert
Institut für Formale Methoden der Informatik, Universität Stuttgart, Universitätsstr. 38, D-70569 Stuttgart, Germany
and
Murray Elder
School of Mathematical and Physical Sciences, University of Technology Sydney, Broadway NSW 2007, Australia
(Date: March 7, 2024)
Abstract.
It is well known that the problem solving equations in virtually free groups can be reduced to the problem of solving twisted word equations with regular constraints over free monoids with involution. In this paper we prove that the set of all solutions of a twisted word equation is an EDT0L language whose specification can be computed in . Within the same complexity bound we can decide whether the solution set is empty, finite, or infinite.
In the second part of the paper we apply the results for twisted equations to obtain in an EDT0L description of the solution set of equations with rational constraints for finitely generated virtually free groups in standard normal forms with respect to a natural set of generators. If the rational constraints are given by a homomorphism into a fixed (or “small enough”) finite monoid, then our algorithms can be implemented in , that is, in quasi-quadratic nondeterministic space.
Our results generalize the work by Lohrey and Sénizergues (ICALP 2006) and Dahmani and Guirardel (J. of Topology 2010) with respect to both complexity and expressive power. Neither paper gave any concrete complexity bound and the results in these papers are stated for subsets of solutions only, whereas our results concern all solutions.
2010 Mathematics Subject Classification: 03D05, 20F65, 20F70, 68Q25, 68Q45.
Keywords: Equation in a virtually free group, twisted equation, EDT0L language, .
Research supported by Australian Research Council (ARC) Project DP 160100486 and German Research Foundation (DFG) Project DI 435/7-1.
Introduction
For a given semigroup the decision problem WordEquation is the following: on input two words and in variables together with letters from a generating set , decide whether or not there exists a substitution of variables by elements in which yields a true identity in . Here, is extended by for all .
In a seminal paper [36] Makanin showed that WordEquation is decidable for free semigroups. The first complexity estimation of the problem was a tower of several exponential functions, but this dropped down to by Plandowski [44] using compression. The insight that long solutions of word equations can be efficiently compressed is due to [45] which also led to the still standing conjecture that WordEquation is -complete for free semigroups (and free groups). Until 2013 the known decidability proofs for solving word equations were long and technical with an accompanied reputation for being difficult. This changed drastically when Jeż applied his recompression technique: he presented an algorithm to solve word equations [26]111In [27] Jeż improved the complexity to .. Actually his method achieves more: it describes all solutions, copes with rational constraints (which is essential in applications), it extends to free groups, and to free monoids with involution [11]. Refining Jeż’s method, Ciobanu and the present authors showed that the full solution set of a given word equation over a free monoid with involution with rational constraints is EDT0L [5]. As a consequence, the same is true in free monoids without involution and for free groups where the constraints are used to ensure that solutions are given by reduced words. Previously this was only known for quadratic word equations [17]. EDT0L languages are defined by a certain type of Lindenmayer system. There is a vast literature on Lindenmayer systems, see [50], but all we need here is that an EDT0L language is specified by a nondeterministic finite automaton accepting endomorphisms over a free monoid and by some initial word. Applying the set of accepted endomorphisms to the initial word yields the language.
The original motivation for [5] was to prove that the full solution set in reduced words of equations in free groups is an indexed language, a problem which was open at that time [18, 25]. However, the result in [5] is stronger since EDT0L forms a strict subclass of indexed languages [15].
Transfer results as in [22, 5] from words to free groups have a long history. In the 1980s Makanin showed that the existential and positive theories of free groups are decidable [37]. In 1987 Razborov gave a description of all solutions for an equation in a free group via “Makanin-Razborov” diagrams [46, 47] which formed a cornerstone in the work of Kharlampovich/Myasnikov [30] and Sela [52] on the positive solution of Tarski’s conjectures about the elementary theory in free groups.
The motivation for the present paper is along this line. We show that given a finitely generated virtually free group there is an algorithm which produces for a given equation with (small) rational constraints an effective description of an EDT0L language which describes the solution set in standard normal forms over a natural set of generators. Moreover, the same complexity is enough to decide whether the solution set is empty, finite or infinite. No algorithm, in fact no concrete complexity bound was known for deciding emptiness before.
In this paper, we define an algorithm
to be a partially defined single-valued function computed by a nondeterministic Turing machine consisting of three tapes: a one-way-read-only input tape, a two-way-read-write work tape, and a one-way-write-only output tape. If the length of the word written on the input tape is , the work tape is restricted to having length . If the machine halts on input at some point, then the contents on the output tape satisfies . In general such a device might specify a partially defined multi-valued function, where several outputs are possible from the same input. However, in our case, we require that the output is unique. The domain of the partially defined function computed by the machine is the halting set of the machine, and for each in the domain there is a single output . This is the standard definition of a nondeterministic transducer which computes partially defined single-valued function. For nondeterministic polynomial time, formal definitions go back to [4]; see also [53, 54]. It is clear that this formalism applies to other nondeterministic complexity classes as well. Every transducer can be simulated by a deterministic transducer using at most working space (Savitch’s Theorem), and also by a deterministic Turing machine which uses a time bound in , see [43] for more details. Thus, every algorithm can be implemented such that it runs in deterministic singly exponential time .
Several remarks are in order here, which point to some additional difficulties in our framework. First, in general virtually free groups have torsion, which is a serious obstacle to applying the known techniques. The reason to study virtually free groups is motivated by the ubiquitous presence of word hyperbolic groups [20]. Solving equations in torsion-free hyperbolic groups reduces to solving equations in free groups [49], but solving equations in word hyperbolic groups with torsion reduces to solving equations in virtually free groups which in turn reduces to solving twisted word equations with rational constraints [7]. The question of whether solving twisted word equations is decidable was asked by Makanin ([38] Problem 10.26(b)). It was solved in [7], thereby showing that the set of solvable equations over a f.g. virtually free group is decidable. This result was also independently shown by Lohrey and Sénizergues [35]. (Actually, [35] proves a more general transfer result.) What is in common: both papers are based on [10] and use explicitly ([35] only implicitly due to [10]) the so-called “exponent of periodicity”. Because of this neither paper describes all solutions, nor gives any concrete complexity bounds.
The result for virtually free groups is obtained by a reduction to the problem to describe the solution sets of twisted word equations with regular constraints, following standard techniques. So, the main new contribution is our approach to solving twisted word equations. We follow the approach in [5] to define a sound and complete algorithm to produce an NFA describing all solutions, however in the setting of twisted equations the technical details are quite far from previous methods. For example, for readers familiar with previous methods, in twisted equations it does not make sense to “uncross” pairs where , are different letters because once all pairs are uncrossed the twisting may produce new crossing pairs , uncrossing them leads to new crossing pairs etc. Thus, our underlying method is quite different from the original recompression due to Jeż.
The class of f.g. virtually free groups appears in many different ways. For example, a fundamental theorem of Muller and Schupp (relying originally on [14]) says that a f.g. group is virtually free if and only if it is context-free [40]. This means that, given any set of monoid generators , the set of words which represent forms a context-free language. Other characterizations include: (1) fundamental groups of finite graphs of finite groups [29], (2) f.g. groups having a Cayley graph with finite treewidth [32], (3) universal groups of finite pregroups [48], (4) groups having a finite presentation by some geodesic string rewriting system [19], and (5) f.g. groups having a Cayley graph with decidable monadic second-order theory [32]. Proofs for the most important equivalences are in [13]. The transformations are effective. For example, starting from a context-free grammar for the word problem, we can construct a representation as a fundamental group of finite graphs of finite groups. However, the finite graphs of finite groups can be much larger than the size of the context-free grammar: the result in [55] showed a primitive recursive bound on the blow-up. It was only very recently that Sénizergues and Weiß showed in [57] that the blow-up can be bounded by a doubly exponential function.
What we use here is another characterization which is proved in [13, Sec. 2.4.5]. It follows rather easily from Bass-Serre theory [58] and the representation of a f.g. virtually free group as a fundamental group of finite graphs of finite groups. The characterization says that a f.g. group is virtually free if and only if it has an effective embedding into a semi-direct product of a free group with basis by a finite group which acts by permutations on the symmetric set . (The precise statement is in Prop. 14.7.) Taking this characterization as a black box, no knowledge in Bass-Serre theory is required to understand our results.
An extended abstract of a preliminary version of this paper was presented at the conference ICALP 2017, Warsaw (Poland), 10-14 July 2017 [9]. Ciobanu and the second author have now extended the results of the present paper to show solutions to equations in any hyperbolic group are EDT0L with description in [6].
1. Organization of the paper
1.1. The overall structure
The paper has two main and separate parts. In a first part we deal the following algorithmic problem. The input is a system of twisted word equations with regular constraints over a free monoid (with involution) . The “twist” comes from a finite group acting on . We present a algorithm which constructs an NFA which gives a description of the set of all solutions as an EDT0L language. Structural properties of the NFA tell us whether the set of all solutions is empty, finite, or infinite. Precise complexity bounds are discussed in Sect. 4.2, and under certain assumptions on the size of the regular constraints, we prove the entire algorithm can be done in where denotes the input size of , and when and are constants, this becomes quasi-quadratic nondeterministic space .
In a second part we apply our results on twisted word equations to the existential theory of equations with rational constraints over finitely generated virtually free groups. From the algorithmic viewpoint we deal with a non-uniform complexity where the virtually free group is not part of the input. (This allows us to assume that is embedded into a semi-direct product of a free group by a finite group , where the rank of and the size of are constants.) The input is a Boolean formula in free variables over equations and rational constraints for the solution specified by NFAs which accepts subsets of . The output is a specification of the set of all solutions in standard normal forms for as an EDT0L language. The proof is a reduction to the setting in the first part. The result is in the same overall complexity as in the first part when taking into account that , and are not part of the input.
In the final section we perform this reduction explicitly for the special linear group (without relying on any knowledge of Bass-Serre theory) starting with the well-known classical fact that can be embedded in semi-direct product of a free group of rank (its commutator subgroup) by the finite cyclic group . A priori, there could be an exponential blow-up in the complexity due to fact that we use matrices and not a word representation when describing equations over . However, there is no such blow-up thanks to work of Gurevich and Schupp [21].
1.2. Technical details
We assume that the reader is familiar with some basic facts in combinatorics on words, formal languages and finite automata, and complexity theory. Apart from that (and the promise that a finitely generated (f.g. for short) virtually free group admits an embedding into a certain semi-direct product of a free group by a finite group ) the paper is self-contained. In principle, it is not necessary that the reader has ever heard of Makanin, word equations, or any method to solve them before. The paper uses various technical tools where the authors would have preferred to give references in the literature rather than lengthy and somewhat pedestrian constructions, but failed to find the appropriate references.
The heart of the paper is Jeż’s compression method in the framework of twisted equations: Sect. 10 and Sect. 11. The adaption to the twisted setting is far from trivial and quite different from the original method in [26] or its extension to free groups as in [11] or [5]. Therefore to understand Sections 10 and 11 is the most demanding part when reading the paper.
Many of the technicalities surrounding complexity can be overlooked if the reader is happy enough to replace the explicit complexity bounds by .
2. Preliminaries
We use standard notation. If and are sets, then means set inclusion, while means . By we denote the set of which are not in . By we mean the set of mappings from to , and denotes the power set of , that is, . We also view as a commutative and idempotent monoid.
denotes the Boolean semi-ring, (resp. ) denotes the semi-ring of natural numbers, (resp. the ring of integers). is also the free monoid and is the free group in one generator.
Monoids (resp. groups) will typically be denoted by and (resp. by and ). If the focus is on finite monoids (resp. finite groups), then we use the notation (resp. ). With a few exceptions (like or ) we denote the identity element in monoids by . A zero in a monoid is an element such that for all . If a zero exists, it is unique. Nontrivial groups cannot have a zero.
Let be a monoid and . We say that is a factor of if we can write for some . If we can write (resp. ), then we say that is a prefix (resp. suffix) of . If is a prefix of , then we also write .
2.1. Complexity
The -notation and complexity classes like , , , are defined as in standard textbooks ([24, 43]), see also page Introduction. We use a convention that . Throughout we use the well-known fact due to Immerman-Szelepcsényi that is closed under complementation. Note that any statement about complexity depends on how the input is given. A statement like “factorization is not known to be in ” makes sense only if the encoding of the problem and a notion of input size has been defined. If integers are encoded in unary, then, trivially, “factorization is in ” is true. Typically, inputs have various parameters. If certain parameters of the input are fixed, then with respect to the input size these parameters behave as constants. Still, for many problems it is more accurate to use parametrized inputs, where the input size is tuple of non-negative numbers: with . If is such a problem, then with respect to polynomial resource bounds we view as a one-parameter problem of input size . The notation is robust: every polynomial in is also a polynomial in for all . Throughout, we take care to define our input sizes (of systems of equations, or Boolean formulae, with regular constraints) in a natural way.
2.2. Sets and monoids with involution
An involution of a set is a bijection such that for all in the set. The identity map is an involution. A monoid with involution additionally has to satisfy . This implies and (in case there is a zero). If is a group, then it is a monoid with involution by taking for all . By default, we choose to be in groups.
A morphism between sets with involution is a mapping respecting the involution. A morphism between monoids with involution is a homomorphism such that . Note that every group homomorphism is a morphism of monoids with involution. The set of automorphisms on a set (or monoid) forms the group . For we say that is a -morphism if for all .
2.3. Group actions and -monoids
Recall that a group acts on a set (with involution) via a homomorphism . That is, defines a permutation with , (and ) for all and . Thus, every defines a permutation of (which respects the involution). The stabilizer of is the subgroup . Frequently, we also write as a synonym for . If acts on a monoid , then we additionally demand that every element of acts as an automorphism: . If is equipped with an involution, then we have . In the following we say that is an -monoid if it is a monoid with involution on which acts. A morphism between -monoids and is given by an -compatible morphism which is a homomorphism respecting for all and the action , and the involution, .
2.4. Free monoids with involution and an -action
By an alphabet we mean a finite set with involution. (Since the identity is an involution of this covers the case of monoids without a predefined involution.) The elements of are called letters (or symbols). By (by resp.) we denote the free monoid (free semigroup resp.) over . The elements of a free monoid are called words. The empty word in a free monoid is also denoted by as in other monoids. We have . The involution extends to : for a word with we let . The monoid is called the free monoid with involution over . If for all then is simply the word read from right-to-left. The length of word is denoted by , and counts how often a letter appears in .
If a group acts on , then acts on with by
[TABLE]
A letter is -visible in if is a factor of for some .
Sometimes it is useful to view a word of with as a labeled linear order as follows. We let be set of positions; and we label a position with the letter . For we denote by the interval . The labels of the interval define a factor
[TABLE]
An occurrence of a factor in is an interval such that . Typically, a factor has several occurrences. For a position we define its dual position by . The notion of duality extends to intervals with by . Thus, the set of intervals is a set with involution.
A word such that is called self-involuting, and for such we have .
2.5. Automata, rational and recognizable subsets in a monoid
For notation and results in the this subsection we refer to the classical textbook [16]. A regular language in finitely generated free monoids can be defined via a nondeterministic finite automaton or via recognizability using a homomorphism to a finite monoid, to mention just two possible definitions. We need the corresponding notions subsets for other monoids, too.
Let be any monoid (not necessarily equipped with an involution). A nondeterministic automaton over is a directed arc-labeled graph denoted as a tuple . The vertices of form the set of states, with subsets of initial and final states. We write if there are no states. The arcs are called transitions and they are labeled with elements of the monoid . We represent the set of transitions as a subset of . A transition labeled by is called an -transition. In pictures we draw a transition as . We say that is accepted by the automaton if there exists a path from some initial to some final state such that multiplying the labels together yields . This defines the accepted language .
Often we specify together with a set of generators or, more generally, together with homomorphism from the free monoid to . In that case, we may denote alternatively as where . This allows two natural interpretations of : first as the set of words obtained by reading as a shorthand for ; second as by identifying with . If the distinction is crucial, we write and . However, sometimes a sloppy notation is used. There will be however no risk of confusion.
A subautomaton of is an automaton such that , , , and .
An automaton is called trim if every state is on some path from an initial to a final state. For a trim automaton we have if and only if . Clearly, every automaton contains a trim subautomaton such that .
If the set of transitions is finite, then we call a nondeterministic finite automaton (or NFA for short). A subset is called rational if is accepted by some NFA over .
A subset is called recognizable if there is a homomorphism to a finite monoid such that . In case that is a finitely generated free monoid, the notion of rational and recognizable subsets coincide; so these subsets are also called regular. It follows rather easily that a monoid is finitely generated if and only if all recognizable subsets are rational [39]. Finite subsets are always rational, but finite subsets in a group are recognizable if and only if the group is finite.
2.6. From NFAs to Boolean matrices
Nondeterministic finite automata encode regular languages in a concise and natural way. It is convenient to work in an algebraic framework with recognizing morphisms, too. Let us recall a well-known and classical construction.
Let be any NFA with states. Then we can assume that , and we represent transitions as a mapping to Boolean matrices as follows. For each letter we define a matrix by
[TABLE]
We obtain a homomorphism such that for all we have
[TABLE]
Example 2.1**.**
Let be an alphabet (with involution) and be a subgroup of automorphisms. The set of words having a factor for some is regular and is invariant under the action of . Let be the complement: it is the set of reduced words. The set is in canonical bijection with the group . The language is accepted by an NFA (actually a DFA) with states. Hence, recognizes them where .
The size of is , but there is a much smaller monoid which recognizes and hence , too. The elements of are , [math], and the pairs in . The elements and [math] act as the neutral element and a zero, respectively. The multiplication for the other elements is given by if and , otherwise. The involution is given by . In effect, “remembers” the first and last letters of elements in . A pair switches to [math] once a factor is recorded.
It is an -monoid by the natural action of induced by the action of on . Consider the morphism of -monoids which is defined by . Then we have and . The size of is therefore . Therefore each element in can be specified by at most bits.
3. Regular languages in presence of an involution and an -action
The application of this section is stated precisely in Prop. 3.2. We give a construction which allows us to handle regular constraints for twisted word equations using morphisms to finite -monoids.
We proceed in two steps. The first step forces homomorphisms to respect the involution. This part is from the arXiv version of [5] which was inspired by [10]. We repeat that construction. Let be any monoid. We define its dual monoid to use the same set , but is equipped with a new multiplication . In order to indicate whether we view an element in the monoid or , we use a flag: for we write to indicate the same element in . Thus, we can suppress the symbol and we simply write . The notation is intended to mimic transposition in matrix calculus, where the dual operation is just the transpose. Similarly, we write instead of which is true for the identity matrix as well. The direct product becomes a monoid with involution by letting . Indeed,
[TABLE]
The following observations are immediate.
- •
If is finite then is finite, too.
- •
We can embed into by a homomorphism defined by . Note that if denotes the projection onto the first component, then .
- •
If is a monoid with involution and is a homomorphism of monoids, then we can lift uniquely to a morphism of monoids with involution such that we have . Indeed, it is sufficient and necessary to define .
Example 3.1** ([10]).**
Let . Then is a submonoid of the set of -Boolean matrices:
[TABLE]
In the line above and are the transposed matrices.
Now, we switch to the new part of our construction. For readers familiar with wreath products it might be helpful to say that the following is a wreath product construction. Let be a monoid with involution. Consider the direct product , which is the set of maps from to . We denote the elements of by tuples with the interpretation that is mapped to . It is a monoid by pointwise multiplication with involution . The monoid embeds into by sending to the constant map . We let act on by
[TABLE]
Now, let be an -monoid with involution and let be a morphism of monoids with involution, then we extend it to by
[TABLE]
The homomorphism respects the involution since
[TABLE]
and it respects the action of since
[TABLE]
Moreover, factorizes though because implies where .
If we start with a homomorphism from an -monoid with involution to a monoid without involution, then means the morphism ; and is a shorthand for . Thus, the constructions above yield the commutative diagram as in Fig. 1. In that figure is a homomorphism, is a morphism of monoids with involution, and is an -compatible morphism. As a direct consequence we obtain the following proposition. Recall that an -monoid is, by definition, a monoid with involution.
Proposition 3.2**.**
Let be a finite group that acts on a finite alphabet ; and hence via a length and involution preserving action on . Then all recognizable subsets of can be recognized by some -compatible morphism to a finite -monoid. More precisely, let be a homomorphism to a finite monoid; and for some . Then we have where and .
3.1. Stabilizers
Let be a finite group acting on an alphabet via a homomorphism . We assume that is given by its multiplication table. The table can be stored with bits. We also need a way to represent the action of and the stabilizer subgroups of . The action is recorded by writing down for each the element as a permutation of . To do this, we write as a set of pairs . Thus, the action of on can be stored with bits.
For a word we denote by its stabilizer:
[TABLE]
stabilizer are subgroups; and the set of subgroups of the form form a commutative monoid where the operation is intersection, the identity element is , and the involution is the identity. Indeed, we have
[TABLE]
[TABLE]
and
[TABLE]
for all , . In particular, acts on by conjugation, and is therefore an -monoid. Let denote the set of all subgroups of , then yields a canonical surjective morphism
[TABLE]
A basic test is to answer “?”. This is easy: for with we check one after another that for . This enables an efficient test to decide whether or not . For each one after another we test whether implies . In particular, we can answer “?”.
Lemma 3.3**.**
We have
Proof.
For each and we either have or because . So, if they are not equal, then their intersection is a subgroup which has index at least in . ∎
The idea is therefore to use words of length at most to represent stabilizers and to perform the calculations for stabilizers on these words. The representation is not unique, but this does not matter for our application.
A main task is to compute a word of length at most such that (when and satisfy ). This can be done efficiently according to the following lemma.
Lemma 3.4**.**
Every element in the commutative monoid of stabilizers can be represented by a word in of length at most , thus with at most bits. Using this representation, multiplication (that is, intersection) and computing the -action (that is, conjugation), can be done in space .
Proof.
Let . We have to compute a word of length at most such that .
We run a loop for to . At each step we have computed a word such that with the invariant (initially we let ). There are exactly three mutually disjoint cases.
- (1)
If then we let . 2. (2)
If , then we let . 3. (3)
If and are incomparable with respect to containment, then we let .
Each case keeps the invariant because, by induction, . ∎
Remark 3.5**.**
The reader can easily check that our computation of a word with yields a word of pairwise different letters. So, we could actually put a bound on its length.
3.2. --monoids
In the following denotes a finite group and denotes a finite -monoid. Let be a set (resp. be a monoid) with involution and
[TABLE]
be a morphism. We say (together with ) is an --alphabet (resp. an --monoid) if acts on such that . For example, the identity map on makes itself to an --monoid.
A morphism between --monoids is an -compatible morphism such that . Thus, if is an --monoid and is a monoid with involution where acts, then every -compatible morphism turns into an --monoid where is uniquely defined by the equation . The use of --monoids is natural in our setting: the -action is due to a group action on letters, and the finite monoid is used for the specification of rational constraints. It is clear that the specification of constraints has to be compatible with the group action.
3.3. Free --monoids and types
Let and be two disjoint --alphabets. We call the alphabet of constants and the set of twisted variables. The free monoid with involution becomes an --monoid where is induced by .
[TABLE]
By we denote a finite homogeneous relation. Here as usual, a relation is called homogeneous if implies . If then we also say that is a defining relation because the algebraic object we are interested in is the quotient monoid
[TABLE]
We need more structure of this quotient monoid; in particular, should induce a morphism of --monoids. Actually we wish more, therefore we impose the following technical restrictions on ; and then we call a type (and for a variable we also define the type of denoted below).
- (1)
implies , , and for all , even if these relations are not listed in the specification of . 2. (2)
If a (twisted) variable appears in (that is for some ), then we call typed. For a typed variable we require that there is a unique primitive word222Recall that is primitive if and only if it cannot be written as with . such that . We define , and say that is the type of . 3. (3)
For we allow exactly three possibilities:
- (i)
with . 2. (ii)
for variables . 3. (iii)
where and are typed variables such that .
It is convenient to choose a subset which is closed under the involution such that every has the form for some and . In the following, by a variable we typically mean and thus, every twisted variable can be written as for some and . We assume for all variables. Having chosen and we denote by the following quotient monoid (and an --monoid with type ):
[TABLE]
Point (1) from above makes sure that one can extend the involution, the morphism and the action of to the quotient . The homogeneity condition for makes it possible to solve the uniform word problem in in nondeterministic quasi-linear space:
Lemma 3.6**.**
There is an algorithm which performs the following task. The input is an alphabet , a homogeneous relation , and two words such that
[TABLE]
The output is “yes” if in the quotient monoid and “no” otherwise.
Proof.
If in , then nondeterministically we can apply rewriting rules from (which preserve length) to until we see in the free monoid . We get the “no” answer because is closed under complementation by the theorem of Immerman-Szelepcsényi, see for example [43]. ∎
Using Lem. 3.6 we represent elements in by words over . For we obtain . By we denote the --monoid submonoid with type which is generated by . In particular, . If , then is a free submonoid of . If acts without fixed points on , then we identify and the action becomes . Later we will write typed variables using a special bracket notation . For complexity issues we will only allow which satisfy where is specified in (2) below.
3.4. EDT0L languages and relations
The acronym EDT0L refers to Extended, Deterministic, Table, 0 interaction, and Lindenmayer. See the handbook [51] for the many results about L-systems. Let be an alphabet. A subset in a -fold direct product is called a EDT0L relation if there is some (extended) alphabet with such that and a rational set of endomorphisms over such that
[TABLE]
The classical situation refers to . In that case we speak about an EDT0L language; and our definition uses a characterization of EDT0L languages due to [1]. The connection is as follows. Let \$$ be a symbol which is not in AL\subseteq A^{}\times\cdots\times A^{}\left{w_{1}$w_{2}\cdots$w_{k}\mathrel{\left|\vphantom{w_{1}$w_{2}\cdots$w_{k}}\vphantom{(w_{1},\ldots,w_{k})\in L}\right.}(w_{1},\ldots,w_{k})\in L\right}A\cup\left{\mathinner{$}\right}$. It should also be noted that the class of EDT0L languages coincides with the class of HDT[math]L languages ([51, Thm. 2.6]).
We say is an effective EDT0L relation if there is an effective description of an NFA with transitions labeled by “deterministic tables” of pairs (encoding the endomorphism which maps to (and to ))333Without restriction we can assume each transition is labeled by an endomorphism which changes at most one pair of letters . and letters such that if and only if there is some such that .
4. Twisted word equations
4.1. The initial setting
We begin with a nonempty alphabet of constants , and a list of variables (as always, both with involution) and a finite group where acts on via a homomorphism . In particular, . As above, acts on by . For and we also use the notation . Hence, we may represent elements in by words in . We abbreviate as for . By we mean a homomorphism which respects the involution and the action of . Thus is, via , an --monoid. Assume that has been extended to a mapping such that , then extends to a morphism of --monoids by . Initially we work over free monoids.
Definition 4.1**.**
A system of twisted word equations with regular constraints over and is given by the following data:
- •
A list of variables such that .
- •
The set of twisted variables becomes .
- •
A set of pairs where .
- •
A morphism of -monoids, with finite.
A solution of is a morphism of sets with involution which is (uniquely) extended to an -morphism of --monoids such that
- •
* for all pairs .*
- •
* for all variables. Hence, .*
As usual, a pair representing a twisted equation is simply written as .
Example 4.2**.**
Let , defined by , , , , , , and (for simplicity) for all . A pictorial representation of the example is shown in Fig. 2. The reader is invited to verify that one possible solution is , and a second solution is .
If is a solution of we also say that solves . For the full solution set of is defined as
[TABLE]
4.2. The main result on twisted word equations
Our main result shows that is an EDT0L language, for which we can compute an effective description in polynomial space. In order to measure complexities accurately, we need a precise notion of input size. Let be a system of twisted word equations with regular constraints over and according to Def. 4.1.
We define the size of using two parameters and . Thus, the size is the pair . The first parameter ignores the size of the finite monoid . It is the main parameter as we don’t want that the complexity due to constraints dominates the overall complexity. The second parameter measures separately the number of additional bits for handling the constraints. We begin by defining . Let
[TABLE]
Recall that is the number of variables, is the number of equations , and denotes a finite group acting on and hence on , too. We are interested in a situation only where and .
The finite monoid is also part of the input. We measure the size relative to . Let be any finite -monoid and be a number such that elements of can be encoded by a number of bits which is at most
[TABLE]
Moreover, using this specification, monoid computations, like computing the involution, the multiplication of two elements, and the action by , can be performed on a Turing machine in space . We let
[TABLE]
There are examples where the monoid (which appears in ) is polynomially bounded in and still . However, if becomes a polynomial in , then we need to consider separately for a finer analysis below .
An -monoid is called small with respect to if . The finite monoid recognizing reduced words (those without factors for ) is small with respect to , see Ex. 2.1. Being small is no restriction for the computability of the representation of the full solution set as an EDT0L relation – we can always add trivial equations until becomes small with respect to . Another example of a small monoid is the finite monoid of stabilizers. Its size depends on and , but still it is small due to Lem. 3.4.
Now, during the process we might wish to use direct products of (small) monoids. For that the parameter behaves nicely:
[TABLE]
Indeed, given we can use the first bits to encode and the last bits to encode . The operations on can be done component wise. In particular, a direct product of small monoids remains small.
We are ready to state our main result which gives as an upper bound for the complexity and a quasi-quadratic space bound if is small.
Theorem 4.3**.**
There is an algorithm which performs the following task. It takes as input a system of twisted word equations with regular constraints. The system use a set of constants , a set of variables , and the regular constraint is given by a morphism . The output is:
- •
an extended alphabet of size ;
- •
distinguished letters for each variable ;
- •
a trim NFA accepting a rational set of -morphisms such that
[TABLE]
The algorithm stores intermediate equations with a length bound in . Moreover, if and only if ; and if and only if doesn’t contain any directed cycle.
Let us comment on the rather complicated space bound
[TABLE]
which appears in the statement of the theorem. First, since and , we can encode all letters by bits. Second, the -value for the constraints changes dynamically: it is a priori not fixed for the extended alphabet . So, it is enough to store the -value for each symbol which appears in intermediate equations. The length bound on intermediate equations is in . Each -value is an element in , which requires, by definition, bits for the encoding. Together, we need bits to encode intermediate equations,
Corollary 4.4**.**
Let be a system of twisted word equations with regular constraints in variables . Then is an effective EDT0L relation.
Proof.
This is a formal consequence of Thm. 4.3. ∎
Sections 5 through 12 are devoted to the proof of Thm. 4.3. The theorem implies that we can decide in (hence, in deterministic singly exponential time) whether is solvable and whether or not there are only finitely many solutions. The decision problem of whether a word equation with regular constraints has a solution is known to be -hard by [31] because the intersection problem of regular languages is a special case. In our setting, if the finite monoid is small, then the best known lower bound to date is -hardness: it is the lower bound for deciding whether or not a linear Diophantine system over has a solution [24].
5. Preparation
We begin the proof of Thm. 4.3 with some technical preparations. Sections 5.1–5.3 concern some reductions, and could easily be skipped in a first reading of the paper. These sections yield a reduction to the situation as stated in beginning of Sect. 5.4. We invite the reader to jump directly to Sect. 5.4 and to read the parts in between only when necessary.
5.1. Reducing to faithful actions
Recall that the action of on is given by a homomorphism . We don’t require that is injective because in some natural examples this is not the case, see Sect. 15. On the other hand it is enough to prove Thm. 4.3 in the case where is actually a subgroup of . Let us show how the reduction works. The principal idea is to replace by where is the kernel of .
If is any -monoid, then the action of induces an action of on only if for all and all we have . In this case becomes an monoid: the action is well-defined for all . By definition of , the free monoid is therefore an -monoid. Inspecting the statement in Thm. 4.3, there are two problems: the induced action of on the finite monoid is not trivial, in general. Moreover, the group acts freely on the set of variables , so there is no induced action of on this set unless is trivial. We address and solve both problems.
Let us begin with the -monoid , then it has a largest -invariant submonoid where acts trivially. It is the submonoid of -invariant elements:
[TABLE]
The image is a submonoid of , since for all and all we have . However, the statement in Thm. 4.3 doesn’t require that takes values in . Let us show that is not solvable if there is some variable such that . Indeed, assume the contrary that there is a solution such that . Then there is some such that
[TABLE]
which is a contradiction. We have because acts trivially on .
Thus, as a first procedure in the proof of Thm. 4.3 we check that for all (and therefore for all ). The test runs over all and for each checks the following implication:
[TABLE]
If the check is positive then for all . If the check fails then we output that is not solvable by defining . We can perform the test within our given space bound by definition of .
After the test, we may assume that maps to , and we replace by . We can use the same bit encoding for elements in as we did for , but if we have to guess an element in , we perform the test (6). Thus, the parameter is still valid.
In the second step we replace each variable by a fresh variable . Again, this doesn’t change since for every -compatible morphism and all we have
[TABLE]
We are done. We have shown the following statement.
Lemma 5.1**.**
It is enough to prove Thm. 4.3 under the additional assumption that is injective. This means we can assume that is a subgroup of .
5.2. Making the finite monoid larger
The aim in this section is to replace by a larger monoid, which additionally encodes information about stabilizers for all . Up to a constant factor we don’t change .
Let be the monoid of stabilizers, see Sect. 3.1. We define a morphism which maps a letter to and each variable to some where is any word of length at most by guessing . The -action on is inherited from the action on and the action on by conjugation. Moreover, guessing is equivalent to taking the union over finitely many cases, see (7). The union will give the same solutions we had before, and it will not introduce any new solutions.
The projection to the first component turns into an --monoid. Using we achieve the following:
- •
for all , is a pair where the second component is which is represented by a word of length at most such that .
The switch to has a price. By defining we restrict the set of possible solutions. The value fixes the stabilizer for a solution to be the subgroup . The number of choices (= nondeterministic guesses) to extend to is bounded by
[TABLE]
These choices result in a splitting the original system into that many subsystems. Splitting is fortunately no problem since EDT0L languages are closed under finite union by taking the unions of the corresponding NFAs.
At the end of this we rename as and as .
5.3. Introducing a zero to and a marker symbol to .
In the following it is convenient to have a special symbol , but we want to make sure no variable uses it, so we add [math] to our constraint monoid. We next embed our current into where [math] is a fresh symbol not included in and [math] acts as a zero in . We turn it into an -monoid by defining for all .
The monoid is an -submonoid of and, by a slight abuse of language, we denote by the induced mapping to the larger monoid as well:xt
[TABLE]
Without restriction (by adjusting constants if necessary) we may assume that doesn’t change the parameter . Using instead of doesn’t change because . Phrased differently, without restriction has a zero [math]; and .
At this point we to add the special symbol to . We let , and for all . So, from now on we assume that . Since we did not change for any variable we are sure that for every solution to and every variable we have : the marker cannot appear in any solution.
5.4. Triangular systems
Due to the preceding subsections we henceforth make the following assumptions:
- •
is a subgroup of .
- •
There is some with and for all .
- •
The -monoid contains a zero [math] and for all we have
[TABLE]
- •
is a pair where the second component is the stabilizer which is represented by a word of length at most such that for all . Since and is in we have for all :
[TABLE]
Definition 5.2**.**
A twisted word equation is called triangular if contains at most two variables and at most one variable.
Following well-known methods (see for example [8]) we enlarge the set of variables to a larger set (using at most more variables) such that every equation becomes triangular in a more specific form: every equation has the form either or where and in both cases is a variable.
It therefore is enough to show Thm. 4.3 in the case where each each equation equals where and . Moreover, since is equivalent to we can restrict ourselves to the case that each is of the form . Due to additional variables, we work over a set of variables
[TABLE]
where and the first variables belong to the original system.
Hence, the starting point is a system of equations . The number of these triangular equations is at most , so we can ignore this blow-up. During the process we need a more general form, nontrivial triangular equations appear as where are words over constants. Whenever such an equation with appears, then necessarily and ; otherwise the equation is “unsolvable”. That is, in a nondeterministic implementation of our process, this branch never leads to an accepting state. In an implementation of the algorithm we would reject the branch immediately.
Finally, it is somewhat convenient to assume . We may achieve this for example by adding some dummy equations, and then .
5.5. Fixing more notation
During the process we enlarge the sets of constants and variables. We begin with two disjoint infinite alphabets with involution and and . All constants are drawn from and all variables are drawn from . We never write down all elements from or , just certain subsets which are needed in a specific situation. Later we will choose such that , but initially for our infinite automata and we do not impose any size restrictions.
Throughout we use following conventions and notation.
- •
There are distinguished letters which appear in Thm. 4.3.
- •
.
- •
unless we are at a final state (to be defined below, see Sect. 7.1.2).
- •
, and for all . If acts freely on , then we write , too. We view .
- •
The action of and the involution on extend those on .
- •
satisfies for .
- •
refer to letters in .
- •
refer to words in .
- •
refer to variables in .
- •
refer to words in .
These conventions hold everywhere unless explicitly stated otherwise. They also apply to primed symbols such as , etc. Throughout we also use the following.
Remark 5.3**.**
If we know for any , then we also know, by the representation of the second component in , a word of length at most such that . This enables for all an efficient test to check whether , see (8) above. Moreover, if we have with and we have to calculate as the product , then we need to find a word of length at most such that . We may assume that and are already given as and where of length at most . In order to compute we run the algorithm from the proof of Lem. 3.4.
5.6. The initial word equation
For technical reasons we encode the initial (triangular) system of twisted equations in variables where as a single word. Let and .
The initial equation is defined as:
[TABLE]
In particular, each appears in . Here:
[TABLE]
Note that if and only if for all .
5.7. Fixing the parameters , , and
Having defined we fix the following parameters by
[TABLE]
By our assumptions this implies . We have . Moreover, since , we have and . As a consequence:
[TABLE]
Note that the right-hand side in (11) coincides with the space bound we allow to store intermediate equations according to Thm. 4.3.
5.8. Extended equations and their solutions
The NFA over the monoid we will construct uses extended equations as states. The overall strategy is to remove variables from the equation until no variables remain. During the process we will enter a phase called -periodic compression repeatedly (which is the analogue of “block compression” for solving word equations in free groups). During each call of -periodic compression, each variable may create temporarily two new variables which will vanish before the end of that call. So at most variables are needed, including these additional (temporary) variables.
Definition 5.4**.**
An extended equation is a tuple , where and is an --monoid with type . Moreover, we require:
- (1)
* which can be written as a word in the form:*
[TABLE]
with , , and . 2. (2)
Given as above we call a local equation. 3. (3)
. 4. (4)
For every there exists some such that appears in . 5. (5)
We say is a standard state if first, , and second, all local equations are triangular. 6. (6)
If is a standard state, then . Moreover,
[TABLE] 7. (7)
If is any state, then (Thus, we can bound by right away.) 8. (8)
If variables are typed with and , then we have in the submonoid generated by .
Recall (Sect. 3.3) that if a variable is typed, then there is a primitive word such that .
Definition 5.5**.**
Let be an extended equation.
- •
A solution is a -morphism such that:
- –
**
- –
, whenever is typed and .
- •
An entire solution is a pair where is an -morphism and is a solution.
6. Twisted conjugacy and -periodic words
A key step in proving Thm. 4.3 is to solve a particular kind of a twisted equation: conjugacy. Let . An easy exercise in combinatorics on words [23] yields:
[TABLE]
This fact is crucial in Makanin’s classical approach [36] to solve (untwisted) word equations. Here, we need a variant of (12) in the twisted environment. We say that words are twisted conjugate if there are and such that . We also say that is the offset of the conjugacy. A twisted conjugacy equation is a (non-triangular) twisted equation of the form
[TABLE]
Proposition 6.1**.**
Let be a solution of the twisted equation (13) such that the offset satisfies . Then there are words , and with such that and
[TABLE]
Proof.
Let and . Since the word is a proper nonempty prefix of . If , then is a prefix of , and so on. Thus, is a prefix of a word for some . Next, observe that for every word . Thus,
[TABLE]
where , and the suffix of is where the pattern runs out, as illustrated in Fig. 3. We then have . Hence, the nonempty word and the length define a unique factorization , integers and such that has the desired form above. ∎
A word is called primitive if it cannot be written as with . In particular, the empty word is not primitive. It is well known (and easy to see) that a nonempty word is if and only if cannot be written as with and .
Let be nonempty words. We say that has period if is a prefix of . In other words, if with , then for all . A word may have several periods, for example has periods . If is the least period of , then and we can choose to be primitive such that . For example, is a primitive prefix and .
Corollary 6.2**.**
Let , , and be words with and . If we have , then has a period of at most .
Moreover, let be any factorization with . Then every letter occurring in satisfies for some and some letter occurring in .
Proof.
By Prop. 6.1 we have
[TABLE]
where for all . Hence, has a period
[TABLE]
For the second claim, if with then is a factor of for some . If we write , then any letter in satisfies . Let so that is a letter in , then for some . ∎
Definition 6.3**.**
We say that a word is -periodic if it has some period of length at most . A -periodic word is called long -periodic if , and very long -periodic if .
For example, is 4-periodic but not long 4-periodic. An important property of -periodic words is the following.
Lemma 6.4**.**
Let be a -periodic word and such that are primitive , , , and . Then , , and .
Proof.
The assertion is clear for . Hence we may assume that is a proper prefix of . Since we conclude . Since , and we see . Thus occurs as a factor inside : we have for some . Since , this contradicts the primitivity of . ∎
Let be a prefix (resp. factor, resp. suffix) of some nonempty word . We say that is a maximal -periodic prefix (resp. factor, resp. suffix) in if we cannot extend the occurrence of the factor inside by any letter to the right or left, to see a -periodic word.
7. The ambient infinite automaton
The states of the NFA (we are aiming for in Thm. 4.3) are extended equations and transitions are certain labeled arcs between states which modify the extended equations. Before we construct let us define an infinite automaton . It will contain as a finite subautomaton. We show that is sound: this means in the notation of Thm. 4.3
[TABLE]
This implies that all subautomata of are sound, too. The set of states in is the set of extended equations according to Def. 5.4, see Sect. 7.1. There are two kinds of transitions: a substitution transition transforms the variables; a compression transition affects the constants, but not the variables, see Sect. 7.2.
If is a transition, then its label is a morphism (in the opposite direction of the arc) which is specified by a mapping where is some subset (possibly empty) of constants with . We assume that such a map extends to a -morphism by leaving all letters in invariant. Since , the restriction of also defines a morphism . Note that we use the same letter for both morphisms. There will be no risk of confusion.
Since , the morphism also induces an endomorphism of which respects the involution assuming for all . However, outside neither the action of nor the value of is defined, so is not an --monoid. It is simply a free monoid with involution, and we can read the label always as an endomorphism of the free monoid with involution .
New constants appear only by compression. If a word is replaced a letter by specifying , then we will automatically set , , , and hence: for all . By definition of , the second component in is a word of length at most such that the stabilizer satisfies . In particular, we have an efficient test whether for all : we just check that for all letters which appear in the word . The crucial observation is that whenever
[TABLE]
is a labeled path and is word, then can be viewed either as a morphism or as an endomorphism of . If we have , then defines a word and the corresponding element . By we denote the identity endomorphism on . Then appears as the label of transitions where is a morphism with for all . For example, the label might appear when or , etc.
7.1. States
We define the states of the as the set of extended equations according to Def. 5.4. Thus, every state is of the form .
7.1.1. Initial state.
The initial state is .
7.1.2. Final states.
A state is final if
- (1)
and uses no variables. 2. (2)
The word has a prefix of the form where are the distinguished letters mentioned in Thm. 4.3.
7.2. Transitions
We denote a transition as as and for both kinds, substitutions and compressions, we put some additional length restrictions on . For example, we allow for a letter only if is a final state. Thus labels on paths not ending in a final state are never length decreasing morphisms. Moreover, we require that is not too long. If is specified by a set , then we require where . These length restrictions are not used in the proof of the soundness result Prop. 7.5. We need them when proving completeness for a finite subautomaton of .
7.2.1. Substitution transitions
Definition 7.1**.**
A substitution transition is denoted as
[TABLE]
We must have and we require that the transition is defined by a -morphism and a -morphism such that for all . In particular, is length preserving.
In the case that some variable is typed in the source node , that is , then we add the following restrictions:
- •
. (Thus, for the set of variables cannot increase.)
- •
If , then . In particular, is defined if and only if is defined.
- •
If is not defined, then .
- •
If is defined, then .
We say that a substitution transition is special if . This implies that the label is is the identity on ; and therefore the label will be . Later it would be enough to only consider special substitution transitions. However this would not simplify the following proof.
Lemma 7.2**.**
Let be a substitution transition. If solves then solves . In particular, if is an -morphism, then and are entire solutions with .
Proof.
Recall by Def. 5.5 to prove solves we must show two things: and whenever is typed and we must have .
We begin by checking that implies for all typed variables. Consider a typed variable . The first case is: . Hence . By definition, is defined and . Then , too. Hence, because every solution has to satisfy . Since and is a -morphism we have . Therefore in the first case. The second case is where . Again, we can conclude . Thus, in both cases: whenever is typed, then .
Since , , and are -morphisms, so is their composition . Since is a solution of , we have . Hence, since because respects the involution. It follows that , so . Thus, is a solution at . As a consequence, and are both entire solutions because is a -morphism and .
M(B^{\prime},\mathcal{X}^{\prime},\theta^{\prime},\mu^{\prime})$$M(B,\mathcal{X},\theta,\mu)$$M(B^{\prime},\theta^{\prime},\mu^{\prime})$$M(B,\theta,\mu)$$\tau$$\sigma^{\prime}$$\sigma$$h
∎
7.2.2. Compression transitions
Compressions are defined only if . They leave the variables invariant, but we encounter both situations or . However, in case that the situation is more subtle than for substitutions, and we need again technical restrictions in order to guarantee soundness.
Definition 7.3**.**
A compression transition
[TABLE]
is defined in if is an -morphism such that the following conditions hold.
- •
We have
- •
* can be written as a word in for every and for all unless is a final state.*
- •
* is specified by a mapping with such that*
[TABLE]
- •
A variable is typed using if and only if it is typed using .
- •
There is some such that for all typed variables we have
[TABLE]
Note that for a given -morphism the conditions to be a compression transition are effective.
Lemma 7.4**.**
Let be a compression and be a solution at . Then there exists a -morphism
[TABLE]
such that for all . The -morphism satisfies the following conditions. If is an -morphism, then first, is an entire solution at and second, is an entire solution at . Moreover,
Proof.
Define for all variables and for all . This defines a -morphism since is a free monoid. (There is no type yet on the left.) Let us show first that implies in the monoid . That is, induces a -morphism (which we also denote by ) .
For with the assertion is trivial because leaves invariant. Thus, it is enough to consider a defining relation of the form where . Because of Def. 7.3 we know that is typed on the right hand side , too. Let . Thus, for some according to the last condition in Def. 7.3. Since for some , we conclude . Hence, whenever , then in since .
So far we have shown that is a well-defined morphism such that . This implies for all variables. For a constant we have Hence and this means that the diagram in Fig. 4 commutes.
The morphism in Fig. 4 denotes the restriction of the morphism , too. Let and hence, . In order to see that is an entire solution at we use and we content ourselves to consider the following line of equations:
[TABLE]
In particular, . It is also clear that is an entire solution at since leaves invariant. ∎
Proposition 7.5**.**
Let be a path in of length , where is an initial and is a final state. Then has an entire solution with . In particular, for we have ; and is sound in the sense of (15).
Proof.
Since is final, it has a unique solution . By the lemmas above, we obtain a solution at such that . Hence, is an entire solution as desired. ∎
8. The intermediate automaton
Prop. 7.5 states that the large automaton is sound. This property cannot be destroyed by removing states or transitions. That is, every subautomaton of is sound, too. We define a subautomaton of as follows. All extended equations are states of , so the state set is the same infinite set as for . However, for transitions we are more restrictive. To define transitions, let us first define a weight for equations and states. The definition is tailored that all compression transitions and certain substitution transitions reduce the weight of the state.
Definition 8.1**.**
Let be an extended equation where (as usual) is represented as a word. The weight of the equation is defined by
[TABLE]
The weight of the state is a pair of natural numbers .
For we order tuples in lexicographically. For example , but ; and we use the fact that there are no infinite descending chains in . Consider any transition in . Then we always have unless the transition is a substitution transition where at least one variable that appears in pops out a constant.
Remark 8.2**.**
The definition of is invariant under the word representation of . This follows because for all . Second, the advantage to use the weight in (instead of using the more straightforward choice of for ) is that following a substitution transition, which does nothing but replace variables by for , leads to a state of smaller weight.
A transition in belongs to if and only if the following properties are satisfied.
- •
If is a substitution transition, then , , and .
- •
If is a compression transition, then and .
The focus for the remaining part of the proof is on completeness. A subautomaton of is called complete if it holds:
[TABLE]
Since every subautomaton of is also sound in the sense (15) we see that every complete subautomaton is sound and complete.
Proposition 8.3**.**
Let be a trim, finite subautomaton of . If , then has at least one solution. If contains a directed cycle, then has infinitely many solutions. Moreover, if is complete, then the converse of both assertions is true.
Proof.
If , then has at least one solution by Prop. 7.5. Now assume that contains a directed cycle. By hypothesis is trim. Hence, there is an accepting path with a directed cycle and this cycle doesn’t involve any final state as final states are without outgoing arcs. Let be this cycle. Without restriction we have and because admits no infinite strictly descending chains. This means must be a substitution transition which is defined by some with for some where appears in the equation belonging to and is a constant. Hence, on some accepting path we can pop out an arbitrary number of letters of . Since on paths from an initial state to the labels are non-erasing endomorphisms, we see that we can make at the initial state larger and larger. Thus, there are infinitely many solutions. The converse, under the assumption that (17) holds, is trivial. ∎
9. Towards completeness
During the completeness proof we always work with a state and a given entire solution . Starting at a triple where is a standard state, we describe a deterministic process which yields a path inside the (infinite) automaton from to some final state so that . Thus, is complete. The crucial property is that we are able to control the lengths of all intermediate equations for by
[TABLE]
We make sure that whenever we see an intermediate state where , then has a special structure. Moreover, when we follow a compression transition then we make sure the soundness condition holds for the corresponding label according Def. 7.3.
We then can deduce Thm. 4.3 because for defining the complete NFA mentioned in the theorem it is enough to consider the starting point
[TABLE]
Since we can ensure is finite by allowing extended equations in only if the corresponding equation satisfies a concrete length bound in . Moreover, we impose that is trim. We will come back later to these issues. For the moment we work in the infinite automaton and there is no length bound for the equation .
9.1. Dummy variables denoting the empty word
In the following it is convenient to have the following notation at our disposal. We introduce purely formal symbols of the form where and is called dummy variable, but the symbol is just another explicit notation for the empty word . The dummy variable is never listed in . Its only purpose is that we have a unified notation for local equations (and avoid case distinctions). Since every morphism maps to . The advantage is that with the help of a dummy variable, we may, whenever convenient, assume that every local equation has the form
[TABLE]
Here are (perhaps dummy) variables and are words over constants.
9.2. The weight of entire solution and the forward property
We need a termination condition for the following compression procedure. Therefore we define a weight for the triple where is a state with an entire solution by
[TABLE]
At non-final states the weights and were defined in (16). Thus, actually for all states, we can write as a pair
[TABLE]
Being at we say that a transition satisfies the forward property if has an entire solution such that first and second,
Following a transition which satisfies the forward property means that we switch from to . Typically after each such step we rename the tuple as . Since using a transition satisfying the forward property reduces the weight , there are no infinite paths of transitions where all transitions on the path satisfy the forward property.
9.3. Meta rules
Let be a state with an entire solution . We apply the following meta rules whenever possible.
9.3.1. Remove variables with short solutions
If for some variable such that , then follow a substitution transition which is defined by a -morphism such that if and otherwise. The state uses the same set of constants, but we have . We also have and is the restriction of . (Thus, according to our convention we can also write .) Let be the restriction of , then is an entire solution at and we have . Moreover, . Hence, and the transition reduces the weight of the state.
As a consequence, whenever we are at a state with an entire solution , then we assume for all where .
9.3.2. Remove useless constants
We say that a letter is useless (with respect to ) if for all . Note that a letter is never useless. If contains a useless letter , then define . The inclusion of into defines canonical embeddings and such that and . The state has an entire solution where is the restriction of . Moreover, . Hence, we can follow the compression transition which satisfies the forward property.
As a consequence, whenever we are at a state with an entire solution , then we assume that doesn’t contain any useless letters.
Remark 9.1**.**
We may have that contains letters that are not -visible, but a solution uses them. Removing useless letters does not remove such letters.
9.3.3. Moving to a final state
Let be a standard state without any variables and with an entire solution . Then is the identity on and we have . If is final, there is nothing to do. Hence, we assume that is not final. Since , Def. 5.4 tells us
[TABLE]
Hence we can enlarge to a set which contains all distinguished for . (By our convention none of the belongs to because the state is not final.) We define a -morphism by letting . Moreover, we let
[TABLE]
We have no variables and . Hence is final. The entire solution at is and we have since none of the belong to . Since the compression transition satisfies the forward property. Hence, we are done.
As a consequence, whenever we are at a standard state with an entire solution , then we assume that . Moreover according to the other meta rules we have for all and every constant is -visible in .
10. Compression round: the first phase
We perform the compression in rounds. Each round has two phases. The first phase is called -periodic compression, the second one is called pair compression. During -periodic compression we perform all meta rules whenever possible. Recall how meta rules decrease the weight at states: removing a variable makes smaller, removing useless letters doesn’t change , but it makes smaller. Moving to a final state decreases the weight of the state down to (which was the exceptional weight at final states) . None of these rules increases the sum . Therefore all meta rules satisfy the forward property according to Sect. 9.2.
10.1. A simple, but useful, estimation
During the rounds the length oscillates but it can be bounded by some function in . In order to obtain such a bound we will later apply the following fact twice with different parameters.
Lemma 10.1**.**
Let and for some real constants , and let be a function with and which satisfies a bound
[TABLE]
for all . Then for all .
Proof.
The statement is true for . Assuming it is true for then
[TABLE]
∎
In -notation (19) reads as: if and , then for all .
10.2. Alphabet reduction at standard states
During our procedures we introduce more and more letters, so the set grows, and removing useless letters is not enough to keep the size of in .
The following procedure which we call alphabet reduction is not a meta rule (which we may apply whenever possible). If we call the procedure we explicitly say so. When we call it we wish that contains only -visible letters in .
We begin at a standard state with an entire solution where there is some letter which is not -visible. Hence for all . Removing useless letters is a meta rule. Hence, we may assume without restriction that all letters are useful and therefore we may assume for some variable. (That is, we are in the situation of Rem. 9.1.) Define
[TABLE]
Then we have . The procedure will takes us (via a compression transition defined by the inclusion ) to the state . Since we have and therefore , too.
It is here where the notion of entire solution becomes important. We have , so we can define a -morphism by for . Since is a free monoid, we don’t have to worry to check defining relations. Moreover, is solution at . Thus, we can switch from to via the compression transition . Since is an -morphism we obtain . Hence, as desired.
As a consequence, whenever we perform an alphabet reduction, then we arrive at a standard state with an entire solution such that every letter in is -visible in . This means that after alphabet reduction the size of is at most .
10.3. Mapping the positions from to
Let be a state with an empty type and let be any -morphism. Recall that (resp. ) denotes the set of positions of (resp. ). Then induces a mapping from to as follows. We define from left-to-right. We let . The first position in is labeled with and so is the first position in . No other position than is mapped to . We shall keep the invariant that if is the largest position which is mapped to . In particular, we have .
Now assume is already defined for all and . If we are done. Otherwise we have and we consider . By the invariant we know . We look at the label of the position . It is labeled by a letter in and there are two cases. In the first case the label is a constant . In this case we let . In the second case the label is of the form with . In that case we map all positions in the interval to the single position .
Note that enjoys the following properties. If is a position of which is labeled by a constant , then is a single position in which is labeled by , too. If is a position of which is labeled by a variable , then is a interval of length in . The label of that interval is just .
Definition 10.2**.**
We say that a position of is visible (in ) if is a constant. Otherwise it is called invisible. An interval of positions of is visible (in ) (resp. invisible) if all positions in that interval are visible (resp. invisible) positions. If contains an invisible position, but , then we say that the interval is crossing.
10.4. The start of a compression round
Each compression round starts at a standard state with an entire solution . We may assume that no meta rule is applicable. The very first step is now an alphabet reduction. For simplicity, we denote the state again by and we have .
10.5. -periodic compression
For convenience we rename the tuple
[TABLE]
At this point we know that no meta rule applies to and that .
Let us consider all very long maximal -periodic factors of which have a maximal occurrence with at least one visible position. (By maximal occurrence we mean that is not a factor of a longer -periodic word at that occurrence.) We assume that at least one such occurrence exists, otherwise we skip the main body of the -periodic compression and proceed directly to the end: Sect. 10.6.
We write with , is primitive of length at most and is a nonempty prefix of . (Recall very long means so .) By Lem. 6.4, we can encode the factor uniquely by writing the triple . Let us call and the borders of the very long maximal -periodic factor . Consider different occurrences and of very long maximal -periodic factors in . If the occurrences overlap, then this overlap takes place in the borders only, because otherwise the occurrence of the factor was not maximal.
It follows that the number of occurrences very long maximal -periodic factors with at least one visible position is less than . Thus we find some minimal index set of size such that
[TABLE]
is exactly the set of very long maximal -periodic factors of which have a maximal occurrence with at least one visible position.
The idea is that at the end we arrive at a state with a solution where all these occurrences are replaced by where is the notation for a fresh letter such that , , and . We also color certain positions in and . At the end of the process a position will be green if and only if it is labeled by some new letter .
Note that is just a formal symbol: we need at most bits to encode it. We also define a set of primitive words
[TABLE]
We have
[TABLE]
Next we consider fresh variables which are denoted as where , and for certain and then for all . These new variables will later be typed. We define the action of by and the involution by . The idea is ; and thus, and . Note that if and only if and hence is in the known stabilizer of .
The following routine introduces these new variables using substitution transitions. Recall that defining substitutes by and simultaneously by for all .
begin procedure (insert new variables)
Initialize a set of fresh variables by and put .
forall do
(Note this means we do the process once for and once for .)
- (1)
Apply all meta rules whenever possible; in particular, for all variables. 2. (2)
Let be the longest suffix of such that is primitive, , and is a prefix of . If , then do nothing. 3. (3)
If , then define words , , and by with , , and . (Note that is primitive: we have for some factorization .) We enlarge by a fresh variables for all factorizations . Moreover, if we enlarge by some , then we also include and for all .
We can write with . Follow a substitution transition which is defined by and define an entire solution at by where and . The transition satisfies the forward property. (Due to the meta rules it can happen that becomes smaller and/or that is not enlarged at all.) 4. (4)
Rename as .
**endforall
endprocedure**
The number of new variables is bounded by because . The factor comes in because we consider all cyclic permutations of . The factor comes in because we close under -action. On the other hand we don’t need to list in for if is already listed. Thus, a list of new variables suffices to specify the full set (which is closed under the action of and involution. Note that . So we keep the invariant that variables are not self-involuting.
From now on until the end of -periodic compression we only remove variables. So, if is the full set of variables we meet during the whole procedure, then we have:
[TABLE]
Before the procedure we had and , and as required for a standard state. The corresponding set after the procedure is . We have to check that (because otherwise it is not an extended equation as per Def. 5.4). This bound is immediate.
In the case we are still at a standard state and For we are not at a standard state because is not contained in .
Since for the type is empty, we map the positions of to the positions as explained above in Sect. 10.3. Consider any occurrence of a very long -periodic factor in which is maximal and where at least one position is visible and where . Consider the occurrence of all very long maximal -periodic factors where . Each factor can be written as where .
For all maximal occurrences of these factors let us color the inner positions belonging to green. Then only green positions are mapped to a variable . It is also clear that we we can write for some factorization . Let us transport the green color to the corresponding positions in . Then for all positions in which are labeled by a variable it holds that the position is green if and only if it is new variable. Note that green positions in are separated by words of length at least .
In the next procedure we will introduce a type which consists of defining relations of the form , but it will be enough to apply such a rule where both positions in are green. Hence, the color of the positions will not be altered under this restriction. In order to define we use , otherwise we skip the next procedure.
begin procedure (introduce a type )
- (1)
Define the type by
[TABLE]
Note that is actually a consequence of the other relations in . We include it order to satisfy the definition of type in Sect. 3.3, that if a variable (in this case ) appears in a type then there is a unique primitive word with which it commutes. 2. (2)
Choose any and write . (Note that we have in this case, since a meta rule would remove the variable if it has a solution shorter than ). Define a morphism by . The morphism is well-defined since in for all . 3. (3)
Follow the corresponding substitution transition
[TABLE]
The transition satisfies the forward property with the entire solution where . Apply all meta rules. (After that we may have again.) 4. (4)
Rename as .
endprocedure
Using the relations from we can move the variables around over green positions. Thus, we can choose a word representation for as such that every maximal green interval of positions in is labeled by a word of the form
[TABLE]
In the following we simply say that is a maximal green factor when we actually refer to the label of a maximal green interval of positions. We can choose because in a standard state all local equations are triangular, but this is not essential. Without restriction we have and that satisfies . This is clear if . For it is enough to substitute by . For each there is such that and therefore:
[TABLE]
At this point we will change to (defined below) since the defining relations with will be of no use anymore. The idea is to replace the factors , , and by fresh letters denoted by , , and . The is used to encode the sum . We will make the assumption , then , , and are three different letters for , and there is no letter , only . For the maximal green factor we intend to define a word and a type such that
[TABLE]
More precisely, for each we associate a new letter with , and for every typed variable with . Recall our notation that is a very long -periodic word, , is primitive, and . It is important that is visible, whenever at least one the green positions is visible. This why in the different word representations (26)–(28) for the same the always sits between the variables.
By introducing (if necessary) more fresh letters we close the set of fresh letters under involution and -action. We let:
[TABLE]
The set of these new letters is denoted by . The number of new letters can be bounded by:
[TABLE]
Let . Next, we define the new type . For each typed variable there is exactly one commutation rule: . The other defining relations say that and are “conjugate” due to the letter . Making this formal we specify by:
[TABLE]
Note that the defining relations in are designed that (26)–(28) hold.
We can now define the rest of the -periodic compression procedure. It is the analogue to Jeż’s “block compression” as described in [11]. During the process sets of positions for and change, but our process makes clear that we can always transport the green color: no change involves an interval which has both colored and uncolored positions. We perform the following steps.
begin procedure (remove very long -periodic factors with a visible position)
- (1)
Define the element by replacing maximal green factors in just we as have done for in (21) in order to produce in (26). Doing this everywhere defines in a word representation as . 2. (2)
Define a -morphism
[TABLE]
by and We have and we obtain a compression transition satisfying the forward property
[TABLE]
Note that since due to the fact that (by our assumption) at least one green interval exists with a visible position exists; and therefore some new letter is visible in (which represents the word of length at least ). The new entire solution at is where for and if . We apply the meta rules and then we rename as but we keep the notation for , , , , and (although , , and may become smaller by the meta rules and changes). 3. (3)
while there is letter do
- (a)
If , then choose some . Use a substitution transition defined by to make sure that is shorter than at the beginning of the loop and that we don’t run out of letters as long as there are typed variables. The invariant is that as long as there is some letter visible. 2. (b)
Use transitions of the form in order to keep the invariant that where is even. Moreover, due the meta rules we maintain . At some point might be too short, then we remove from . We also maintain the invariant that for all and . Thus, if we remove one , then all other typed variables using the symbol are removed simultaneously and becomes smaller, too. 3. (c)
If there is a maximal green factor
[TABLE]
where and is odd, then define an endomorphism
[TABLE]
by . Thus, we can write
[TABLE]
This defines a new equation and a -morphism such that and . Hence, there is a compression transition satisfying the forward property
[TABLE]
As above, since . The new entire solution at is . We apply the meta rules and then we rename as . 4. (d)
Due to the previous steps: whenever we see a maximal green factor
[TABLE]
then for and is even. Define an endomorphism
[TABLE]
by for all which appear in . Thus, we can write
[TABLE]
This defines a new equation and a -morphism such that and . Hence, there is a compression transition satisfying the forward property
[TABLE]
As above, since . The new entire solution at is . We apply the meta rules and then we rename as .
endwhile
endprocedure
It is clear that the procedure terminates in some standard state. Let us denote that state and its entire solution as:
[TABLE]
We began the routine at . During the procedure we see symbols and , and the length of the equation grows as we pop out letters in the suffix and prefix of each variable. At the end all the new variables disappeared, either by the meta rules or when maximal green factors are compressed into a single letter . The only new letters in are of the form and there are not more than of them.
The following proposition summarizes all the changes that happen in the procedure.
Proposition 10.3**.**
Let be the state where we started -periodic-compression with an entire solution . Let denote the standard state with the entire solution where we finish -periodic compression and let be any state which we have seen (with the full set of variables ) on the path from to during the procedure.
Then we have the following.
- (1)
* for some .* 2. (2)
. 3. (3)
. 4. (4)
. 5. (5)
. 6. (6)
. 7. (7)
. 8. (8)
For each the word does not start or end with a very long -periodic word.
Proof.
We justify each item as follows.
- (1)
Meta rules may remove some (useless) letters from the initial alphabet , so we have , and the only new constants that survive at the end are of the form . 2. (2)
consists of letters in and those from . Since we applied alphabet reduction at the beginning, , and since the letters cannot be eliminated by any compression during the procedure, their number is bounded by . The only other new constants added during the procedure are of the form but these are all eliminated by compression, so do not appear in by the meta rule. 3. (3)
Again we have . During the procedure we add letters and . For each variable we add some and , then we need to multiply by since we have all cyclic permutations of these and . Since the are at most variables this gives new constants, so applying the action we get the bound of new constants. 4. (4)
We first pop out because we had with . (If we do nothing.) After applying we have and . If it is the case that then later we do not apply any compression to since it is not part of a very long factor, instead we simply pop it out. This contributes at most in the worst case that this happens in the suffix of every .
If then together with this gives a factor of length at least , so is part of a very long -periodic word so it is compressed down to a single letter. Thus is the most added at either end of any variable by the procedure. This gives . We give the larger bound to simplify later calculations only. 5. (5)
Since at every state in , it is enough to show . However this only requires the estimation in Sect. 10.1. By that estimation we content ourselves to define a function with and which satisfies for all a bound
[TABLE]
for some and . To see where the comes from in our application, choose to be number of letters at the state where they first appear. Each time we pass through a transition defined by we half the number of these letters; and this shows that we can define . Between these steps where we halve the number of ’s we create at most new ones with . 6. (6)
During the procedure we add new variables but these are eliminated by the compression. Since we apply meta rules we may also remove variables . Thus . 7. (7)
This is justified above at (20). 8. (8)
Consider any with . If for that , the word at the beginning at the procedure “insert new variables” had a -periodic suffix of length more than , then, due to the splitting of variables, the length of the maximal -periodic suffix in is exactly . Hence, there is no very long -periodic suffix. In the other case the suffix of length in and coincide. Thus, in this case the length of the maximal -periodic suffix in is at most . Since implies the same is true for the prefix of each variable.
The proposition is therefore shown. ∎
10.6. The end of the -periodic compression
Recall that we started a compression round at a standard state with an equation ; and we end standard state with an equation . (Possibly .) If, due the meta rules, is final, we are done. Hence, we continue under the assumption that is not a final state.
11. Pair compression
We enter the second phase of the compression round with “pair compression” directly after the end of -periodic compression. We enter the pair compression procedure at a standard state which is not final and with an entire solution . If and denote the situation where we began the current compression round (where we began -periodic compression), then Prop. 10.3 tells us:
[TABLE]
During the pair compression all states are standard states. No type is needed. Phrased differently, we have , there are no typed variables and hence, all variables belong to . Thus, the number of positions labeled with twisted variables is at most , as it is required for standard states.
Our goal in this section is to compress pairs of constants into single letters without causing any conflict due to overlap with other pairs or variables that are connected via twisted equations. In particular, compressing a pair linked to a -periodic factor might cause problems, so we wish to avoid compressing those pairs. This leads us to define the following.
Definition 11.1**.**
Let be a standard state with a solution . We say that satisfies the shrinking pair condition if there is no such the word starts with a very long -periodic word444Recall that a word is very long -periodic if and only if and is a prefix of some word where , see Def. 6.3..
Note this is the situation we find ourselves in at the conclusion of the -periodic compression procedure: with its solution satisfies Def. 11.1. The shrinking pair condition is a necessary condition when proving Lem. 11.3 below. That technical lemma is one of the key steps.
11.1. Positions revisited
Consider any standard state together with a entire solution . We introduce a precise notion of equivalence between positions (and intervals) of , which we introduce now. The idea is that whenever we modify a solution at a position , then we must modify at all equivalent positions in order to keep the property of being a solution. Moreover, should be the finest equivalence relation with that property. For example, when we compress a factor where , are letters, then we want to compress only certain occurrences of (where ) and not all of them.
As explained in Sect. 10.3 there is a canonical mapping from the set to the set of positions in . By we denote the label of a position in . Recall also the notion of duality: if is an interval in , then denotes the dual interval, where for all . According to the definition of standard states, the set of twisted variables which appear in can be written as and we have . It is convenient to fix a subinterval of for each such that as follows. Consider , then without restriction we have for some unique (and hence ). Choose for the left-most maximal interval in which is mapped to a position labeled by . In particular, . We let . By the specific structure of being an extended equation, we see that is the right-most maximal interval in which is mapped to a position labeled by . To have a notation we let and
[TABLE]
Note that and are disjoint sets of positions: if , then there is some such that is mapped to a position labeled by and is mapped to a position labeled by . The next idea is to identify positions in based on the fact that we can write in the form such that . In pictures we intend to place the positions of and on top of each other. The intuition is clear: we have . The positions of cover . Hence, we can think that uses the same set of positions as , namely the set . Thus, every has always two interpretations: for as a position either in or in , for the situation is dual. Let us make this intuition formal.
The mapping from to the positions of induces a relation
[TABLE]
We define inductively. If is mapped to a position in which labeled by a constant, then we have and we let and . In the other case is mapped to a position labeled by for some and . Let the leftmost position in which is mapped to the same position as . Then we can write and we find . In this case we let and . Note that this implies . The position belongs to .
Up to duality, there are three cases:
- (1)
and . Then there is only one such that . 2. (2)
and . Then we have and . Since , we have . 3. (3)
and . Then and with . Hence, there there are at most two such that and i\mathrel{\mathchoice{\reflectbox{\displaystyle\leadsto}}{\reflectbox{\textstyle\leadsto}}{\reflectbox{\scriptstyle\leadsto}}{\reflectbox{\scriptscriptstyle\leadsto}}}k.
Let us explain the meaning of this “” relation by considering a local equation . In this local equation corresponds to some factorization
[TABLE]
Let and . Then the interval is labeled by ; and, since is a solution, we have . For each we have where either or . If , then and therefore , too. The positions of are visible in , but with respect to this true only for the positions of and . For the positions of and the relation is the identity. The relations are depicted in Fig. 5: the relation is given by the positions in the middle row to the top and bottom row. Let j\mathrel{\mathchoice{\reflectbox{\displaystyle\leadsto}}{\reflectbox{\textstyle\leadsto}}{\reflectbox{\scriptstyle\leadsto}}{\reflectbox{\scriptscriptstyle\leadsto}}}i denote . If j\mathrel{\mathchoice{\reflectbox{\displaystyle\leadsto}}{\reflectbox{\textstyle\leadsto}}{\reflectbox{\scriptstyle\leadsto}}{\reflectbox{\scriptscriptstyle\leadsto}}}i\leadsto k, then we write .
Consider any and such that j\mathrel{\mathchoice{\reflectbox{\displaystyle\leadsto}}{\reflectbox{\textstyle\leadsto}}{\reflectbox{\scriptstyle\leadsto}}{\reflectbox{\scriptscriptstyle\leadsto}}}i\leadsto k. (The interesting case is .) Hence, we have and in the pictures we put the positions and on top of each other. Fig. 5 gives an example, where , , and .
Since we have
[TABLE]
Moreover, implies that there are such that . Thus, ensures
We have and is a symmetric relation. It is also reflexive on .
By we denote the reflexive and transitive closure of . However, the relation is too fine, in general. Since implies , we cannot expect that , because is typically not in . Clearly, if we intend to change the label at position from, say, to , then we must change the label at position from to .
In the following, we write if and we define to be the equivalence relation over which is generated by . We have , but we have just seen that these relations are different, in general. Since by (40), we have
[TABLE]
Hence,
[TABLE]
We extend the notation above to intervals. Let , be positions in such that , and let . Assume (by symmetry) that we have due to mapping the position of to a position in which is labeled by a twisted variable . If the position is also mapped to the same position , then all positions in the interval are mapped to . We then write
[TABLE]
As above we now define the relation on intervals. Again, we let be the generated equivalence relation, now on intervals. Finally, we relate an interval with to the interval via
[TABLE]
Thus, we also extend to the equivalence relation on intervals which is generated by and . Having this, the general form of (41) becomes
[TABLE]
In the following we say that two positions (or intervals) are equivalent if they are related by .
Lemma 11.2**.**
Let and be a solution at a standard state such that for all . For each write with . Let and denote state and solution which we obtain by following a substitution transition defined by for all . Let be the set of positions according to (38) and the equivalence relation on intervals with respect to . Let and positions in such that , then we have with respect to and .
Proof.
Let . Then and if , then the corresponding interval with respect to is . Thus, if with and , then we obtain a “domino tower” as depicted in Fig. 6. The intervals with respect to are the white blocks and and are arranged such that sits along a vertical column above . We obtain the corresponding tower with respect to by adding the grey borders of length at each side in order to switch from to . Thus, with respect to implies . ∎
The distance between positions of is denoted as usual: . We continue with the same the notation as in Lem. 11.2. We apply the lemma with . Recall that we fixed the parameters such that and . Hence, .
Lemma 11.3**.**
Let and suppose that satisfies the shrinking pair condition (Def. 11.1) with respect to . Let be a variable with (and hence, ); and let such that with respect to . Then we have .
Proof.
According to Lem. 11.2 we have with respect to . Next, we choose as large as possible so that is a subinterval of and with respect to . By induction on the number of steps using the relation , this implies that there is some interval such that both, first
[TABLE]
and second, is the first position in , see Fig. 7. Assume, by contradiction, . Then, and are twisted conjugate with a positive offset which is at most . This implies that is a very long -periodic word by Cor. 6.2. Therefore, the prefix of is a very long -periodic word. This contradicts the hypothesis that satisfies the shrinking pair condition. ∎
11.2. Red positions
We use the notation of Sect. 11.1. Let be a maximal interval in which is mapped to a position in which is labeled by some where and . Thus, the factor is equal to the word . The positions and at the borders of play a special role because if there is a factor , then we cannot compress because is “crossing”: compressing might be “dangerous”. In order to signal “danger” we color the first and the last position in each interval red. Moreover, whenever holds in , then color red, too. For example, if we have a situation as depicted in Fig. 8, then the red color at the last position of and the red color at the first position of yields two red columns. Note that the first red position in and the last red position in in are equivalent: these are dual positions. For convenience, we also color all positions in red which are labeled by the marker symbol . If the label of is , then .
Since for all positions, it follows that there are at most pairwise different equivalence classes of red positions. This counting will be used later.
Consider an interval of length two without red position. The idea is to compress into a single position. The problem is overlapping: we might have or . Note that implies or . Similarly, implies or . Therefore, we start with intervals of length where all four positions are inequivalent: This enables us to compress the middle interval of length . We shall use the following lemma.
Lemma 11.4**.**
Let be an interval of length without any red position and where the positions are pairwise inequivalent. Consider . Then there are two cases:
- (1)
, 2. (2)
* and .*
Proof.
Notice that each of the intervals is without red positions. We may assume that because otherwise we are done.
First, let . By contradiction assume . Then which implies . Since we obtain . This was excluded.
In the second case we have . Let us show that and leads again to a contradiction. Since we cannot have . Hence or . By symmetry in and , we may assume .
We cannot have because then , but , and hence, . This is impossible. Thus, and . We remember . If , then (as no position is red) implies . This is impossible. Hence, the last option is and . However, implies . We have again a contradiction as . ∎
Ex. 11.5 indicates why the assertion in Lem. 11.4 only holds in the middle interval of , in general.
Example 11.5**.**
We don’t exclude that acts with involution. Thus, there might be an and such that . Consider the equation with the solution and where for . Then we have
[TABLE]
The positions of can be identified with with for all positions . Since positions and are equivalent, the interval contains equivalent positions. The four positions in the interval are pairwise inequivalent. However, intersects with . Thus, later on we cannot compress the interval corresponding to the pair . On the other hand, there is no obstacle to compress the interval which is labeled by .
Lemma 11.6**.**
Let be a solution at a standard state and be an interval of length in without any red position such that implies for all . Then contains a subinterval of length where all positions are pairwise inequivalent.
Proof.
For simplicity of notation let . If all positions in are pairwise inequivalent, we are done. In particular, there are such that . Since, this implies by (41). This in turn means that we cannot have where because this would lead to via . We say that is the partner of if but . We conclude that every has at most one partner.
We know for some . Hence . Let . Since is without red positions, this implies
[TABLE]
This means that every position has one partner in . Since and , we are done: in all four positions are pairwise inequivalent. ∎
Definition 11.7**.**
We say that an interval in is good if the following conditions hold.
- •
Neither nor is red.
- •
The positions and are visible,
- •
Whenever , then either or .
Remark 11.8**.**
The definition of a good interval excludes . Indeed, since neither nor is red, implies , hence an overlap . However, is allowed. Hence, it may happen that . If such an is labeled with , then there is some with . Hence, and . We deduce that we obtain a consistent labeling for
[TABLE]
Thus, we may compress into a single position with label and therefore, due to , we must also compress into a single position with label ; and due to , we have to compress into a single position with label . But this is fine, we have , , and .
11.3. The procedure
Recall that we have fixed and . Thus, and . We start at a standard state together with an entire solution where none of the meta rules apply. In particular, and with . Hence, by definition:
[TABLE]
All local equations have the form . (As before dummy variables are allowed.) We define the equivalence relations and over the set of positions of as defined in Sect. 11.1. Let be a standard state with equation and entire solution . Once, we found a good interval in , we may call the following procedure for that interval.
begin procedure (compress a good interval )
- (1)
Let and let be the label of the good interval . Choose a fresh letter with stabilizer ; and define a -morphism from to by . Whenever , then the label of is for some . Replace each of the intervals (resp. ) by a single new position and label this position with (resp. ). (There is no conflict in this relabeling, see Rem. 11.8.) Since there is no red position in and , none of the intervals or is “crossing”. So, this gives a new but shorter equation . We have and new solution such that . 2. (2)
Follow the corresponding compression transition
[TABLE]
We have a new state with an entire solution . There is also new numbering for the positions, but the red positions can still be identified.
endprocedure
We are now ready to define the procedure “pair compression” which uses “compress a good interval” as a subroutine.
begin procedure (pair compression)
- (1)
For every write with . Follow a substitution transition x
[TABLE]
defined by the substitution and . This transition satisfies the forward property with the new entire solution where for all . Recall that .
After the preceding step, define the intervals with respect to as done in Sect. 11.1. Use the red color for the first and the last position in each . Color in red all equivalent positions in of red positions with respect to , too. See Sect. 11.2. 2. (2)
Rename as . 3. (3)
Define the alphabet . During the following loop we keep the invariant . 4. (4)
while contains a good interval with a label in
do
- (a)
Choose any good interval in . 2. (b)
Run the procedure “compress ”. 3. (c)
Rename as and transfer the induced coloring of red positions.
endwhile 5. (5)
Perform an alphabet reduction at the standard state . 6. (6)
Rename as .
endprocedure
Remark 11.9**.**
The procedure “pair compression” may not actually succeed in compressing any pair. Its first step always “pops out” letters to make the equation longer (by ). After that if no pair is compressed, the procedure leaves the equation longer than before it was called. This is intentional: if the equation becomes long enough, then one of -periodic- or pair compression is guaranteed to reduce the equation size by a positive fraction.
11.4. The end of pair compression ends the compression round
We began the compression round at a standard state with an entire solution . We ended the -periodic compression either by entering a final state or, in the other case, at a standard state with an entire solution such that
[TABLE]
We started the pair compression at the standard state with the entire solution . Compression took place only for good intervals which where labeled by words with . Each compression reduced the length of the equation because a good interval consists of two visible positions. Thus, at most compressions were possible; and this shows that we did not introduce more than fresh letters. Thus, every alphabet of constants we met during the entire round satisfied
[TABLE]
Now, let denote the standard state with the entire solution where we end the procedure “pair compression”. In the very first step of the procedure we followed a substitution transition. This is enough to infer
[TABLE]
Proposition 11.10**.**
Let be a standard state with an entire solution at the start of a compression round and be the standard state where we end the round with the entire solution . Then we have
[TABLE]
Moreover, if is any equation which we see on the path from to , then we have .
Proof.
Each compression round has two phases. The -periodic compression stops at a standard state with an entire solution . By Prop. 10.3 and all intermediate equations satisfy .
Now, let be any equation being on the path from to . The additional length for is due to the first step in pair compression when we substitute variable by with . This shows . Moreover, and .
Thus, by Lem. 10.1 it suffices to prove
[TABLE]
Let us have a closer look at a local equation in . (We allow dummy variables). In particular, we can think that begins with a prefix and ends with a suffix . Having this, the word is covered by factors and . In the first steps of pair compression we follow substitution transitions and a factor becomes and becomes .
Pair compression compresses all factors , , and into single letters. This bounds the total increase by the first substitution transitions by .
We don’t have such a simple bound for the factors because the corresponding positions in interact with the positions in . Let be the interval in corresponding to . Let us cut the interval in into a disjoint union of intervals, each of them having exact length . If a position belongs to any of these intervals of length , then we mark the position. Thus, at least positions in the interval belonging to are marked by these intervals. (We have no better bound since and might be dummy variables.) Removing if necessary at most of these intervals we may assume that their total number is with . The crucial observation is that we have
[TABLE]
Each interval of length is split in intervals of length . By Lem. 11.3 an interval of length can have at most red positions. Thus, in each interval of length there are at least intervals of length without any red position. By Lem. 11.6 each such interval contains an interval of length where all positions are inequivalent. By Lem. 11.4 we can compress at least one interval in that interval of length . (Note that Lem. 11.4 provides us with a compression inside . This means, the compression is guaranteed even if we compressed before an interval or .) This means that the length of is reduced to at most during compression. Hence,
[TABLE]
Due to (47) we conclude . This shows (46) and hence, the assertion of the proposition. ∎
Remark 11.11**.**
Prop. 11.10 tells us that there is a constant such that We content ourselves with a generous bound by letting . This bound suffices and it is an overestimation, as it can seen by the preceding proof and by reversing the -notation into concrete constants. The value was chosen such that the later constant in Cor. 12.1 is divisible by . Thus, we can conclude and for every equation we see on the path from to the following upper bounds.
- (1)
If , then and . 2. (2)
If , then .
These estimations are used in next section.
12. Putting it all together: the overall compression method
Now we explain what we do if we start the first compression round at the initial state with a given initial entire solution . We begin a first compression round with and with a given initial entire solution . We end the round after one phase each of -periodic compression and pair compression with a standard state and an entire solution such that . We repeat this process by starting the next round with and and ending the round in and . For simplicity of notation we write . Thus,
[TABLE]
We conclude
[TABLE]
By (49) the process terminates: there exists some round and during that round we reach a final state without variables and with an entire solution . Hence, the entire process defines a path in which is labeled by some such that We have and therefore . (Note that for large the ratio tends to [math]. For large the initial size is much, much smaller than . By Rem. 11.11, for all rounds with we can state:
[TABLE]
We also need an estimation for the maximal weight of an equation in the middle of each round. Prop. 11.10 says we have to add at most with respect to the starting point of a round. Thus, the conclusion of (50) is therefore: whenever we see an equation on the path from to we have
[TABLE]
Corollary 12.1**.**
Let and let the subautomaton of which is defined defined as follows. The states of are the extended equations where
[TABLE]
Then is a finite and complete subautomaton of . Let be the trimmed subautomaton of , then the NFA accepts a rational set of -morphisms satisfying the following conditions from Thm. 4.3
[TABLE]
Moreover, if and only if ; and if and only if doesn’t contain any directed cycle.
Proof.
The automaton is finite because first, the number of states is finite and second, if is any state in , then there are only finitely many transitions in where . Thus, the out-degree is finite for every state in . Since is finite, is finite, too. The NFAs and are both sound by Prop. 7.5. They are complete, this follows from Prop. 7.5, since is large enough by (51). This shows
[TABLE]
Finally, Prop. 8.3 implies that if and only if and that if and only if doesn’t contain any directed cycle. ∎
12.1. The algorithm to compute the trim NFA .
The method is standard and is essentially the same as in [26, 11, 5]. Therefore we give a rough sketch only. The key is the upper bound in Cor. 12.1: it is enough to consider states where . This implies that the maximal length of an equation and the maximal number of -visible letters is in . This in turn gives the upper bound on the alphabet . It is also clear that we need at most variables. To each symbol we have to attach its -value in the finite monoid .
By Sect. 4.2 storing a -value costs bits by (4). As a consequence we can specify a state (and therefore a transition ) in with bits.
Our algorithm must output all transitions which belong to . Hence, we consider all candidates based on the upper bound of bits for their specification one after another in some order, say in some lexicographical order. The algorithm has to decide if it outputs the transition or whether it moves to the next candidate. Thus, when considering whether or not belongs to , then the algorithm guesses a path of transitions from an initial state to the state and a path of transitions from to a final state. If the guess is successful, then it outputs and it moves to the next candidate. If unsuccessful, then we apply again the theorem of Immerman-Szelepcsényi: is closed under complementation. Hence, the algorithm “knows” whether or not belongs to before moving to the next candidate.
The proof of Thm. 4.3 is complete, and the first part of the paper is finished.
13. Part 2: The existential theory with rational constraints for virtually free groups
It was shown in [7, 35] that the existential theory with rational constraints in f.g. virtually free groups is decidable. Our main result (Thm. 14.2) provides an effective EDT0L description for the full set of satisfying assignments to a Boolean formula in free variables over equations and rational constraints. In order to make our statement precise we need some preparation.
13.1. NFAs revisited
Let and be finitely generated monoids. In the application and are fixed and not part of the input. Therefore we can define the size of an NFA over (resp. ) which is, up to a constant, independent of the generating set.
We begin by choosing any finite generating set . Then we specify an NFA for as tuple where the set of transitions is finite and satisfies . Having this, a natural definition for the input size of is
[TABLE]
The transitions in might be labeled by words of length greater than . However, this can be “repaired” easily by replacing a transition with and by a sequence of transitions
[TABLE]
were are fresh states. The input size of the new automaton is at most twice as large as before. The exact size of an NFA is of not important. We let
[TABLE]
This is well-defined, since if we move to another finite generating set for , then we see . Thus, it is convenient to denote simply as because then the interpretation is encoded in the syntax. Still, we can use up to multiplicative constants.
Let be a homomorphism to a monoid with a finite generating set , then the NFA is defined as where . For let . If for all , then there is a result which is again independent of the choice of and :. We have
[TABLE]
13.2. Exponential expressions
The ideas and results in this section are not new. The notion of exponential expression was proposed, for example, by Plandowski in [44]. For the application to exponential expressions are crucial to show a complexity within . Intuitively it is more natural to represent strings by allowing exponents. For example, if is a word, then it is more natural to write rather than in plain form by repeating a hundred times .
Exponential expressions (and plain exponential expressions) over an alphabet and their sizes are defined inductively as follows.
- (1)
Every word is a plain exponential expression of size . 2. (2)
Every plain exponential expression is an exponential expression. 3. (3)
If are exponential expressions, then the concatenation is an exponential expression of size . If are plain, then is plain, too. 4. (4)
If is an exponential expression and , then is an exponential expression of size .
Since is equipped with an involution, we define for all the expression as a synonym for ; and we let denote the empty word . The size of the expression is still .
In the following we allow that an equation appearing in a Boolean formula is written as where and are exponential expressions. We view and as words which have a special encoding in a compact form.
13.3. The existential theory with constraints and expressions
As above denotes a finitely generated monoid with involution. We let be any finite symmetric set of generators: that is, . Let be the canonical morphism which is induced by the inclusion . By we denote a countable set of variables such that . Without restriction we assume that is a set with involution and for all . As usual, we let for group elements.
The existential theory of with rational constraints and exponential expressions is defined with the help of Boolean formulae in free variables from . As we did in Sect. 4.2, we obtain more accurate (and therefore better) complexity results if we define the size of a Boolean formula as a pair . The parameter behaves as if all NFAs defining the rational constraints were of constant size. Thus, essentially, it adds up the sizes of the equations of the exponential expressions defining the equations. This is reflected by the index “eq”. The parameter adds up the input sizes for the NFAs which define the rational constraints. This is reflected by the index “rat”.
The formal definitions are as follows. Here we assume that every constraint with is given as (resp. ) where is an NFA as in Sect. 13.1. Exponential expressions were defined in Sect. 13.2.
- (1)
Every atomic formula is Boolean formula. The atomic formulae are:
- •
The constant (meaning “false”)
.
- •
Exponential expressions over .
and .
- •
Constraints .
and . 2. (2)
If are Boolean formulae, then so are , , and , but we omit brackets when possible.
, and for .
Let be a Boolean formula and be a morphism (that is, a mapping respecting the involution). Then the truth value is defined in the obvious way. If there exists some with , then we say that is satisfiable. We also say that is a solution if because it solves the satisfiability problem. So, we do not distinguish between satisfying assignments and solutions. The existential (first-order) theory with rational constraints refers to the set of satisfiable Boolean formulae
[TABLE]
We are not only interested to decide , what we aim for is an algorithm which produces on input a Boolean formula an effective description of the full solution set . To define it properly we let be the set of variables such that or appears in . We let
[TABLE]
Note that satisfies if and only if its restriction to satisfies . It is also clear that every morphism satisfying can be extended to a morphism satisfying . If the context of is clear, we abbreviate . Once we have chosen a presentation where is finite and is onto, then we typically represent elements of by words over and a morphism is defined via a mapping . Moreover, without restriction comes with a linear order. If is the subset of the first variables with for all , then we let
[TABLE]
Clearly, to decide is the same as to decide on input whether or not is empty. Moreover, . Note that either or . We will see that is an effective EDT0L relation for every if is a f.g. virtually free group.
When proving this result for virtually free groups we make various transformations on NFAs (which up to a constant factor don’t change ) before, eventually, we switch to Boolean matrices.
13.4. Removing exponential expressions in
Exponential expressions in Boolean formulae as in (56) are used because they may reduce the size of significantly. On the other hand, with the help of more variables we can transform into a new formula where all equations are written in plain form as . The transformation is not expensive; and it doesn’t change the full solution set:
Proposition 13.1**.**
There is a deterministic algorithm working in linear space which takes as input a Boolean formula using exponential expressions.
The output is a formula having the following properties.
- (1)
Equations in appear in plain form as . Hence, . 2. (2)
. 3. (3)
. 4. (4)
. 5. (5)
The restriction induces a bijection
[TABLE]
Proof.
The method is standard: replace all exponential expressions by straight-line programs (SLPs), see for example [33, 34]. More precisely, as soon as an exponential expression with appears, replace the expression by the empty word . If an exponential expression appears in , then replace every occurrence of simply by . If an exponential expression with appears in , then define a fresh variable . (This implicitly means to introduce , too. We don’t repeat this anymore.) Whenever a variable is introduced where , then we introduce another fresh variable , too. In particular, and are introduced (but the condition makes sure that is never introduced). The total number of fresh variables introduced that way is bounded by .
After that step, replace all occurrences of by , if was defined by in ; and for each fresh with introduce a new plain equation
[TABLE]
Moreover, introduce a single equation The effect is that each occurrence of , having size , is removed. The gain of is mitigated by new equations of constant size and one more equation of size .
After that step replace by the conjunction of with the conjunction of the new equations. Continue until all equations are written in plain form. This defines the formula . Note that is not necessary to add any constraint on the fresh variables . Therefore, . The proposition follows. ∎
14. Virtually free groups
We restrict ourselves to the non-uniform complexity where the given virtually free group is not part of the input. The restriction allows us to ignore the way a virtually free group is given to us. For example whether the group is given by a context-free grammar for the word problem or whether it is given as a fundamental group of a finite graph of finite groups may result in uniform complexities which differ exponentially. We refer the interested reader to the arXiv version of [57] for more details. See also Rem. 14.8.
In the following denotes a fixed finitely generated virtually free group. Thus, there is a finitely generated free subgroup such that is finite. Replacing by the normal subgroup (which is of finite index in ) we can assume without restriction that is normal and that is a finite group. That is, we start with some surjective homomorphism where is finite and the kernel is a f.g. free group. This yields a short exact sequence:
[TABLE]
Choosing a generating set for and a set of coset representatives from , we obtain a generating set for . We need generating sets which are closed under involution, so we are more specific. We use the following definition.
Definition 14.1**.**
Let be given as in (58). We say that a subset of is a standard generating set for if the following conditions are satisfied.
- •
* can be written as a union .*
- •
* is a basis for , that is .*
- •
* for all .*
- •
* induces a bijection between and .*
- •
.
Every standard generating set is closed under the involution with . The three set , , and are pairwise disjoint subsets of . There is a bijection between and , but perhaps .
Let denote the canonical projection. We say that is in standard normal form if we can write where is a freely reduced word (that is without factors ) and . By we denote the set of standard normal forms. For every there is a unique such that in . The set of freely reduced words over becomes ; and we let . Hence,
[TABLE]
Theorem 14.2**.**
Let be a finitely generated virtually free group. Then with respect to any short exact sequence as in (58) there is a standard generating set and an algorithm which performs the following task. It takes as input a Boolean formula (according to Sect. 13.3) with such that is the th variable in some fixed chosen linear order on . The output is an extended alphabet of size , letters for all , and a trim NFA accepting a rational set of -morphisms over such that the EDT0L relation
[TABLE]
is equal to the full solution set in standard normal forms
[TABLE]
Moreover, if and only if ; and if and only if doesn’t contain any directed cycle.
Remark 14.3**.**
In a simplified analysis using a single parameter, the natural choice is to define . This yields
[TABLE]
If , then we have
[TABLE]
Remark 14.4**.**
Let us comment why we consider only a subset of the first variables of rather than all variables. The reason is that during the proof we manipulate in various ways including some which introduce fresh variables. But these new variables are just auxiliary symbols, and we make sure that they don’t enlarge the full solution set. If we introduce fresh variables, then we put them in the linear order behind the first variables. Therefore, there is no risk to denote as .
14.1. Proof of Thm. 14.2, Phase 1
Using Prop. 13.1 we may assume that all equations in are written in plain form as where . In the following we introduce many fresh variables into . The enlarged set is still called . Moreover, we choose a subset of positive variables such that , , and .
Having this, we push all negations to the atomic formulae using De Morgan’s law. This increase the size at most by the number of atomic formulae. For each inequality we introduce a fresh variable and then we replace by the conjunction . This increases the size by the number of inequalities since the singleton is accepted by a two-state NFA. Thus, without restriction doesn’t contain any negation and only three types of atomic formulae:
[TABLE]
Here, denotes an NFA of the form with . We may assume because for every NFA there is another NFA of the same size such that (the complement of ). We also write or because and therefore we can view directly as a rational subset of .
Lemma 14.5**.**
Let be as above. In particular, is free and is finite. It is enough to prove Thm. 14.2 under the following assumptions about the input formula .
- •
* implies (Note that the syntax makes sense since the f.g. free group is a rational subset in .)*
- •
If an NFA appears in , then where is an NFA over and the transitions are labeled with an arbitrary, but fixed, finite set of generators of .
- •
* is a conjunction where each atomic formula is either an equation in plain form with or or .*
Remark 14.6**.**
Assume that satisfies the assumptions of Lem. 14.5. Then Thm. 14.2 implies that there is standard set of generators containing a basis of such that
[TABLE]
In particular, the full solution set is an EDT0L relation over freely reduced words of .
The proof of Lem. 14.5 is based on two closure properties:
- finite unions of EDT0L (resp. rational) languages in a monoid are EDT0L (resp. rational); and
- if is an EDT0L (resp. rational) language and , then is EDT0L (resp. rational). The analogous statements hold for EDT0L relations.
Proof of Lem. 14.5.
The difficult part is to show the first and third item because we have to respect the given space bounds. The second item is very easy to show, and we prove it “on the fly” when showing the first item.
Let be any input formula for Thm. 14.2. We wish to add the constraint for all variables. This requires the introduction of fresh variables. More precisely, for each and we introduce a new variable with ; and we construct an NFA such that for each . The NFA is obtained by adding a single new final state and new transitions from the former final states to the new single one, all of them are labeled by the letter . The size of increases by a constant. Moreover, each function defines a new formula over the variables as follows: every occurrence of (resp. ) inside an equation is replaced by (resp. ) where . The length of each equation is at most doubled. Every constraint (resp. ) is replaced by the (resp. ). Recall that . Let denote the result of that transformation. Then we let
[TABLE]
Note that a constraint is the same as . Therefore we can use as a recognizing finite monoid for all . Since is of constant size, the size of is in . All variables in are of the form or . The old variables are still present but not used in any . Therefore, inside each we rename all by . After that the variables are superfluous: we remove them from . Thus, each uses the same set of as did.
Each formula is written again in disjunctive normal form where each index set has again (at most) exponential in the size of .
Having this, we see that is equivalent to the following disjunction
[TABLE]
Note that and use the same set of positive variables. It is also clear how to transform a solution for into a solution for and vice versa: if solves , then solves and if solves , then solves .
Since is a constant it is easy to see that the number of disjunctions in (63) is (at most) exponential in the size of . But it can also happen that the size of is exponential in the size of , so in general we have no way to store within the given space bound. What we do instead is to construct NFAs for each , one after another, such that defines the EDT0L relation of the full solution set for .
More precisely, suppose we have shown Thm. 14.2 for each which is a conjunction of constraints and equations. Then indeed, for all , one after another, we can output some NFA where the transitions are labeled by endomorphisms over (the same) extended alphabet such that
[TABLE]
We can also assume that all these NFAs use exactly the same set of distinguished letters . As an output of the overall algorithm we obtain the disjoint union over all these NFAs . Without restriction , but the elements of are not used in any NFA so far. Moreover, for each we may assume that there are letters , again still not used by any . We add one more new state and connect this new state with all final states in via a single transition labeled by the endomorphism which is defined by where corresponds to the variable and . The new state becomes the single final state of the “union” automaton.
We conclude that it is enough to show Thm. 14.2 for each . Since satisfies properties as required by Lem. 14.5, the lemma follows.∎
14.2. Proof of Thm. 14.2, Phase 2.
Embedding into a semi-direct product
Let be a finite set with involution. Then denotes the group . If the involution on is without fixed points, then we can write such that ; and the inclusion into induces an isomorphism between the free group with basis and . The group is called specular in [3], which means it is the free product of a free group with groups of order two.
In the following we use that is the fundamental group of a finite graph of finite groups [29], which enables us to reduce questions about equations with rational constraints in to questions about twisted word equations with rational constraints.
Suppose that the group acts on via a morphism . Thus, for we have and . We have and the action of on and defines two different (but related) semi-direct products and . The elements of (resp. ) are the pairs (resp. ) and the multiplication is defined by
[TABLE]
The semi-direct product is a monoid with involution by
[TABLE]
It is also clear that in the group .
The free monoid embeds into via and the group embeds into via . Having this, we obtain:
[TABLE]
Since we identify with and with , we can write:
[TABLE]
Thus, for , , and . Let and . Thus, the identity element in is identified with the empty word in . It also appears as a letter in . The interpretation as and as yields canonical surjective morphisms
[TABLE]
Our proof of Thm. 14.2 relies on Prop. 14.7.
Proposition 14.7** ([13], Sec. 2.4.5).**
Let be a finitely generated virtually free group and be a homomorphism onto a finite group such that the kernel is free. Then embeds into a semi-direct product of the form ; and we can construct an injective homomorphism and a partition into two subalphabets such that is isomorphic to . Moreover, using that isomorphism, we can embed into such that such that is freely reduced in . The embedding of into is also depicted in Fig. 9.
Proof.
The first assertion is the nontrivial direction in [13, Cor. 2.4.23]. The corollary says that is a free factor of . This means that is a free product of with . The additional property for all is a special case of [13, Prop. 2.4.22]. ∎
Remark 14.8**.**
As we deal here with non-uniform complexity, we content ourselves to know that the embedding can be effectively computed and therefore we can treat as a constant. But in fact the proof of Lemma 30 in the arXiv version of [57] shows
[TABLE]
Thus, if is given to us as the fundamental group of a finite graph of finite groups, then the interested reader could derive uniform complexity bounds from the material presented here.
Corollary 14.9**.**
We use the same notation as in Prop. 14.7. Define a morphism from onto by and for and . Then maps freely reduced words to freely reduced words in .
Proof.
The subgroup of is generated by words of the form where is freely reduced over . Thus, we can write every element in as a word
[TABLE]
such that for . Now, every freely reduced word can be obtained from some word as above by cancellation of factors . Since for , we obtain
[TABLE]
In particular, , and is freely reduced by definition. ∎
Remark 14.10**.**
Let us give a few more comments how Prop. 14.7 and Cor. 14.9 are shown in [13]. Since is a fundamental group of a finite graph of finite groups, it acts on its Bass-Serre tree without edge inversion [58]. As the notation suggests, is indeed a tree: a connected acyclic undirected graph. The same is true for the free subgroup of : it acts on as a graph automorphism without edge inversion. It follows that has trivial intersection with all vertex groups because the vertex groups are finite and embed into , see again [58]. So, if the intersection was not trivial, the would have a finite nontrivial subgroup, but free groups are torsion free. Thus, acts on without vertex stabilizers and without without edge inversion.
Now, let be the quotient graph . The finite group acts on : it permutes the edges and vertices of by respecting the incidence relation. Moreover, appears as the fundamental group of the finite and connected simplicial graph . This can be viewed as the main structure theorem about groups acting on trees, [58, Thm. 13]. That is, we can write . The point is that we always have two views on fundamental groups of a simplicial graph. The first view is to choose a base point and we write where is a set of paths from to . The second view is to choose a spanning tree of and we realize as . That is . The isomorphism between and is induced by the inclusion of into followed by the projection onto the quotient .
Let be the set of edges in . It is (in the sense of [58]) a finite alphabet: a finite set with involution without fixed points. Thus, we can view as a disjoint union with . As a set we identify with the regular set of reduced words in . Recall that a word is reduced if and only if no factor for appears. Since acts on the graph , each acts on via a length preserving automorphism which respects the involution. Hence, is reduced if and only if is reduced.
14.3. Proof of Thm. 14.2, Phase 3.
Transformation of to
Let be the input formula for showing Thm. 14.2. By Lem. 14.5 we may assume that where appears in (63). Thus, is given as a single conjunction of a special form where every variable is bounded by a constraint . It follows that the choice of for the standard generating set doesn’t effect from this point on. Therefore, we can write
[TABLE]
Next, we use the embedding of into the semi-direct product as given by Prop. 14.7 and Fig. 9. We are going to transform into a formula over such that the inclusion of into the semi-direct product defines a bijection between and .
We construct according to the following steps.
- (1)
We extend the embedding to an embedding and we replace every equation in by . Identifying , , and with subsets of , we see that generates the group . Hence, every equation can be written as a plain equation over the alphabet . As we have defined , we have . 2. (2)
We replace every which appears in by . That is . By assumption we have . Hence, is a rational subset of the free group .
Note that . Without restriction, we may assume that the transitions in are labeled by elements from . The property is not effected by that assumption. Let be the intermediate formula. It is clear that induces a bijection between and . 3. (3)
We transform each appearing in into an NFA such that first, and second, the transitions use labels from , and third . This well known by [56, 59], but not completely obvious. In Lem. 14.11 we give a slightly simplified proof for the special situation of semi-direct products.
Let be the corresponding formula. Since , we have .
The construction of is finished. We have
[TABLE]
Lemma 14.11** ([56, 59]).**
Let be an NFA with the property . Then there is an NFA such that where the transitions use labels from , and .
Proof.
In the beginning we let be any finite subset of . By Sect. 13.1 and perhaps by doubling the size of , we may assume that . Since and we may assume that . Thus, the label of every transition is either an element from or from or a product where and . Moreover, we may assume that is trim. In particular, if we reach a state when reading a word from an initial state, then there is a word such that . Now, . We let . This is well-defined as .
For every state with we introduce exactly one more state and transitions and This does not change the language accepted, and the NFA is still trim with . For each outgoing transition with and we have ; and there is some such that in and hence, we add a transition as depicted in Fig. 10.
This doesn’t change the language accepted as in . The larger NFA still accepts , but the crucial point is that for we can accept the same element in by reading just labels from . This is easy to see by induction on . Now, we remove all original states (they are no longer needed) and make initial (resp. final) if and only if was initial (resp. final), to obtain the NFA . By construction, we have . This implies . Recall that is well-defined up to a multiplicative constant only by (54). This makes independent of the choice of a finite generating set. ∎
14.4. Proof of Thm. 14.2, Phase 4.
From to : applying the techniques of Benois
The transformation in this subsection doesn’t effect the equations in . We only change the NFAs such that they accept with every word also the word which is obtained by canceling all factors . Nevertheless the rational subset will not change. The techniques for the transformation is well known by the work of Michèle Benois [2]. Therefore we call the new formula . We will see that . For convenience of the reader, we explain the transformation in detail. We use notation from string rewriting.
For we write if and for some and . By we mean the reflexive and transitive closure of . Clearly, implies . Moreover, implies for some .
By we denote the set of freely reduced words over ; and we identify with the regular set . These a words without any factor where or, equivalently, the set of words such that implies . The identification as sets is possible because yields a bijection from onto .
The formula uses NFAs where the transitions are labeled by letters from or by the empty word , see Sect. 14.3. The interpretation so far is that denotes a rational subset in . Now, we switch the viewpoint: denotes a regular subset in ; and we replace all constraints (resp. ) by (resp. ). This is nothing but a change of notation, so we call the new formula still . However, we now on we consider the full solution set as a relation over . Thus, a solution is given as a morphism . Recall that the “actual” solution over the group is therefore given by .
Lemma 14.12** ([2]).**
Let an NFA which appears in . Thus, and . Then we can transform into an NFA such that , , and
[TABLE]
Proof.
Let an NFA over where . We run the following while-loop.
While there there are a letter and states such that but enlarge by the -transition .
The while-loop terminates after at most rounds with the desired NFA . The number of states is same as before.
The inclusion is trivial. The converse follows by induction on the length of . Moreover, for each there is a (unique) such that . This shows (70) and hence the lemma. ∎
Let us define a new formula in two steps:
- (1)
Every constraint (resp. is replaced by (resp. where is the NFA constructed in Lem. 14.12. Let be the new formula. 2. (2)
Define by
[TABLE]
Lemma 14.13**.**
*Let satisfy the properties in Lem. 14.5. Then the embedding induces a bijection between and
. Moreover, .*
Proof.
The proof is immediate by (69), (70), and the construction of which makes sure that all variables satisfy the constraint . Thus a constraint is equivalent to a constraint and a constraint is equivalent to a constraint . ∎
14.5. Proof of Thm. 14.2, Phase 5.
Switching from NFAs to finite monoids: From to
The goal is to reduce the proof Thm. 14.2 to Thm. 4.3. This requires that we represent regular constraints by recognizing morphisms. In the following a guess means to run deterministically over all possibilities. That is, there is deterministic transducer which respects the space bound in Thm. 14.2 and produces all possible outputs one after another. The corresponding EDT0L relations are calculated separately and then everything is put together as we did when we split into formulae in (63).
Let be the list of NFAs which appear in . We have and without restriction . According to Ex. 2.1 there is a morphism to an -monoid of size such that where . Since , the monoid is of constant size. For the other constraints we cannot expect such a small recognizing monoid, and we use Boolean matrices instead. For let be the number of states of the NFA . According to Sect. 2.6 and Ex. 3.1 in Sect. 3 we find for each a morphism to a morphism to a monoid with involution of size such that where for a negative constraint and for a positive constraint. Recall that the monoid is a submonoid of . Let be the direct product . Let the canonical projection, Then we obtain a single morphism such that for all .
Now, for each we guess a value . Each time we make a guess we check that it is consistent with the constraints. Thus, for each and each we do the following. If there there a positive constraint , then we check . If there is a negative constraint , then we check . If the guess is not consistent, then the guess is not successful and the corresponding output is empty.
For a consistent guess we define the following formula
[TABLE]
Here, is the set of equations which appear in the conjunction . By a slight abuse of language we call a conjunction as in (72) still a Boolean formula. It is clear what we mean by a solution of , it is given by morphism such that
- (1)
for all . 2. (2)
for all .
For an inconsistent guess we let . Using this interpretation we have
[TABLE]
The size of the finite monoid is in . Thus, in general we cannot store the disjunction over all guesses in . So, we produce the required NFAs for each again one after another. We are approaching our goal prove Thm. 14.2. For that we use the following proposition.
Proposition 14.14**.**
Let satisfy all conditions in Lem. 14.5. Then there is an algorithm which performs the following task. It takes as input a Boolean formula
[TABLE]
which appears as in (72), The output is an extended alphabet of size , letters for all , and a trim NFA accepting a rational set of -morphisms over such that the EDT0L relation
[TABLE]
is equal to the full solution set in freely reduced words
[TABLE]
Moreover, if and only if ; and if and only if doesn’t contain any directed cycle.
14.6. Proof of Prop. 14.14
In the proof of Prop. 14.14 we wish to apply Thm. 4.3. In order to do so, we define another parameter by the following equation.
[TABLE]
Recall that by the definition in Sect. 2.1. Therefore we have:
[TABLE]
Hence, for the proof we can use the space bound which is in the form we need for Thm. 4.3.
14.6.1. From to the system
Let be written as in (74). Then we define to be the following system of equations (without any constraint)
[TABLE]
Recall that we have defined morphisms and . We join and to a morphism by letting for and for .
The group acts on , but neither on nor on . Therefore we perform two steps. First, we embed the set of variables into a larger set of twisted variables
[TABLE]
In order to have an embedding we identify with .
The group acts freely without fixed points on by and . In this way every morphism extends uniquely to an -compatible morphism .
Second, we embed into a larger -monoid as constructed in Sect. 3.2. Moreover, using the universal property of the -monoid , we extend uniquely to a morphism of -monoids by . Twisted variable of the form appear in only if , but formally the set of variables is now and for each variable the value is defined. The morphism is respects the involution and the action of , so does every solution .
We define the system by the system with the set of variables and where for each there is a constraint .
14.6.2. Triangulation: From to
The “problem” with the system is that equations are written as words where . In a twisted word equation the and should be words over .
Now, let be any word. We intend to move letters to the right. If contains a factor with , then we replace by the letter if in . Whenever we see a letter , then we remove it. If contains a factor where and , then we replace it by where corresponds to the letter according to (65). Since is letter moves to the right without increasing the length of . The last rule is that we replace every factor with and by . Again, moves to the right without increasing the length. Thanks to this rule twisted variables other than appear in the equations. Thus, every with can be written as such that , , and .
Moreover, if is any morphism, then and . Since and , we have only if . Thus, whenever we find , then we can stop: there is no solution. On the other hand, for we have . Hence, we can replace the equation by and is a twisted word equation over in twisted variables and with regular constraints defined by an compatible morphism .
Using standard techniques as described in Sect. 5.4 we can assume without restriction that all equations are in triangular form. The number of fresh (twisted) variables and the increase of the length over all equations is thereby bounded by . The set of variables is still called and the set twisted variables is still called . Thus after the modifications above and triangulation we obtain the system of twisted word equation with regular constraints . We have and all equations have the form
[TABLE]
where is a variable, , and . For example, we could have and . Then the equation becomes . The triangular form is convenient to achieve the property that solutions are in freely reduced words.
14.6.3. From to : solutions in freely reduced words
This subsection mimics [10] in the context of virtually free groups. will be the “final” system in the sequence of transformations. Recall that denotes the regular subset of freely reduced words. Clearly, if and , then , too. Another crucial observation is that for all freely reduced words and we have in if and only if there are freely reduced words such that
[TABLE]
According to (77) every equation in the triangular system has the form . For each such equation and each we introduce six fresh twisted variables
[TABLE]
After that we replace the equation by the conjunction of three new equations:
[TABLE]
For simplicity, the new set of twisted variables is still called .
We obtain a system , and this finishes the construction of the new formula . Let be any compatible morphism such that . Then we there is some such that first, , and second solves the three equation in (78) in freely reduced words. That is solves the three equation under the constraint for all . For the other direction: if solves the three equations in without any constraint on twisted variables, then there is some such that solves the equation in . The remaining problem is that our formalism asks to define values for each new variables. (That is of all variables). The only way to do so in the given space bound is to guess the correct value. We can write the equations appearing in as a system
[TABLE]
where and is already fixed. We can read this system as a system of equations over the finite monoid . To check whether such systems have a solution is actually hard, however we don’t need -hardness. It is enough that within our space bound we can output by guessing-and-checking all possibilities to assign values to each of the fresh twisted variables. Such an assignment is again a tuple . Formally we can write a as a disjunction
[TABLE]
Some of the systems can be empty. If all are empty, then we can stop: is not solvable.
Lemma 14.15**.**
Let satisfy all conditions in Lem. 14.5. Then there is an algorithm which performs the following task. It takes as input a Boolean formula non-empty system from the disjunction in (80).
The output is an extended alphabet of size with , letters for all , and a trim NFA accepting a rational set of -morphisms over such that the EDT0L relation
[TABLE]
is equal to the full solution set in freely reduced words
[TABLE]
Moreover, if and only if ; and if and only if doesn’t contain any directed cycle.
Proof.
The existence of the NFA with the desired properties is a formal consequence of Thm. 4.3. For the complexity issues we need an estimation of . It is however clear from the construction that we have
[TABLE]
where was defined in (4) and was defined in (75).
is due to (76). Thus the complexity follows again by Thm. 4.3. ∎
We did various modifications to the input formula to arrive at a system mentioned Lem. 14.15. Each step on the way from to involved a splitting or guessing, which are realized by transducers respecting the space bound. In order to define the NFA which is needed for Prop. 14.14, we put all the pieces together. Thus, Prop. 14.14 is shown.
Corollary 14.16**.**
Let be a finitely generated virtually free group given by a short exact sequence as in (58) and let the embedding of into a semi-direct product as in Fig. 9.
Then there is an algorithm which performs the following task. It takes as input a Boolean formula . The output is an extended alphabet of size with , letters for all , and a trim NFA accepting a rational set of -morphisms over . The corresponding EDT0L relation
[TABLE]
satisfies the following properties.
- (1)
We have . Thus, each for each and the word is freely reduced. 2. (2)
We have .
Proof.
As above we can use the same techniques of splitting and guessing based on (69), (71), and (73). Hence it is possible to construct the NFA by putting exponentially many NFAs of the form provided by Prop. 14.14. Again we may use a transducer which satisfies the required space bound since all pieces can be constructed one after another. ∎
14.7. Proof of Thm. 14.2. From the NFA back to .
We have and in Sect. 14.2 we defined an -morphism by for all . Since we see for all . See the commutative diagram in Fig. 11. Therefore, the second statement in Cor. 14.16 yields
[TABLE]
The first statement says that is an EDT0L relation in freely reduced words over ; and Cor. 14.9 asserts that maps freely reduced words to freely reduced words over . Using one state more than the NFA (actually a new initial state) and a transition labeled by from the old initial state to the new one, we obtain the desired NFA . Hence, we can realize as an effective EDT0L relation in freely reduced words over . Thus, the projection yields a bijection between and the full solution set . This concludes the proof of Thm. 14.2.
15.
In this section we apply our results to the perhaps most prominent example of a (non-free) virtually free group: the special linear group of matrices over . It is well known that is isomorphic to the amalgamated product . Possible generators to establish the isomorphism between and are the matrices and of orders and respectively. We have . We also denote the matrices and as and respectively.555Typical proofs for use a “ping-pong-argument” for a faithful action of the projective linear group on . When working with algebraic problems over , like solving equations, it is more natural that the constants are just matrices (with entries written as binary numbers) rather than words over a finite generating set. Moreover, there is no reason to see a sum or a factor of two matrices and because we would add or multiply the matrices together. For a matrix in we let ; and we define its binary size
[TABLE]
Note that is the usual matrix one-norm of the matrix . We use the notion of binary size to define the size of equations and Boolean formulae where constants are matrices. The only difference is that the size of a constant in is not as for a finite generating set, but . We leave it to the reader to define the size of a Boolean formula accordingly. To have a notation for Boolean formulae as well, we denote the new size by .
The aim of this section is to prove the following result.
Corollary 15.1**.**
There exists a generating set for of letters, and an algorithm which performs the following task. It takes as input a Boolean formula where the constants are matrices over (counted in their binary size) and in variables from such that and , where each variable has size for simplicity. The output is an extended alphabet of size , letters for all , and a trimmed NFA accepting a rational set of -morphisms over such that the EDT0L relation
[TABLE]
is equal to the full solution set in standard normal form as given in (57)
[TABLE]
Moreover, if and only if ; and if and only if doesn’t contain any directed cycle.
The proof of Cor. 15.1 covers the rest of the section. In a first part, we make the reduction to the framework of Thm. 14.2 fully explicit. The main message is that a few elementary facts are enough to apply Thm. 14.2 to without any reference to Bass-Serre theory [58] with the resulting black box Prop. 14.7. In fact, what we use about predates the invention of Bass-Serre theory. For that we reformulate Thm. 14.2 for in Cor. 15.1. The point is that we view Cor. 15.1 directly as a corollary to Thm. 4.3.
In the second part we show that working with matrices doesn’t increase the complexity. To see the difference, let be a word in the (symmetric) set of natural generators with , and let denote its image in , then a straightforward calculation shows , where is the nd Fibonacci number. In particular,
[TABLE]
This means that working with matrices and their binary size doesn’t increase the input size with respect to the reduced word lengths over . However, an exponential gap between and is possible. For example, we have and It is easy to see that is the shortest word in which represents the matrix . Thus, the matrix representation of (shortest) words can lead to an exponential compression. However, in [21] Gurevich and Schupp give an exponential representation of a matrix in by words over where the bit complexity of the exponential representation is linear in . (In an exponential representation exponents over factors are written in binary.) In order to prove the lemma of Gurevich and Schupp we use the matrices and in Sect. 15.2.
15.1. Explicit embedding of into a semi-direct product
Throughout, we use and we work with and its quotient . The group is the modular group666Note that is not the derived subgroup . which is frequently denoted as in the literature. There are natural actions of and (and hence of and ) on the complete bipartite graph . The actions are defined below and the graph is depicted in Fig. 12. We give an orientation to the set of undirected edges in according to that picture777Actually, is the quotient graph of the Bass-Serre tree for modulo the action by that group. Fig. 12 as well as some subsequent calculations appear in [13], too.. Denoting the set of directed edges , we obtain an alphabet . As usual, an undirected edge is two-element set .)
Let us write and where and . The action of on the bipartite graph is as follows. The generator (resp. ) stabilizes the vertices for , and we let with . Thus, and are transpositions. The elements and are rotations. Both stabilize the vertices and , and we let (with ). The action of is faithful, and its image in the is the direct product . Thus, acts on by identifying the action of with the action of and by identifying the action of with the action of .
This leads to surjective homomorphisms and by and . Note that is a homomorphism since . Moreover, induces an isomorphism between the kernel of the canonical projection of to (which is the center of generated by ) and the the kernel of the canonical projection of to . Thus, the mapping and induces a canonical isomomorphism between the kernels and by Fig. 13.
The following proposition is well-known. It is stated in [41, Lem. 1] (without proof) since, according to the author Morris Newman, Prop. 15.2 it is based on a more general result by Jacob Nielsen [42]. For the proof of Prop. 15.2 one might use the structure of as an amalgamated product as well as the well-known fact that the matrices and generate a free subgroup in . However, in the spirit of the paper, let us give a purely combinatorial proof of Prop. 15.2 using the structure of as a free product of and .
Proposition 15.2**.**
The kernel of is the commutator subgroup of is a free group of rank two, which is generated by the commutators and .
Proof.
Clearly, . We have and . Let us show first that is a normal subgroup in . Indeed:
- (1)
. 2. (2)
. 3. (3)
.
This implies that is the normal subgroup generated by the commutator . By definition, . Hence, is generated by two elements.
Second, we claim . We know
[TABLE]
Since induces a surjective homomorphism , this induced homomorphism is an isomomorphism.888More generally, if is a free product of two cyclic groups, then is equal to the kernel of the canonical projection of to the direct product . Hence, the claim.
The commutator subgroup is henceforth denoted by . We wish to show that is free. For that step let be three letters such that in and be four letters. Using we obtain a homomorphism . Let us define the letters and as the words and in . The aim is to show the restriction of to defines an isomomorphism . Since and generate , we content ourselves to show that a nonempty freely reduced word in is not mapped to . In we use the reduced normal form which is obtained by a confluent and length-reducing rewriting system which replaces , , and by and which replaces by and by .
We claim that we can detect the last letter of by knowing the last four letters in the reduced normal form of . This is clear for . Hence, we may assume that with and that the claim is correct for words of length at most . For that we define a finite automaton with eight states and transitions which are labeled by the letters , , , and . Those transitions where the label differs from the target are given by the following list:
- (1)
2. (2)
3. (3)
4. (4)
5. (5)
6. (6)
7. (7)
8. (8)
We don’t define initial or final states. Since we intend to read only freely reduced words, each state has out degree . Hence, there are transitions but only of them are listed in the table above. The automaton is deterministic. Consider a non-empty freely reduced word with and . After reading we are in the corresponding state. Hence, the claim is correct for . For example, if , then we are in the state which is the left-hand side in line (2). For we can assume by induction that the state of the left-hand side in the corresponding represents the last four letters in the reduced normal form of . For example, assume the state is the left-hand side in line (6) which is the right-hand side in line (7). This implies . Therefore . If , then reading leads to the state . If , then reading leads to the state . If , then reading leads to the state . Thanks to symmetries, the same type of argument applies in all situations. Since after reading the word we are in a state where the reduced normal form has length , it is not in . Hence, the proposition. ∎
Corollary 15.3**.**
The kernel of is the commutator subgroup of is a free group of rank two, generated by the commutators and .
Proof.
We know that the mapping to and to defines a homomorphism from to . This homomorphism maps to and to which yields an isomomorphism between and , see Fig. 13. Hence, the statement about the commutator subgroup for follows from Prop. 15.2. ∎
The action of on induces a faithful action on the set of directed edges which respects the involution. For example: , , and etc. Therefore, the canonical homomorphism yields a semi-direct product . The action of on is not faithful: for all and we have . In the next step let us show that is the fundamental group of the graph . Simultaneously, we will derive the desired result that embeds into the semi-direct product where and . We choose a spanning tree of by the solid edges in according to Fig. 12, and we let be a base point in . Then the fundamental group (which is, by definition, a subgroup in ) can be identified with the free group of rank . The identification is due to the fact that are the chords for the chosen (directed) spanning tree . Indeed, the isomorphism is given by
[TABLE]
To see this, say for , just follow the shortest path in from to the source of , traverse the chord and choose the shortest path in back to . Consider the canonical projection which maps the edges of to . Then is the identity on .
Define by and . It is an isomomorphism by Cor. 15.3.
Finally, guided by and we define a homomorphism where
[TABLE]
The homomorphism is well-defined since
[TABLE]
Another direct calculation shows
[TABLE]
Thus, the identity factorizes as follows:
[TABLE]
As a consequence, we obtain a commutative diagram Fig. 14 where we let . Since is bijective, is injective. Hence, induces an isomomorphism between and the subgroup .
Since is a finitely generated subgroup, is a rational subset in . Hence, we can reduce the question about solving equations in to twisted word equations over with rational constraints.999This is the approach of [7] to solve word equations in virtually free groups, too. However, Thm. 4.3 is more ambitious. In order to apply Thm. 4.3 we need in particular, an explicit construction of a set of standard generators. We obtain such a set by defining where and . We have and becomes a self-involuting letter in .
Remark 15.4**.**
Let , , and be letters in . Then the element has length . The corresponding element in standard normal form is which has length . This yields a concrete example showing that the standard normal forms are not geodesic, in general.
15.2. Euclidean matrix calculation
For the proof of Cor. 15.1 it remains to show that the complexity is not worse than . This is done next. We have and hence, . Since , generate as a monoid, we see that generate as a group. It is therefore clear that every matrix in can be written as a word in , but of course the representation is not unique as for example .
Let with . Using the extended Euclidean algorithm for computing the we define natural numbers for and with
[TABLE]
such that for we have
[TABLE]
The sequence finishes with some such that and . The last value is therefore indeed . We say that is the -sequence defined by . Note that together with uniquely define . Note also that for and .
By we mean the following submonoid of :
[TABLE]
It is a well-known classical fact and not difficult to see that is a free monoid with unique basis , see for example [12, Chap. 8.12] or [28] for an application to fast randomized pattern matching. The following quantitative lemma belongs probably to folklore. It can be easily derived from [21], but for lack of a reference for the precise statement we give a proof.
Lemma 15.5**.**
Let with and let be the -sequence defined by . Then there is a (unique) such that following assertions hold.
- (1)
. 2. (2)
If is even, then
[TABLE] 3. (3)
If is odd, then and
[TABLE]
Proof.
For the following we don’t need the uniqueness of . It follows from the fact that forms a basis for the free monoid , which in turn follows easily from the present proof. We leave this part to the interested reader.
Consider a matrix with . Note that this implies . Moreover, because . (The case is possible only for .) Let us treat the case as a special case first. That is: . We obtain and
[TABLE]
Moreover, . Since we have .
For the rest of the proof we may assume . We let (and ) be the -sequences defined by . Next, we define matrices for according to the following rules.
- (1)
If and is odd and is defined, then we let
[TABLE] 2. (2)
If and is even and is defined, then we let
[TABLE]
It follows by induction that for all . Having this we can deduce, again by induction, for all :
[TABLE]
The situation for the is slightly different. For for all
[TABLE]
To see (87) we observe that . Hence, we can use (86) to conclude (87). Considering shows the first claim in the lemma, because (87) implies and by and (84).
For the last matrix is and depending on whether is odd or even, we have two options. If is even we let and otherwise. We obtain:
[TABLE]
First case. Let be even, hence . Then we have
[TABLE]
It is possible that in the line above.
Second case. Let be odd, hence . Then we have
[TABLE]
Note that for odd, we have and . Using (88) and a case distinction (whether or not is even) yields the result. ∎
Proposition 15.6** (Gurevich and Schupp [21]).**
Let and . Then there are words and positive integers with such that
[TABLE]
Proof.
As a preamble let us note that we will be able to enforce because is a short word over and .
The assertion is trivial for . Hence we assume . Using short words , we obtain a matrix
[TABLE]
with and . Since it is enough to see that we can choose and where the exponents are in . We have and therefore the result follows from Lem. 15.5. ∎
Proof of Cor. 15.1
Prop. 15.6 shows that the size of the exponential expression
[TABLE]
is linear in . Thus, we can apply Cor. 14.16 based on the explicit embedding of into the semi-direct product as depicted in Fig. 14.
Acknowledgments
The authors are indebted to anonymous reviewers for their careful reading and extremely helpful feedback on the initial submission of this manuscript. We also thank Armin Weiß for various suggestions and Igor Potapov for pointing out the paper [21] of Gurevich and Schupp.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] P. R. Asveld. Controlled iteration grammars and full hyper-AFL’s. Information and Control , 34(3):248 – 269, 1977.
- 2[2] M. Benois. Parties rationelles du groupe libre. C. R. Acad. Sci. Paris, Sér. A , 269:1188–1190, 1969.
- 3[3] V. Berthé, C. D. Felice, V. Delecroix, F. Dolce, J. Leroy, D. Perrin, C. Reutenauer, and G. Rindone. Specular sets. Theoretical Computer Science , 684:3–28, 2017.
- 4[4] R. V. Book, T. J. Long, and A. L. Selman. Quantitative relativizations of complexity classes. SIAM J. Comput. , 13:461–487, 1984.
- 5[5] L. Ciobanu, V. Diekert, and M. Elder. Solution sets for equations over free groups are EDT 0L languages. International Journal of Algebra and Computation , 26:843–886, 2016. Conference abstract in ICALP 2015, LNCS 9135 with full version on Ar Xiv e-prints: abs/1502.03426.
- 6[6] L. Ciobanu and M. Elder. Solutions sets to systems of equations in hyperbolic groups are EDT 0L in PSPACE. In C. Baier, I. Chatzigiannakis, P. Flocchini, and S. Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019) , volume 132 of Leibniz International Proceedings in Informatics (LIP Ics) , pages 110:1–110:15, Dagstuhl, Germany, 2019. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
- 7[7] F. Dahmani and V. Guirardel. Foliations for solving equations in groups: free, virtually free and hyperbolic groups. J. of Topology , 3:343–404, 2010.
- 8[8] V. Diekert. Makanin’s Algorithm. In M. Lothaire, editor, Algebraic Combinatorics on Words , volume 90 of Encyclopedia of Mathematics and Its Applications , chapter 12, pages 387–442. Cambridge University Press, 2002.
