Unification on Compressed Terms

Unification on Compressed Terms Author: Adri`a Gasc´on Director: Guillem Godoy M`aster en Computaci´o Departament de Llenguatges i Sistemes inform`atics (LSI) Setembre 2009 Contents 1 Introduction 5 2 Preliminaries 9 2.1 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.2 Terms, trees, and positions . . . . . . . . . . . . . . . . . . . . 10 2.3 Subterms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.4 Functions on terms . . . . . . . . . . . . . . . . . . . . . . . . 11 2.5 Substitutions . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.6 Contexts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.7 Unification and matching . . . . . . . . . . . . . . . . . . . . . 13 2.8 Representations for terms . . . . . . . . . . . . . . . . . . . . 15 3 First-order unification with STGs 22 3.1 Outline of the algorithm . . . . . . . . . . . . . . . . . . . . . 22 3.2 Computing the preorder traversal of a term. . . . . . . . . . . 24 3.3 Computing the first different position of two words. . . . . . . 24 3.4 Isolating variables . . . . . . . . . . . . . . . . . . . . . . . . . 26 3.5 Application of substitutions and a notion of restricted depth . 28 3.6 A polynomial time algorithm for first-order unification with STGs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 4 First-order matching with STGs 35 4.1 Outline of the algorithm . . . . . . . . . . . . . . . . . . . . . 35 4.2 Finding the first occurrence of a variable . . . . . . . . . . . . 36 4.3 A polynomial time algorithm for first-order matching with STGs 37 5 Conclusion & further work 38 2 Acknowledgements 1 Thanks to Guillem Godoy for introducing me to the world of research and showing me how to face interesting (and sometimes frustrating) problems with patience, passion, and most of all good mood. Thanks to my family for always being more proud of me than what I would actually deserve. 1Part of this work was supported by the FORMALISM project (TIN2007-66523), funded by the Spanish government. 3 Abstract First-order term unification is an essential concept in areas like functional and logic programming, automated deduction, deductive databases, artificial intelligence, information retrieval, compiler design, etc. We build upon recent developments in grammar-based compression mechanisms for terms and investigate algorithms for first-order unification and matching on compressed terms. We prove that the first-order unification of compressed terms is decidable in polynomial time, and also that a compressed representation of the most general unifier can be computed in polynomial time. Furthermore, we present a polynomial time algorithm for first-order matching on compressed terms. Both algorithms represent an improvement in time complexity over previous results [GGSS09, GGSS08]. We use several known results on the tree grammars used for compression, called singleton tree grammars (STG)s, like polynomial time computability of several subalgorithmms: certain grammar extensions, deciding equality of represented terms, and generating their preorder traversal. An innovation is a specialized depth of an STG that shows that unifiers can be represented in polynomial space. 4 Chapter 1 Introduction The task of solving equations is an important component of any mathematically founded science. In general, solving an equation s. =tconsists of finding a substitution σfor variables occurring in both expressions sand tsuch that σ(s) = σ(t). The range for the variables, the kind of expressions sand t, and their semantics, as well as the semantics of = depend on the context. By specifying some of these parameters we can define the well-known first-order term unification problem. The first-order unification problem In the context of this problem the expressions sand tare terms with leaf variables standing for terms, all function symbols are non-interpreted, and = is interpreted as syntactic equality. Intuitively, we can see terms as trees, the widely-used data structure. To be more concrete, we usually consider terms built of functions symbols f, g, a, b (where f and g are binary, and a,b are nullary), and variable symbols xand y. Therefore, the unification problem s. =tfor terms s=f(x, b) and t=f(a, y) is concerned to the question: is it possible to replace the variables x,yin sand tby terms such that the two terms obtained this way are (syntactically) equal? In this example, if we replace xby aand yby bthen sand tbecome equal, and we obtain an unified term, i.e. the resulting term after applying the substitution, f(a, b). Hence, the substitution {x7→ a, y 7→ b}is called a unifier for sand t. Robinson [Rob65] showed that the first-order Unification problem is decidable and that whenever a unifier exists, there always exists a most general unifier, i.e. a unifier such that every other unifier can be obtained by instantiation. Even more, in first-order unification, whenever this most general unifier exists, it is unique up to variable renaming. Robinson’s algorithm for 5 computing most general unifier requires exponential time and space in the worst case. A great deal of effort has gone into improving the efficiency of first-order unification. Among several other results, there are the ones by Venturini-Zilli [VZ75], reducing the complexity of Robinson’s algorithm to quadratic time, and by Martelli and Montanari [MM82], presenting a linear time algorithm for unification. The first-order matching problem The term matching problem is a particular case of term unification. It is characterized by the condition that one of the sides of the equation s. =t, say t, contains no variables. Like term unification, this is a common problem in areas like functional and logic programming, automated deduction, deductive databases, artificial intelligence, information retrieval, compiler design, etc. Variants In most applications of unification and matching, one is not interested just in the decision problem, which simply asks for a ”yes” or ”no” answer to the question commented above. A unification or matching algorithm should thus not only decide solvability of a given instance of these problems, but also either compute a most general unifier, i.e. a unifier such that every other unifier can be obtained by instantiation, or compute all solutions. The first-order term unification and matching problems are efficiently solvable, but their expressivity is often insufficient to deal with the current challenges in the areas mentioned above. For this reason, several variants and generalizations of these problems have been studied. Incorporating more complex interpretation of the function symbols and equality predicate under equational theories has been widely considered (see [BS94, BS01]). In this case, instead of requiring that the terms are made syntactically equal, equational unification is concerned to make the terms equivalent with respect to a congruence induced by certain equational axiom E. For example, if E=f(a, a)≈g(a, a) , then the terms f(a, x) and g(x, a), which are not (syntactically) unifiable, are E-unifiable. Another extension of first-order unification is concerned with allowing other kinds of variables related to terms. This is the case of context variables, i.e. variables which can be substituted by contexts, which are terms with a single hole (syntactically, the hole is a special constant denoted by •). Context variables have arity one, hence they have 6 a subterm t. Once they are instanciated by a context, the hole denotes where thas to be inserted. For example, we say that the context unification equation F(f(h(a), h(a))) . =h(f(F(a), F(a))) has only one solution {F7→ h(•)}and the unified term is h(f(h(a), h(a))). The context unification instance F(f(x, b)) . =f(a, F(y)) has several solutions such as {F7→ f(a, •), x 7→ a, y 7→ b},{F7→ f(a, f(a, •)), x 7→ a, y 7→ b}, {F7→ f(a, f(a, f(a, •))), x 7→ a, y 7→ b}, and so on. The unified terms are f(a, f(a, b)), f(a, f(a, f(a, b))), and f(a, f(a, f(a, f(a, b)))) respectively. On the other hand, f(a, F (x)), and F(f(b, a)) are not unifiable. The context unification problem was first introduced by Comon [Com91] and its decidability still remains open. However, some particular cases has been already solved [SSS04, SS02, SSS02, LSSV06b, GGSS08]. Analogously to the firstorder case, the context matching problem is the particular case of context unification where one of the sides of the equation contains no variables. However, the extension of unification and matching treated in this work is concerned with reconsidering complexity issues for the first-order unification problem when applied to compressed input terms. In recent years there has been an increase of interest in compression mechanisms based on grammar representation, since other mechanisms can in general be efficiently simulated. These compression techniques were initially used for words [Pla95, Loh06, Lif07], and led to important results in string processing, with applications [HSTA00, GM02, LR06] in software/hardware verification, information retrieval, and bioinformatics. In that sense, Straight-Line Programs (SLP), or the equivalent formalism of Singleton Context Free Grammars (SCFG), are now a widely accepted formalism for text compression. Later, grammar-based compression was extended to terms/trees [BLM05, SS05, CDG+97] with applications on XML tree structure compression [BLM05] and XPATH [LM05]. STG-based compressors have already been developed [MMS08]. Essentially, an SCFG, i.e. a context free grammar where all nonterminals generate a singleton language, is used for representing single words, and similarly, every nonterminal in a singleton tree grammar (STG) represents one tree. An STG can succinctly represent terms/trees which are exponentially big in size and height. Efficient algorithms have been developed for checking whether two compressed inputs represent the same word/term [Pla95, Loh06, Lif07], and for finding occurrences of one of them within the other (fully compressed pattern matching)[KRS95, KPR96, MST97, Lif07]. Recently, it was shown that tree grammars using multi-hole-contexts are polynomially equivalent to STGs [LMSS09]. STGs have also been used for complexity analysis of unification algorithms in [LSSV06b, LSSV06a], and the context matching problem [GGSS08]. 7 Overview of results obtained in this work In [GGSS09], and in [GGSS08], there were presented polynomial time algorithms for first-order unification and matching , in both cases with terms represented with STGs. As a nobel contribution we describe, in Chapter 3 and Chapter 4 respectively, faster algorithms for this two problems. Moreover, we believe that the presented solutions represent also a gain in simplicity which makes them easily implementable. 8 Chapter 2 Preliminaries In this chapter the necessary concepts and definitions in the scope of this work are introduced. Most of the basic definitions and explanations regarding terms and term unification were borrowed from [CDG+97], [Vil04], and [BS01]. 2.1 Terms Terms allow the representation of data with substructure. A term is either: •A constant symbol •A variable •A compound term A compound term consists of a function symbol applied on a sequence of one or more terms called arguments. It sometimes helps to think of a compound term as a tree structure. Example 2.1.1 The formula f(+(1, x),∗(3,4),−(5, y)) could be depicted as the structure: f + * - 1x3 4 5 y where f,+,−and ∗are function symbols, 1,3,4and 5are constants, and x, yrepresent variables. 9 f f . . . f a b Figure 2.3: Encoding using dags of term in example 2.8.2 but have lots of common subterms, like t1=f(a, b), t2=f(t1, t1),...,tn= f(tn−1, tn−1), then one would require exponential space using the term representation to represent tn, whereas a directed acyclic graph (dag) representation requires linear space because of the reusement of the nodes. Hence, dags allow to represent terms of exponential width in linear space. Example 2.8.2 Given the set of equations {t1=f(a, b),t2= f(t1, t1),...,tn=f(tn−1, tn−1)}, using a dag to represent tnprovides an efficient encoding as shown in figure 2.3. One of the reasons for the exponential execution time of Robinson’s algorithm is the exponential size increase of the terms to be unified due to instantiation of variables. The dag structure for term representation is used in later algorithms to keep the size of this terms linearly bounded. Furthermore, note that since each node in a term-dag has an interpretation as a term, once two subterms are unified they are represented by the same node, which helps to avoid repeated calculations. 2.8.2 Grammars In this work we consider singleton tree grammars (STG) for term compression. This kind of grammars are a generalization of singleton context-free grammars (SCFG) [LSSV04, Pla94], which can only generate strings, extending the expressivity of SCFGs by terms and contexts. This is consistent with [BLM05], and also with the context free tree grammars in [CDG+97]. However, the latter are slightly more general in permitting contexts with several holes. 16 First of all it is necessary to define the well-known Context-Free Grammars (CFG). Then, by making a restriction on the form of the rules we define Singleton Context Free Grammars (SCFG), and finally, by extending SCFG to represent terms we introduce Singleton Tree Grammars (STG). Definition 2.8.3 A context-free grammar is a quadruple G= (V, Σ, P, S) where Vis a finite set of variables (nonterminals), Σis a finite set of terminals disjoint with V,S∈Vis the start symbol and Pis a finite set of production rules of the form Z→αwhere Z∈Vand α∈(V∪Σ)∗. A rule Z→αis called a Z−rule. Example 2.8.4 A context-free grammar for the language consisting of all strings over {a, b}for which the number of a’s and b’s are different is: S→U S →V U→TaU U →T aT V→TbV V →TbT T→aTbT T →bTaT T→λ Here, the nonterminal Tcan generate all strings with the same number of a’s as b’s, the nonterminal Ugenerates all strings with more a’s than b’s and the nonterminal Vgenerates all strings with fewer a’s than b’s. The symbol λdenotes the empty string. As we can see in the example above, the non terminals T, U, V are recursive. For this reason, arbitrarily long strings may be generated. Furthermore, due to that recursivity and to the fact that there is more than one rule containing a given non terminal in its left-hand side, every non terminal can generate more than one string. SCFGs are called singleton because each non terminal generates just one string. Definition 2.8.5 Asingleton context free grammar (SCFG) is a nonrecursive context-free grammar such that for every nonterminal Zthere is exactly one Z−rule. Then every non-terminal Zgenerates just one word, denoted wZ, and we say that Zdefines wZ. We do not distinguish a particular start symbol. Hence, a singleton context-free grammar is defined as a 3-tuple G= (V, Σ, P ), analogously to context-free grammars. Alternatively, SCFGs are defined in a different way. They contain variables X1,...,Xnwhere every variable Xioccurs in a left hand-side of exactly one rule of the form either Xi→c, for some c∈Σ, or Xi→XjXk, for some j, k < i. Note that, with this alternative definition, SCFGs are in Chomsky Normal Form. 17 Now we can define singleton tree grammars (STG) as an extension of the already presented SCFGs in order to capture terms and contexts. Note that SCFGs can be obtained from STGs for the case of a monadic signature, i.e. all function symbols have arity one except for one constant. Definition 2.8.6 Asingleton tree grammar (STG) is a 4-tuple G= (T N,CN ,Σ, R), where T N is a set of tree/term non-terminals, or nonterminals of arity 0,CN is a set of context non-terminals, or non-terminals of arity 1, and Σis a signature of function symbols (the terminals), such that the sets T N,CN , and Σare pairwise disjoint. The set of non-terminals N is defined as N=T N ∪ CN. The rules in Rmay be of the form: •A→f(A1,...,Am), where A, Ai∈ T N , and f∈Σis an m-ary terminal symbol. •A→C1A2where A, A2∈ T N, and C1∈ CN . •C→ • where C∈ CN. •C→C1C2, where C, Ci∈ CN. •C→f(A1,...,Ai−1, Ci, Ai+1,...,Am), where A1,...,Ai−1, Ai+1,...,Am∈ T N ,C, Ci∈ CN , and f∈Σis an m-ary terminal symbol. •A→A1, (λ-rule) where Aand A1are term non-terminals. Let N1>GN2for two non-terminals N1, N2, iff N1→t, and N2occurs in t. The STG must be non-recursive, i.e. the transitive closure >+ Gmust be terminating. Furthermore, for every non-terminal Nof Gthere is exactly one rule having Nas left-hand side. Given a term twith occurrences of nonterminals, the derivation of tby Gis an exhaustive iterated replacement of the non-terminals by the corresponding right hand sides. The result is denoted as wG,t. In the case of a non-terminal Nwe also say that Ngenerates wG,N . We will write wNwhen Gis clear from the context. Note that we have used Σ instead of Ffor denoting the set of terminals of the grammar, although it is also a signature. We explain the reasons as follows. In this work, STGs are used for representing first-order terms and contexts. In particular, a terminal Aof a STG Ggenerates a term. If Σ was Fwe would be able to represent just ground terms. Thus, Σ must also contain first-order variables as terminals of arity 0. 18 Example 2.8.7 The terms in the equation s. =t, where s=f(g(a, b), h(x)), and t=f(h(b), g(a, x)), are generated by term non-terminals Asand At, respectively, in the following STG. As→f(A1, A2)At→f(A3, A4) A1→C1AbA3→C2Ab A2→C2AxA4→C1Ax C1→g(Aa, C.)C2→h(C.) Ab→b Ax→x C.→ • Aa→a A directed acyclic graph (dag) can be defined as a particular case of an STG (in fact, this representation is in direct correspondence with the classic implementation of graphs using adjacency lists). Definition 2.8.8 ADAG is an STG where the set of context non-terminals CN is empty, and moreover, there are only rules of the form A→ f(A1,...,Am). Example 2.8.9 Given the set of equations {t1=f(a, b), t2= f(t1, t1),...,tn=f(tn−1, tn−1)}, using a STG to represent tnprovides an efficient encoding (as shown in example 2.8.2 for the case of the dag representation). Tn→f(Tn−1, Tn−1) . . . T2→f(T1, T1) T1→f(A, B) A→a B→b Nevertheless, STG-represented terms may have exponential height in the size of the grammar in contrast to dags, which only allow for a linear height in the (notational) size of the dags as shown in the following example. Example 2.8.10 The term s=f2n(a)described by the following grammar would have exponencial height in a term or dag representation. s→CnAa Aa→a C.→ • C0→f(C.) C1→C0C0 19 C2→C1C1 C3→C2C2 . . . Cn→Cn−1Cn−1 Definition 2.8.11 The size |G|of an STG Gis the sum of the sizes of its rules, where the size of a rule N→uis 1 + |u|. The depth within Gof a non-terminal Nis defined recursively as depth(N) := 1 + max{depth(N′)|N′is a non-terminal in uwhere N→u∈G}and the maximum of an empty set is assumed to be 0. The depth of a grammar Gis the maximum of the depths of all nonterminals of G, and it is denoted as depth(G). Plandowski [Pla94, Pla95] proved decidability in polynomial time for the word problem for SCFG, i.e., given a SCFG Pand two non-terminals Aand B, to decide whether wA=wB. The best complexity for this problem has been obtained recently by Lifshits [Lif07] with time O(|P|3). In [BLM05, SS05] Plandowski’s result is generalized to STG. Since the result in [BLM05] is based on a linear reduction from terms to words and a direct application of Plandowski’s result, it also holds for the Lifshits result. Hence, we have the following. theorem 2.8.12 ([Lif07, BLM05]) Given a STG G, and two tree nonterminals A, B from G, it is decidable in time O(|G|3)whether wA=wB. Several properties on STGs are efficiently decidable. The following lemmas will be used all along the paper. Lemma 2.8.13 Let Gbe an STG. The number |wN|, for every non-terminal Nof G, is computable in time O(|G|). Proof. We give an alternative definition of |wN|recursively as follows. •if (N→f(N1,...,Nm)∈G) then |wN|= 1 + |wN1|+...+|wNm|, where N1,...,Nmare non-terminals of Gand fis a function symbol with ar(f) = m. •if N→C1N2then |wN|=|wC1|+|wN2| − 1, where C1is a context non-terminal and N2is a non-terminal of G. The correctness of the above definition can be shown by induction on the size of wN. Moreover, since the recursive calls in the definition of |wN|will be done, at most, over all the non-terminals of G,|wN|is computable in linear time over |G|using a dynamic programming scheme. 2 20 Lemma 2.8.14 Given an STG G, a terminal α, and a non-terminal Nof G, it is decidable in time O(|G|)whether αoccurs in wN. Proof. Whether αoccurs in wNcan be computed efficiently again using a dynamic programming squeme: note that αoccurs in wNiff either wN→α∈ G, or αoccurs in wN′for some non-terminal N′occurring in the right-hand side of the rule for N.2 21 Chapter 3 First-order unification with STGs In this section we prove that the first-order unification problem can be solved in polynomial time even when the input is compressed using STGs. Definition 3.0.15 The first-order unification problem with STG has an STG Grepresenting first-order terms and contexts as input, plus two term non-terminals Asand Atof Grepresenting terms s=wG,Asand t=wG,At. Its decisional version asks whether sand tare unifiable. In the affirmative case, its computational version asks for a representation of the most general unifier. Our algorithm generates the most general unifier in polynomial time and represented again with an STG. 3.1 Outline of the algorithm Given a STG Gas a compressed representation of two terms sand t, we compute a minimal index kin which pre(s) and pre(t) differ. At this point, if both pre(s)[k] and pre(t)[k] are function symbols, we terminate stating non-unifiability. Otherwise, either pre(s) or pre(t), say pre(s), contains a variable xat k. Note that, since the arity for the terminals in Gis fixed, the index kcorresponds to a unique position p∈Pos(s)∩Pos(t), as commented in Section 2.4.1. If xproperly occurs in the subterm of tat p, then we terminate, again stating non-unifiability. Otherwise, we replace xby the subterm of tat peverywhere, and re-start the process until both sand t become equal, in which case we state unifiability. 22 Input: An STG Gand term non-terminals Asand At. (we write sand tfor wAsand wAt). While sand tare different do: Look for the first position ksuch that pre(s)[k]6=pre(t)[k]. If both pre(s)[k]and pre(t)[k]are function symbols; Then Halt stating that the initial sand tare not unifiable // Here, either pre(s)[k]or pre(t)[k], say pre(s)[k], is a variable x. If xoccurs in t|p, where p=iPos(t, k), Then Halt stating that the initial sand tare not unifiable Extend Gby the assignment {x7→ t|p} EndWhile Halt stating that the initial sand tare unifiable Figure 3.1: Unification Algorithm of STG-Compressed Terms Note that, as commented in Section 2.7, our algorithm is just an adaptation of the algorithm defined in Figure 2.1 to the case where the inputted terms are compressed using STGs. Hence, the difficulties are induced by the task of performing all the operations mentioned above on the compressed representation of terms. In [BLM05] it was shown how to succintly represent the preorder traversal word of a term generated by an STG using an SCFG. We reproduce this construction in Section 3.2 to compute an SCFG PreGwith non-terminals Psand Ptgenerating pre(s) and pre(t), respectively. We also need to compute, given PreG, the minimal index kin which pre(s) and pre(s) differ. In Section 3.3 we show how to perform this task efficiently. Our approach is based on a recent result on compressed string processing [Lif07]. As commented above, kcorresponds to a unique position p∈Pos(s)∩Pos(t). In Section 3.4, we present the procedure to, given G and k, extend Gsuch that a new non-terminal generates t|p. Avoiding the explicit calculation of prefines the approach presented in previous work in STG-compressed first-order unification [GGSS09] in order to obtain a faster algorithm. We also need to apply substitutions once a variable is isolated. Performing a replacement of a first-order variable xby a term uis easily representable with STGs by simply transforming xinto a non-terminal xof the grammar and adding rules such that xgenerates u. However, since successive replacements of variables by subterms modify the initial terms, we have to show that this does not produce an exponential increase of the size of the grammar, since its depth may be doubled after each of these operations. To this end, we develop a notion of restricted depth, and show that its value is preserved along the execution, and that the size increase at each step can be 23 A→f(A1,...,Am)⇒ PA→fPA1...PAm A→C1A2⇒ PA→ LC1PA2RC1 A→A1⇒ PA→ PA1 C→C1C2⇒LC→ LC1LC2 RC→ RC2RC1 C→f(A1,...,Ai−1, Ci, Ai+1,...,Am)⇒LC→fPA1...PAi−1LCi RC→ RCiPAi+1 ...PAn C→ • ⇒ LC→λ RC→λ Figure 3.2: Generating the Preorder Traversal bounded by this restricted depth, which is shown in Section 3.5. 3.2 Computing the preorder traversal of a term. In [BLM05] it is shown how to construct, from a given STG G, an SCFG PreGrepresenting the preorder traversals of the terms and contexts generated by G. We reproduce that construction here, presented in Figure 3.2 as a set of rules indicating, for each term non-terminal Aand its rule A→αof G, which rule PA→α′of PreGis required in order to make the non-terminal PAof PreGsatisfy wPreG,PA=pre(wG,A). To this end, for each context nonterminal Cof Gwe also need non-terminals of PreGgenerating the preorder traversal to the left of the hole (LC), and the preorder traversal to the right of the hole (RC). It is straightforward to verify by induction on the depth of Gthat, for every term non-terminal Aof G, the corresponding newly generated nonterminal PAof PreGgenerates pre(wA). Lemma 3.2.1 Let Gbe a STG. A SCFG PreGof size O(|G|)can be constructed in time O(|G|)such that, for each non-terminal Nof G, there exists a non-terminal PNin PreGsatisfying wPreG,PN=pre(wG,N ). 3.3 Computing the first different position of two words. Given two non-terminals p1and p2of an SCFG P, we want to find the minimum index ksuch that wp1[k] and wp2[k] are different. In order to solve this problem, a linear search over the generated words wp1and wp2is not a 24 good idea, since their sizes may be exponentially big with respect to the size of P. Hence, one may be tempted to apply a binary search since prefixes are efficiently computable with SCFG and equality is checkeable in time O(|P|3), which would lead to O(|P|4) time complexity. However, we will use more specific information from Lifshits’ work [Lif07] to obtain O(|P|3) time complexity. Lemma 3.3.1 [Lif07] Let Gbe an SCFG. Then a data structure can be computed in time O(|G|3)which allows to answer to the following question in time O(|G|): given two non-terminals N1and N2of Gand an integer value k, does wN1occur in wN2at position k? Thus, assume that the pre-computation of Lemma 3.3.1 has been done (in time O(|P|3)), and hence we can answer whether a given wp1occurs in a given wp2at a certain position in time O(|P|). For finding the first different position between p1and p2, we can assume |wp1| ≤ |wp2|without loss of generality. Moreover, we also assume wp16=wp2[1..|wp1|], i.e wp1is not a prefix of wp2. Note that this condition is necessary for the existence of a different position between wp1and wp2, and that this will be the case when p1and p2generate the preorder traversals of different trees. Finally, we can assume that Pis in Chomsky Normal Form. Note that, if this was not the case, we can force this assumption with a linear time and space transformation. We generalize our problem to the following question: given two nonterminals p1and p2of Pand an integer k′satisfying k′+|wp1| ≤ |wp2|and wp16=wp2[(k′+ 1)..(k′+|wp1|)], which is the smallest k≥1 such that wp1[k] is different from wp2[k′+k]? (Note that we recover the original question by fixing k′= 0). This generalization is solved efficiently by the recursive algorithm given in Figure 3.3, as can be shown inductively on the depth of p1. By Lemma 3.3.1, each call takes time O(|P|), and at most depth(P) calls are executed. Thus, the most expensive part of computing the first different position of wp1and wp2is the pre-computation given by Lemma 3.3.1, that is, O(|P|3). Lemma 3.3.2 Let Pbe an SCFG of size n, and let p1, p2be non-terminals of Psuch that wp16=wp2. The first position kwhere wp1and wp2differ is computable in time O(|P|3). 25 and, since Vdepth(C1)<Vdepth(N), at most VdepthG(N)≤Vdepth(G) new non-terminals have been added in the construction of kext(G, N, k). Furthermore, since VdepthG(N) = 1 + max(VdepthG(C1),VdepthG(A2)), VdepthG′(A) = 1 + max(VdepthG′(N′),VdepthG′(A2)) and VdepthG(A2) = VdepthG′(A2), it also holds that VdepthG′(A)≤VdepthG(N)≤Vdepth(G). 2 3.6 A polynomial time algorithm for firstorder unification with STGs From a high level perspective the structure of our algorithm described in Section 3.1 is very simple and rather standard. Most algorithms for firstorder unification are variants of this scheme. They represent the terms with directed acyclic graphs (dags), implemented somehow, in order to avoid the space explosion due to the repeated instantiation of variables by terms. In our setting, those terms are represented by STGs. In fact, the input is an STG G, and two term non-terminals Asand Atrepresenting sand t, respectively. Since our algorithm is just an adaptation of the algorithm defined in Figure 2.1 to the case where the inputted terms are represented using STGs we will not argue about its correctness. In previous sections we showed how to efficiently perform all the required operations on STGs: Decide whether sand tare equal, generate a compressed representation for pre(s) and pre(t), look for the minimum index ksuch that pre(s)[k]6=pre(s)[k], construct the term t|p, where p=iPos(t, k), and replace the variable x=s|pby t|peverywhere. The algorithm runs in polynomial time due to the following observations. Let nand mbe the initial value of depth(G) and |G|, respectively. We define Vto be the set of all the first-order variables at the start of the execution (before any of them has been converted into a non-terminal). Hence, at this point Vdepth(G) = n. The value Vdepth(G) is preserved to be nalong the execution of the algorithm thanks to Lemmas 3.5.4 and 3.5.6. Moreover, by Lemma 3.5.6, at most nnew non-terminals are added at each step. Since at most |V|steps are executed, the final size of Gis bounded by m+|V|n. Each execution step takes time at most O(|G|3). Thus we have proved: theorem 3.6.1 First-order unification of two terms represented by an STG can be done in polynomial time (O(|V|(m+|V|n)3), where mrepresents the size of the input STG, nrepresents the depth, and Vrepresents the set of different first-order variables occurring in the input terms). This holds for the 32 decision question, as well as for the computation of the most general unifier, whose components are represented by the final STG. 3.6.1 Example of execution Let G= ({At, As, A, B1, B2, Ax, By},{C0, C1, C2, C3, C4, C., D}, {g, f, a, x}, R), where R={At→g(B1, A), As→g(B2, A), A →C4Aa, C4→ C3C3, C3→C2C2, C2→C1C1, C1→C0C0, C0→f(C.), C.→ •, Aa→ a, D →C3C2, B1→DBx, B2→C4By, Bx→x, By→y}, be an STG. Note that wG,At=g(f12(x), f16(a)), and wG,As=g(f16(y), f16(a)). Hence, hG, As . =Atiis an instance of first-order unification with STG. The goal is to find a substitution σsuch that σ(wG,As) = σ(wG,At). The set of rules of the SCFG PreGobtained by applying the rules of Figure 3.2. to Gis {PAt→gPB1PA,PAs→gPB2PA,PA→ LC4PAaRC4,PAa→ a, PB1→ LDPBxRD,LD→ LC3LC2,RD→ RC2RC3,PBx→x, PB2→ LC4PByRC4,LC4→ LC3LC3,LC3→ LC2LC2,LC2→ LC1LC1,LC1→ LC0LC0,LC0→fLC.,LC.→λ, RC.→λ, RC0→ RC.,RC1→ RC0RC0,RC2→ RC1RC1,RC3→ RC2RC2,RC4→ RC3RC3,PBy→y, }. Note that wPAt=gf12xf16aand wPAs=gf16af16a. The SCFG PreGis not in Chomsky Normal Form, but it is easy to adapt the algorithm of Figure 3.3 to this case. Thus, if we execute an adapted version of index(PAt,PAs,0,PreG), the following sequence of calls is produced: index(PAt,PAs,0,PreG), index(PB1,PAs,1,PreG), index(PBx,PAs,13,PreG). The third call returns 1, the second one returns 13, and the first one returns 14, which corresponds to the first different position of wPAsand wPAt. Note that iPos(wG,As,14) = 113. We compute now and extension kExt(G, As,14) of G, as described in Definition 3.4.1, such that a new term non-terminal A′ sgenerates wAs|113 . We obtain the following set of rules, where rules in bold correspond to the added non-terminals due to the kext constructions w.r.t to the STG Ggiven as input: {A′ s→C2By, At→ g(B1, A), As→g(B2, A), A →C4Aa, C4→C3C3, C3→C2C2, C2→ C1C1, C1→C0C0, C0→f(C.), C.→ •, Aa→a, D →C3C2, B1→ DBx, B2→C4By, Bx→x, By→y}. Note that, in the extended grammar, wA′ s=wAs|iPos(wG,As,14) =wAs|113 = f4(y). Then, we need to check that the variable xdoes not occur in wA′ s, which can be done in linear time as shown in Lemma 2.8.14. Finally, we perform the substitution {x7→ A′ s}(G) by converting xinto a non-terminal of the grammar generating wA′ sas stated in Definition 3.5.1. The set of rules of the obtained grammar G′after the kext construction and this assignment 33 is {x→A′ s,A′ s→C2By, At→g(B1, A), As→g(B2, A), A →C4Aa, C4→ C3C3, C3→C2C2, C2→C1C1, C1→C0C0, C0→f(C.), C.→ •, Aa→ a, D →C3C2, B1→DBx, B2→C4By, Bx→x, By→y}. Note that wG′,A′ s=wG,As|iPos(wG,As,14) =wG,As|113 =f4(y), and thus, wG′,At=g(f12(wG′,x), f16(a)) = g(f12(wG′,A′ s), f16(a)) = g(f12f4(y), f16(a)) = g(f16(y), f16(a)) = wG′,As. Hence, we state unifiability. The solution σis represented in the STG G′as σ(x) = wG′,x. 34 Chapter 4 First-order matching with STGs In this section we prove that the first-order matching problem can be solved in polynomial time even when the input is compressed using STGs. Definition 4.0.2 The first-order matching problem with STG has an STG Grepresenting first-order terms and contexts as input, plus two term nonterminals Asand Atof Grepresenting terms s=wG,Asand t=wG,At, where tis ground. Its decisional version asks for the existence of a substitution σ such that σ(s) = twhereas its computational version asks for a representation of σ. First-order matching is a particular case of first-order unification. However, taking advantatge of the fact that one of the terms is ground leads to a faster algorithm with respect to the one presented in the previous chapter. We also improve previous results for this problem [GGSS08]. 4.1 Outline of the algorithm The structure of our algorithm is sketched in Figure 4.1. Note that, as commented in Section 2.7, our algorithm is just an adaptation of the algorithm defined in Figure 2.2 to the case where the inputted terms are compressed using STGs. Hence, the input of the problem consists on a STG Gas a compressed representation of two terms sand t. As in the first-order unification case, the algorithm works with representations of the preorder traversal words of the terms sand tto be matched. Hence, we first compute a representation of pre(s) and pre(t). Then we find the index kof the first ocurrence of a variable xin pre(s), and, given Gand 35 k, compute t′=t|iPos(t,k). If t′is undefined we halt giving a negative answer. Otherwise we apply the substitution {x→t′}(s) and restart the process until all variables are replaced. Finally, let s′be the term obtained from safter all replacements are done. We check whether s′and tare syntantically equal and answer accordingly. Note that, in contrast to unification algorithm, we Input: An STG Gand term non-terminals Asand At. (we write sand tfor wAsand wAt and Xfor the set of variables in s). Repeat |X| times: Look for the minimum index ksuch that pre(s)[k] = x∈ X. If iPos(t, k)is undefined Then Halt stating that the initial sand tmatch. Extend Gby the assignment {x7→ t|p}, where p=iPos(t, k). EndRepeat If s=tThen Halt stating that the initial sand tmatch. Else Halt stating that the initial sand tdo not match. Figure 4.1: Matching Algorithm for STG-Compressed Terms look for the first occurrence of a variable in pre(s) instead of looking for the first difference between pre(s) and pre(t). This refines the approach used in previous section for the unification general case of first-order unification and improves time complexity results in previous work on first-order matching with STGs [GGSS08]. In previous section we already showed how to compute a succint representation of pre(s) and pre(t), compute, given a natural number k, the subterm of a term tat position iP os(t, k), and apply a substitution. Hence, it only rests to show how to compute k, the index of the first ocurrence of a variable in pre(s). 4.2 Finding the first occurrence of a variable The task of finding the index of the first occurrence of a variable in a compressed word can be solved efficiently as stated in the following Lemma. Lemma 4.2.1 Let Pbe a SCFG, and let pbe a non-terminal of Prepresenting the preorder traversal word of a first-order term. Then, the minimum index ksuch that wp[k]is a variable can be computed in time O(|P|). Proof. Let Xdenote the set of first-order variables. We define k= index(p, P) as follows: 36 index(p,P)=            1 , if p→α∈P∧α∈ X index(p1,P) , if (p→p1p2)∈P∧ ∃x∈ X :xoccurs in wP,p1 |wP,p1|+index(X2,P) , Otherwise. Note that we assumed that Pis in Chomsky Normal Form. If this was not the case, we can force this assumption with a linear time and space transformation. The fact that index(p, P) computes the minimum index k such that wp[k] is a variable can be shown by induction on depth(p). With respect to the time complexity, for each non-terminal pof a SCFG P, both the number |wp|and whether wpcontains a variable can be precomputed in linear time as stated in Lemmas 2.8.13 and 2.8.14, respectively. Once this precomputations are done index(p, P ) can be computed by a single run over the rules of Pand hence, it runs also in linear time. 2 4.3 A polynomial time algorithm for firstorder matching with STGs The algorithm presented in the previous section runs in polynomial time due to the following observations. Let nand mbe the initial value of depth(G) and |G|, respectively. We define V:= Xto be the set of all the first-order variables at the start of the execution (before any of them has been converted into a non-terminal). As in the unification case, the final size of the grammar is bounded by m+|V|nthanks to Lemmas 3.5.4 and 3.5.6. Our algorithms iterates at most Vtimes. By Lemmas 3.4.2, and 4.2.1 each iteration takes linear time. Finally we check equality of two words generated by a SCFG P, which takes time O(|P|3) thanks to Theorem 2.8.12. Hence, we have the following: theorem 4.3.1 First-order matching of two terms represented by an STG can be done in polynomial time (O((m+|V|n)3), where mrepresents the size of the inputted STG, nrepresents its depth, and Vrepresents the set of different first-order variables occurring in the inputted terms). This holds for the decision question, as well as for the computation of the unifier, whose components are represented by the final STG. 37 Chapter 5 Conclusion & further work We presented instantiation-based algorithms for the first-order matching problem and the first-order unification problem, that can be immediately executed on the compressed representation of large terms and run in polynomial time on the size of the representation. This results represent an improvement in time complexity with respect to previous work. Furthermore, we believe that the obtained algorithms represent also a gain in simplicity whichs makes their implementation feasible. It would be also interesting to investigate optimizations for these algorithms, as well as finding an improved upper bound. We also believe that it would be natural to consider the context matching problem using an STG encoding for terms under certain restrictions like fixing the number of context variables (this restriction was already consider using a dag representation in [GGSS08]). Finally, we think that our techniques could be useful to decide the one context unification problem in NP when the input is represented by an STG. This problem has been solved for plain terms as input in [GGSST09]. This project has been useful for me for being introduced in several research tasks such as those directly related to problem solving, those related to the composition of a paper showing the obtained results as well as the experience of going throught a revision process for a conference. Furthermore, in the context of this project I had the oportunity of presenting a paper in an international conference. Without a doubt this has been a rewarding task. 38 Bibliography [BLM05] G. Busatto, M. Lohrey, and S. Maneth. Efficient memory representation of XML documents. In Proc. of DBPL 2005, volume 3774 of LNCS, pages 199–216, 2005. [BS94] F. Baader and J. Siekmann. Unification theory. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, pages 41–125. Oxford University Press, 1994. [BS01] F. Baader and W. Snyder. Unification theory. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 8, pages 445–532. Elsevier Science and MIT Press, 2001. [CDG+97] H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available on: http://www.grappa.univ-lille3.fr/tata, 1997. release 1.10.2002. [Com91] H. Comon. Completion of rewrite systems with membership constraints. Journal of Symbolic Computation, 25(4):397 – 419, 1991. [GGSS08] A. Gasc´on, G. Godoy, and M. Schmidt-Schauß. Context matching for compressed terms. In 23rd IEEE LICS, pages 93–102, 2008. http://www.lsi.upc.edu/ ggodoy/publications.html. [GGSS09] A. Gasc´on, G. Godoy, and M. Schmidt-Schauß. Unification with singleton tree grammars. In RTA, pages 365–379. Springer, 2009. [GGSST09] A. Gasc´on, G. Godoy, M. Schmidt-Schauß, and A. Tiwari. Context Unification with One Context Variable. Journal of Symbolic Computation, 2009. To appear. 39 [GM02] B. Genest and A. Muscholl. Pattern matching and membership for hierarchical message sequence charts. In Proc. of LATIN 2002, pages 326–340. Springer-Verlag, 2002. [HSTA00] M. Hirao, A. Shinohara, M. Takeda, and S. Arikawa. Fully compressed pattern matching algorithm for balanced straightline programs. In SPIRE ’00, page 132, Washington, DC, USA, 2000. IEEE Computer Society. [KPR96] M. Karpinski, W. Plandowski, and W. Rytter. Efficient algorithms for Lempel-Ziv encoding. In In Proc. 4th Scandinavian Workshop on Algorithm Theory, pages 392–403. SpringerVerlag, 1996. [KRS95] M. Karpinski, W. Rytter, and A. Shinohara. Pattern-matching for strings with short description. In CPM ’95, pages 205–214. Springer-Verlag, 1995. [Lif07] Y. Lifshits. Processing compressed texts: A tractability border. In CPM 2007, pages 228–240, 2007. [LM05] M. Lohrey and S. Maneth. The complexity of tree automata and XPath on grammar-compressed trees. In Proc. of the 10th CIAA ’05, 2005. [LMSS09] M. Lohrey, S. Maneth, and M. Schmidt-Schauß. Parameter reduction in grammar-compressed trees. In 12th FoSSaCS, volume 5504 of LNCS, pages 212–226. Springer, 2009. [Loh06] M. Lohrey. Word problems and membership problems on compressed words. SIAM Journal on Computing, 35(5):1210–1240, 2006. [LR06] S. Lasota and W. Rytter. Faster algorithm for bisimulation equivalence of normed context-free processes. In Proc. MFCS’06, volume 4162 of LNCS, pages 646–657. Springer-Verlag, 2006. [LSSV04] J. Levy, M. Schmidt-Schauß, and M. Villaret. Monadic secondorder unification is NP-complete. In Proc. 15th RTA, volume 3091 of LNCS, pages 55–69. Springer, 2004. [LSSV06a] J. Levy, M. Schmidt-Schauß, and M. Villaret. Bounded secondorder unification is NP-complete. In Proc. RTA-17, volume 4098 of LNCS, pages 400–414. Springer, 2006. 40 [LSSV06b] J. Levy, M. Schmidt-Schauß, and M. Villaret. Stratified context unification is NP-complete. In Proc. Third IJCAR 2006, volume 4130 of LNCS, pages 82–96. Springer, 2006. [MM82] A. Martelli and U. Montanari. An efficient unification algorithm. ACM Trans. on programming languages and systems, 4(2):258– 282, 1982. [MMS08] S. Maneth, N. Mihaylov, and S. Sakr. XML tree structure compression. DEXA, 0:243–247, 2008. [MST97] M. Miyazaki, A. Shinohara, and M. Takeda. An improved pattern matching algorithm for strings in terms of straight-line programs. In Proc. 8th CPM, number 1264 in LNCS, pages 1–11. Springer-Verlag, 1997. [Pla94] W. Plandowski. Testing equivalence of morphisms in contextfree languages. In Jan van Leeuwen, editor, Proc. 2nd ESA’94, volume 855 of LNCS, pages 460–470, 1994. [Pla95] W. Plandowski. The Complexity of the Morphism Equivalence Problem for Context-Free Languages. PhD thesis, Department of Mathematics, Informatics and Mechanics, Warsaw University, 1995. [Rob65] J.A. Robinson. A machine oriented logic based on the resolution principle. J. of the ACM, 12(1):23–41, 1965. [SS02] M. Schmidt-Schauß. A decision algorithm for stratified context unification. J. of Logic and Computation, 12(6):929–953, 2002. [SS05] M. Schmidt-Schauß. Polynomial equality testing for terms with shared substructures. Frank report 21, Institut f¨ur Informatik. FB Informatik und Mathematik. J. W. Goethe-Universit¨at Frankfurt am Main, November 2005. [SSS02] M. Schmidt-Schauß and K. U. Schulz. Solvability of context equations with two context variables is decidable. J. Symb. Comput., 33(1):77–122, 2002. [SSS04] M. Schmidt-Schauß and J. Stuber. On the complexity of linear and stratified context matching problems. Theory of Computing Systems, 37:717–740, 2004. 41