Generalizing Programs via Subsumption

Generalizing Programs via Subsumption Miguel A. Guti´errez-Naranjo, Jose´ A. Alonso-Jim´enez, and Joaqu´ın Borrego-D´ıaz Dept. of Computer Science and Artificial Intelligence University of Seville {magutier,jalonso,jborrego}@us.es Abstract. In this paper we present a class of operators for Machine Learning based on Logic Programming which represents a characterization of the subsumption relation in the following sense: The clause C1 subsumes the clause C2 iff C1 can be reached from C2 by applying these operators. We give a formalization of the closeness among clauses based on these operators and an algorithm to compute it as well as a bound for a quick estimation. We extend the operator to programs and we also get a characterization of the subsumption between programs. Finally, a weak metric is presented to compute the closeness among programs based on subsumption. 1 Introduction In a Machine Learning system based on clausal logic, the main operation lies on applying an operator to one or more clauses with the hope that the new clauses give a better classification for the training set. This generalization must fit into some relation of order on clauses or sets of clauses. The usual orders are the subsumption order, denoted by , and the implication order |=. Subsumption was presented by G. Plotkin [9]. In his study about the lattice structure induced by this relation on the set of clauses, he proved the existence of the least general generalization of two clauses under subsumption and defined the least generalization under relative subsumption. Both techniques are the basis of successful learning systems on real-life problems. Later, different classes of operators on clauses, the so-called refinement operators, were studied by Shapiro [11], Laird [5] and van der Laag and Nienhuys-Cheng [13] among others. In their works, the emphasis is put on the specialization operators, which are operators such that the obtained clause is implied or subsumed by the original clause, and the generalization operators are considered the dual of the first ones. In this paper we present new results and algorithms about the generalization of clauses and logic programs via subsumption. We propose new generalization operators for clausal learning, the Learning Operators under Subsumption which represent a characterization by operators of the subsumption relation between  Work partially supported by project TIC 2000-1368-C03-0 (Ministry of Science and Technology, Spain) and the project TIC-137 of the Plan Andaluz de Investigaci´on. clauses in the following sense: If C1and C2are clauses, C1subsumes C2if and only if there exists a finite sequence (a chain)ofLOS{∆1/x1},...,{∆n/xn} such that C1=C2{∆1/x1}...{∆n/xn}.IfC1subsumes C2, we know that the set of chains of LOS from C2to C1is not empty, but in general the set has more than one element. The existence of a non-empty set of chains gives us the idea for a formalization of closeness among clauses as the length of the shortest chain from C2to C1,if C1subsumes C2, and infinity otherwise. This mapping, which will be denoted by dc, is the algebraic expression of the subsumption order: for every pair of clauses, C1and C2,C1subsumes C2if and only if dc(C2,C 1) is finite. Since the subsumption order is not symmetric, the mapping dc is not either. Therefore dc is not a metric, but a quasi-metric. Finally, dc is computable. We give in this paper an algorithm which calculates the quasi-distance between two clauses and present a bound which allows to estimate the closeness between clauses under the hypothesis of subsumption. This algorithm and estimation provides useful tools for the design of new learning systems which use quasi metrics to compute closeness. In the second part of the paper, we extend the study to programs. We define a new class of operators, the composed LOS, which act on the set of programs and they also represent a characterization of the subsumption relation between programs. Analogously to the clausal case, the minimum of the length of the chains of operators between two programs is the basis of a weak metric to quantify the closeness between programs. This weak metric has been experimentally checked and can be added to existing systems or used to design new ones. 2 Preliminaries From now on, we will consider some fixed first-order language Lwith at least one function symbol. Var,Term and Lit are, respectively, the sets of variables, terms and literals of L.Aclause is a finite set of literals, a program is a nonempty finite set of non-empty clauses, Cis the set of all clauses and Pis the set of all programs. A definite program is a program where each clause contains one positive and zero or more negative literals. As usual, TPwill denote the immediate consequence operator of the program P. Asubstitution is a mapping θ:S→Term where Sis a finite set of variables such that (∀x∈S)[x=θ(x)]. We will use the usual notation θ={x/t :x∈S}, where t=θ(x), Dom(θ) for the set Sand Ran(θ)=∪{Var(t):x/t ∈θ}.A pair x/t is called a binding.IfAis a set, then |A|is the cardinal of Aand PA its power set. We will denote by |θ|the number of bindings of the substitution θ. The clause Csubsumes the clause D,CD, iff there exists a substitution θ such that Cθ ⊆D.Aposition is a non-empty finite sequence of positive integers. Let N+denote the set of all positions. If t=f(t1,...,t n) is an atom or a term, tiis the term at position iin tand the term at position iˆuin tis sif sis at position uin ti. Two positions uand vare independent if uis not a prefix of v and vice versa. A set of positions Pis independent if it is a pairwise independent C2={sum(z,0,s(x)), sum(s(x),0,s(x)), sum(z,0,z)} zz P1={1}P2=∅P3={1,3} s(x) sum(s(x),0,s(x)) }C1={ .................... .................... .................... Fig. 1. Example of generalization set of positions. The set of all positions of the term tin Lwill be denoted by Pos(L, t). If tis a term (resp. an atom), we will denote by t[u←s] the term (resp. the atom) obtained by grafting the term sin tat position uand, if Lis a literal, we will write L[P←s] for the literal obtained by grafting the term s in Lat the independent set of positions P. 3 The Operators In the generalization process, when a program Pis too specific, we replace it by Pwith the hope that Pcovers the examples better than P. The step from Pto Pis usually done by applying an operator to some clause Cof P. These operators can be defined as mappings from Cto C, where Cis the set of clauses of the language. Before giving the definition of the operator, we will give some intuition with an example. Consider the one–literal clause C1={L}with L=sum(s(x),0,s(x)). In order to generalize it with respect to the subsumption order, we have to obtain a new clause C2such that there exists a substitution θverifying C2θ⊆C1. For that, we firstly choose a term tin L,sayt=s(x), then we choose several subsets of Pos(L, t), e.g. P1={1},P 2=∅,P 3={1,3}and a variable not occurring in L,sayz, and finally we build the clause C2= {L[Pi←z]|i=1,2,3}={sum(z,0,s(x)), sum(s(x),0,s(x)), sum(z,0,z)}. Obviously θ={z/s(x)}satisfies C2θ⊆C1(see Fig. 1). If the clause has several literals, for example, C1={L1,L 2,L 3}, with L1=num(s(x)), L2= less than(0,s(x)) and L3=less than(s(x),s(s(x))), the operation is done with all literals simultaneously. First, the same term is chosen in every literal of C1,sayt=s(x). Then, for each literal Li∈C1, some subsets of Pos(Li,t) are chosen, e.g.,P∗ 1={∅,{1}}⊆PPos(L1,t), P∗ 2=∅⊆PPos(L2,t) and P∗ 3={{1,2·1},{1}}⊆PPos(L3,t) After taking a variable which does not occur in C1,sayz, we build the sets L1 P∗ 1 −−→{num(s(x)), num(z)}L2 P∗ 2 −−→∅ and L3 P∗ 3 −−→{less than(z,s(z)), less than(z,s(s(x)))}.C2is the union of these sets, i.e., C2={num(s(x)), num(z), less than(z,s(z)), less than(z,s(s(x)))} and C2{z/s(x)}⊆C1. In our general description, we will begin with substitutions and grafts. Definition 1. Let Lbe a literal and ta term. The set of positions Pis called compatible with the pair L, tif P⊆Pos(L, t). Let P∗be a set whose elements are sets of positions. Let Lbe a literal and ta term. P∗is called compatible with the pair L, tif every element of P∗is compatible with L, t For example, if L=sum(s(x),0,s(x)) and t=s(x), then P1={1},P2=∅, P3={1,3}are compatible with L, tbut P4={1·1,2},P5={1,4·3}are not. If P∗ 1={P1,P 2,P 3}and P∗ 2={P2,P 4}, then P∗ 1is compatible with L, tand P∗ 2is not. The next mappings are basic in the definition of our operators. As we saw in the example, the key is to settle a set of sets of positions for each literal, all them occupied by the same term. This one is done by the following mappings. Definition 2. A mapping ∆:Lit →PPN+is an assignment if there exists a term tsuch that, for every literal L,∆(L)is compatible with the pair L, t. Note that the term tdoes not have to be unique, for example, consider the identity assignment (∀L∈Lit)[∆(L)={∅}], the empty assignment (∀L∈ Lit)[∆(L)=∅] or any mixture of both. The assignments map a literal into a set of sets of positions. Each element of this set of positions will produce a literal, and the positions are the places where the new term is grafted. If ∆:Lit →PPN+is an assignment of positions and s is a term, we will denote by L{∆(L)/s}the set of literals, one for each element P∈∆(L), obtained by grafting sin Lat P. Formally L{∆(L)/s}={L[P← s]|P∈∆(L)}For example, if L=sum(s(x),0,s(x)), zis a variable, P∗ 1is taken from the above example and ∆is an assignment such that ∆(L)=P∗ 1 then L{∆(L)/z}={L[P←z]|P∈∆(L)}={L[P←z]|P∈P∗ 1}={L[P1← z]},L[P2←z],L[P3←z]}={sum(z,0,s(x)), sum(s(x),0,s(x)), sum(z,0,z)} We can now define our Learning Operators under Subsumption1. Definition 3. Let ∆be an assignment and xa variable. The mapping {∆/x}:C−→ C C→ C{∆/x}=L∈CL{∆(L)/x} isaLearning Operator under Subsumption (LOS) if for all literal L,if∆(L)=∅ then x∈ Var(L). Turning back to a previous example, if C={L1,L 2,L 3}, with L1=num(s(x)), L2=less than(0,s(x)), L3=less than(s(x),s(s(x))), and the assignment ∆(L)=       P∗ 1={∅,{1}} if L=L1 P∗ 2=∅if L=L2 P∗ 3={{1,2·1},{1}}if L=L3 ∅otherwise 1A preliminary version of these operators appeared in [2]. and considering zas the variable to be grafted, then C{∆/z}={num(s(x)), num(z), less than(z,s(z)), less than(z,s(s(x)))}. These operators allow us to generalize a given clause and go up in the subsumption order on clauses as we see in the next theorem. Proposition 1. Let Cbe a clause and {∆/x}a LOS. Then C{∆/x}C. The LOS define an operational definition of the subsumption relation. The last result states one way of the implication. The next one claims that all the learning based on subsumption of clauses can be carried out only by applying LOS. Theorem 1. Let C1and C2be two clauses such that C1C2. Then there exists a finite sequence (a chain){∆1/x1},...,{∆n/xn}of LOS such that C1=C2{∆1/x1}...{∆n/xn} For example, if we consider C1={p(x1,x 2)}and C2={p(x2,f(x1)),p(x1,a)} and the substitution θ={x1/x2,x 2/f(x1)}. Then C1θ⊆C2holds and therefore C1C2. Decomposing θwe can get σ1={x2/x3},σ2={x1/x2}, σ3={x3/f(x1)}and C1σ1σ2σ3⊆C2holds. Hence, considering the assignments ∆1(p(x2,f(x1)) = {{2}} and ∆1(L)=∅if L=p(x2,f(x1)) ∆2(p(x2,x 3)) = {{1}} and ∆2(L)=∅if L=p(x2,x 3) ∆3(p(x1,x 3)) = {{2}} and ∆3(L)=∅if L=p(x1,x 3) we have C1=C2{∆1/x3}{∆2/x1}{∆3/x2}. Note that if we take the assignment ∆(p(x1,a)) = {{2}} ;∆(L)=∅if L=p(x1,a), then C1=C2{∆/x2}also holds. 4 A Quasi-metric Based on Subsumption The operational characterization of the subsumption relation given in the previous section gives us a natural way of formalizing the closeness among clauses. As we have seen, if C1C2then there exists at least one chain of LOS from C2to C1and we can consider the length of the shortest chain from C2to C1.If C1does not subsume C2, we will think that C1cannot be reached from C2by applying LOS, so both clauses are separated by an infinite distance. Definition 4. Achain of LOS of length n(n≥0) from the clause C2to the clause C1is a finite sequence of nLOS {∆1/x1},{∆2/x2},...,{∆n/xn}such that C1=C2{∆1/x1}{∆2/x2}...{∆n/xn}The set of all the chains from C2to C1will be denoted by L(C2,C 1)and |C| will denote the length of the chain C. We define the mapping dc :C×C→[0,+∞]as follows: dc(C2,C 1)=min{|C| :C∈L(C2,C 1)}if C1C2 +∞otherwise The subsumption relation is not symmetric, so the mapping dc is not either. Instead of being a drawback, this property gives an algebraic characterization of the subsumption relation, since C1C2iff dc(C2,C 1)=+∞. Notice that a quasi–metric satisfies the conditions to be a metric, except for the condition of symmetry. Definition 5. A quasi–metric on a set Xis a mapping dfrom X×Xto the non–negative reals (possibly including +∞) satisfying: (1) (∀x∈X)d(x, x)=0, (2) (∀x, y, z ∈X)d(x, z)≤d(x, y)+d(y,z)and (3) (∀x, y ∈X)[d(x, y)= d(y,x)=0⇒x=y] The next result states the computability of dc and provides an algorithm to compute it. Theorem 2. dc is a computable quasi–metric. Proof (Outline). Proving that dc is a quasi-metric is straightforward from the definition. The proof of the computability is split in several steps. Firstly, for each substitution θwe define the set of the splittings up: Split(θ)=σ1...σ n:σi={xi/ti}xi∈ Var(ti) (∀z∈Dom(θ))[zθ =zσ1...σ n] with length(σ1...σ n)=nand weight(θ)=min{length(Σ)|Σ∈Split(θ)}. The next equivalence holds dc(C2,C 1)=       0ifC1=C2 1ifC1=C2and C1⊆C2 min{weight(θ)|C1θ⊆C2}if C1C2and C1⊆ C2 +∞if C1 C2 We can decide if C1C2and, if it holds, we can get the finite set of all θ such that C1θ⊆C2, so to conclude the theorem we have to give an algorithm which computes weight(θ) for each θ. The Fig. 2 shows a non-deterministic algorithm which generates elements of Split(θ). The algorithm finishes and for all Σ∈Split(θ) it outputs Σ∗∈Split(θ) verifying length(Σ∗)≤length(Σ). The previous theorem provides a method for computing dc, but deciding whether two clauses are related by subsumption is an NP-complete problem [1], so, from a practical point of view we need a quick estimation of the quasi-metric before deciding the subsumption. The next result settles an upper and lower bounds for the quasi-metric under the assumption of subsumption. Theorem 3. Let C1and C2be two clauses such that C1⊆ C2.IfC1C2then |Var(C1)−Var(C2)|≤dc(C2,C 1)≤min{2·|Var(C1)|,|Var(C1)|+|Var(C2)|} Proof (Outline). For each θsuch that C1θ⊆C2,θhas at least |Var(C1)− Var(C2)|bindings and we need at least one LOS for each binding, hence the first inequality holds. For the second one, if C1θ⊆C2then we can find nsubstitutions σ1,...,σ nwith σ1={xi/ti}and xi∈ Var(ti) such that C1σ1...σ 2⊆C2 verifying n=|θ|+|Ran(θ)∩Dom(θ)|. The inequality holds since Ran(θ)⊆ Var(C2), Dom(θ)⊆Var(C1) and |θ|≤Var(C1). If C1={p(x1,x 2)},C2= {p(a, b)}and C3={p(f(x1,x 2),f(x2,x 1))}then dc(C2,C 1)=|Var(C1)−Var(C2)|=2 dc(C3,C 1)=min{2·|Var(C1)|,|Var(C1)|+|Var(C2)|} =4 The above examples show that these bounds cannot be improved. Input: A non-empty substitution θ Output: An element of Split(θ) Set θ0=θand U0=Dom(θ)∪Ran(θ) Step 1: If θiis the empty substitution Then stop Otherwise: Consider θi={x1/t1,...,x n/tn}and go to Step 2. Step 2: If there exists xj∈Dom(θi) such that xj∈ Ran(θi) Then for all k∈{1,...,j−1,j+1,...,n}let t∗ kbe a term such that tk=t∗ k{xj/tj}Set θi+1 ={x1/t∗ 1,...,x j−1/t∗ j−1,x j+1/t∗ j+1,...,x n/t∗ n} σi+1 ={xj/tj} Ui+1 =Ui set ito i+ 1 and go to Step 1. Otherwise: Go to Step 3. Step 3: In this case let zibe a variable which does not belong to Uiand set Ui+1 =Ui∪{zi} choose j∈{1,...,n}y let Tbe a subterm of tjsuch that Tis not a variable belonging to Ui+1. Then, for all k∈{1,...,n}let t∗ kbe a term such that tk=t∗ k{z/T}. Set θi+1 ={x1/t∗ 1,...,x n/t∗ n} σi+1 ={z/T} set ito i+ 1 and go to Step 1. Fig. 2. Algorithm scheme to compute the subset of Split(θ) 5 Programs In this section we extend the study of subsumption to programs. Definition 6. The program P2subsumes the program P1,P2P1, if there exists a mapping F:P1→P2such that F(C)C, for all C∈P1. In the case of definite programs, the subsumption is related to the semantics via the immediate consequence operator. The proof is adapted from [7]. Proposition 2. Let P1and P2be two definite programs. Then P1P2if and only if for all interpretation I,TP2(I)⊆TP1(I) The operators for programs are sets of pairs assignment–variable. These operators represent a characterization for the subsumption relation between programs, as we will show below. Definition 7. Acomposed LOS is a finite set of pairs Θ={∆1/x1,...,∆ n/xn} where {∆i/xi}is a LOS for all i∈{1,...,n}. For applying a composed LOS to a program we need an auxiliary mapping which associates one LOS to each clause of the program. Definition 8. Let Pbe a program and Θa composed LOS. An auxiliary mapping for applying (amfa) is a mapping a:P→Θsuch that for all clause C∈P, the clause C{a(C)}is not the empty clause. The program PaΘ= {C{a(C)}|C∈P}is the program obtained by applying Θto Pvia the amfa a. For example, consider the program2P={C1,C 2,C 3}with C1=sum(0,s(s(0)),s(s(0))) ←sum(0,s(0),s(0)) C2=sum(s(x),s(0),s(z)) ←sum(s(0),0,s(0)), sum(x, s(0),z) C3=sum(s(y),y,s(z)) ←sum(0,y,y), sum(y,y,z) and Θ={∆1/x, ∆2/y, ∆3/x}with ∆1(L)={{2,3}} if L=sum(0,s(s(0)),s(s(0))) ∅otherwise ∆2(L)=   {{2}} if L∈sum(s(x),s(0),s(z)) ¬sum(x, s(0),z) ∅otherwise ∆3(L)=   {{1·1}} if L=sum(s(y),y,s(z)) {{1}} if L=¬sum(y,y,z) ∅otherwise Consider the amfa a:P→Θsuch that a(C1)= ∆1/x ,a(C2)= ∆2/y , a(C3)= ∆3/x . Then C1{a(C1)}=C1{∆1/x}≡sum(0,x,x)← C2{a(C2)}=C2{∆2/y}≡sum(s(x),y,s(z)) ←sum(x, y, z) C3{a(C2)}=C3{∆3/x}≡sum(s(x),y,s(z)) ←sum(x, y, z) Therefore PaΘ=sum(0,x,x)← sum(s(x),y,s(z)) ←sum(x, y, z) The composed LOS also represent an operational characterization of the subsumption relation among programs. The main results are theorems 4 and 5. Theorem 4. Let P1and P2be two programs and Θa composed LOS. If P2θ⊆ P1then P1P2, where Θis applied to Pvia an appropriate amfa. The following corollary is immediate. Corollary 1. Let P1and P2be two programs and Θ1...Θ na finite chain of composed LOS. If P2Θ1...Θ n⊆P1then P1P2, where each Θis applied via an appropriate amfa ai. The next result is the converse of the corollary 1. 2We use the Prolog notation A←B1,...,B ninstead of {A, ¬B1,...,¬Bn} Theorem 5. Let P1and P2be two programs. If P1P2then there exists a finite chain of composed LOS Θ1...Θ nsuch that P2Θ1...Θ n⊆P1, where each Θis applied via an appropriate amfa ai. The proof of this theorem can be obtained straightforwardly from the theorem 1. If P1P2then for each C∈P2there exists D∈P1such that DC and we can find a finite chain of LOS {∆1/x1},...,{∆n/xn}such that D= C{∆1/x1},...,{∆n/xn}. By joining appropriately the LOS from these chains we have the composed LOS. 6 Quantifying Closeness among Programs If P1subsumes P2we can find a finite chain of composed LOS which maps P2 onto a subset of P1. This chain has not to be unique. In a similar way to the clausal case, the shortest chain quantifies the closeness between programs. We formalize this idea in the next definitions. Definition 9. Let P1and P2be two programs such that P1P2. We will say that C=Θ1,a 1,...,Θn,a n is a chain from P1to P2if –Θ1,...,Θ nare composed LOS. –For all i∈{1,...,n},ai:P2Θ1...Θ i−1→Θiis an amfa. –P2Θ1...Θ n⊆P1where the composed LOS have been applied via the correspondent ai. In this case we will say that Cis a chain of length nand we will denote it by |C| =n.IfP1⊆P2we will say that the empty chain, of length zero, is a chain from P1to P2. The set of chains from P1to P2will be denoted by L(P1,P 2). If P1P2, the set L(P1,P 2) is not empty and the next definition makes sense. Definition 10. We will define the mapping dp :P×P→[0,+∞]as follows: dp(P1,P 2)=min{|C| :C∈L(P1,P 2)}if P1P2 +∞otherwise The mapping dp verifies the following properties: –P1⊆P2⇔dp(P2,P 1) = 0, in particular, dp(P,P)=0 –In general, dp(P1,P 2)=dp(P2,P 1), P1,P 2∈P –dp(P1,P 2)≤dp(P1,P 0)+dp(P0,P 2) for all P1,P 2,P 3∈P hence, dp is a pseudo-quasi-metric and (P,dp)isaquantitative domain. The next equivalence summarize our study about the generalization of programs under subsumption, by putting together our operators, the subsumption relation, the semantics of definite programs and the weak metric dp. Theorem 6. Let P1and P2be two definite programs. The following sentences are equivalent: