Folding by Similarity

Folding by Similarity F. J. Gal´an and J. M. Ca˜nete Dept. de Lenguajes y Sistemas Inform´aticos. Facultad de Inform´atica. Av. Reina Mercedes s/n. 41012. Sevilla. Fax:34 954557139, Voice: 34 954552773 E-mail: [email protected] Abstract A formal specification can describe software models which are difficult to program. Transformational methods based on fold/unfold strategies have been proposed to palliate this problem. The objective of applying transformations is to filter out a new version of the specification where recursion may be introduced by a folding step. Among many problems, the ”eureka” about when and how to define a new predicate is difficult to find automatically. We propose a new version of the folding rule which decides automatically how to introduce new predicates in a specification. Our method is based on finding similarities between formulas represented as parsing trees and it constitutes an assistance to the complex problem of deriving recursive specifications from non recursive ones. Keywords: specification transformation, program synthesis, correctness preservation, program specification. 1 Introduction Usually, a specification describes software models which are difficult to program. Systematic construction of programs from specifications is known as program synthesis. A huge variety of synthesis mechanisms have been developed [BSW90], [BD77], [DeK94], [Dro88], [Fle95], [Smi90], [AFM99]. In this work, we are interested in transformational mechanisms; a sequence of meaning-preserving transformation rules (e.g. unfolding, folding, universal instantiation, abstraction, predicate definition, etc.) is applied to a specification until a program is obtained. The objective of applying transformations is to filter out a new version of the specification where recursion may be introduced by a folding step. However, among many others problems, deciding about when and how to define a new predicate (i.e. recursive predicate) is difficult to find automatically. Fold/unfold transformations represent an important investigation subject in the literature [ArD95], [BD77], [Par90], [PrP93], [PeP94], [TaS84]. Basically, unfolding represents the replacement of an atom by its definition and folding represents the inverse operation of replacing a subformula by an atom. In the following example, the context Sdefines a (many-sorted) first-order APPIA-GULP-PRODE 2001 language with types Nat (natural numbers) constructed from the function symbols 0 and sand Seq(Nat) (sequences of natural numbers) constructed from the function symbols empty and conc. It defines also the meaning of relation symbols such as = (identity between natural numbers), nocc (number of occurrences of an element in a sequence) and perm (permutations of a sequence of natural numbers). S={T ypes :Nat generated by 0, s Seq(Nat) generated by empty, conc D=: 0 = 0 ⇔true 0 = s(x)⇔false s(x) = 0 ⇔false s(x) = s(y)⇔x=y Dnocc :nocc(e, empty, z)⇔z= 0 nocc(e, conc(x, Y ), s(z)) ⇔x=e∧nocc(e, Y, z) nocc(e, conc(x, Y ), z)⇔ ¬x=e∧nocc(e, Y, z) Dperm :perm(L, S)⇔(nocc(a, L, z)⇔nocc(a, S, z))} Dperm is not closed to the structure of a program (i.e. there is not any explicit recursion). Following a transformational synthesis process for Dperm (e.g. applying universal instantiation on variables L,Sand zin Dperm, we obtain D1and then unfolding D1w.r.t. nocc(b, conc(v, V ), s(k)) and nocc(b, conc(w, W ), s(k))) atoms using second axiom in Dnocc) we reach expressions such as D2: D1:perm(conc(v, V ), conc(w, W )) ⇔(nocc(b, conc(v, V ), s(k)) ⇔ nocc(b, conc(w, W ), s(k))) D2:perm(conc(v, V ), conc(w, W )) ⇔((v=b∧nocc(b, V, k)) ⇔ (w=b∧nocc(b, W, k))) Two questions arise at this point, (a) Is it possible to introduce recursive predicates in D2? and (b) How can we do it? It is difficult to achieve an ”automatic answer” to these questions. Our method follows a constructive approach. A comparison based on the notion of similarity between D2and Dperm is needed to decide about first question. Only if first question is answered affirmatively then a similarity-based folding rule is applied to Din order to answer second question. Our work is explained in the following manner. Section 2 defines the form of our specifications and a non-constructive characterization of the folding rule is presented. Section 3 defines the concept of similarity. Basically, it represents an automatic method for deciding which subformulas produce recursion. In section 4, we describe a similarity based folding rule which preserves correctness, and finally, in section 5 we establish conclusions. 2 Preliminary Definitions In this section, the syntax and semantics of our specifications and a non-constructive definition of the folding rule are presented. The use of the folding rule is intended to introduce recursion in a specification. Folding by Similarity Definition 2.1 (Syntax of a Formula) A many-sorted (typed) first order language is assumed to write our formulas. A formula Qτ1x1...QτnxnFwhere Qτixi is a universal or existential quantifier defined on a type τi,xiis different from xj for i6=j, and Fcontains no quantifier, is said to be in prenex normal form. We consider that, when possible, all quantifiers in a formula are ordered following a lexicographic order defined on the names of their respective types. For example, ∀Nata∀Natz∀Seq(Nat)L∀Seq(Nat)S(nocc(a, L, z)⇔nocc(a, S, z)) is in prenex normal form where all quantifiers have been ordered following a lexicographic order defined on the names of their respective types. In the following, we assume that all our formulas are in prenex normal form, this does not represent any restriction due to the existence of an effective procedure for transforming any first-order formula into an equivalent one in prenex normal form [Men87]. For legibility reasons, we omit τsubscripts when a type can be induced clearly in a formula and expressions such as Qτx...QτzF can be collapsed into equivalent expressions Qτx, ..., zF . For example, the formula ∀Nata∀Natz∀Seq(Nat)L- ∀Seq(Nat)S(nocc(a, L, z)⇔nocc(a, S, z)) can be collapse into the equivalent formula ∀Nata, z∀Seq(Nat)L, S(nocc(a, L, z)⇔nocc(a, S, z)). In addition, when possible, universal quantifiers are omitted in the front of a formula. Definition 2.2 (Substitution) A (ground) variable substitution is the pair (v, t) where vis a variable and tis a (ground) term. A substitution σis a set of variable substitutions. Let X={x1, ..., xn}and Y={y1, ..., yn}be two sets of variables where xiis different from xjand yiis different from yjfor i6=j. Let QX={Qτx1, ...,- Qτxn}and QY={Qτy1, ..., Qτyn}be two sets of quantifiers for variables in Xand Y respectively. We say that σ={(x1, y1), ..., (xn, yn)}is a renaming substitution which agrees w.r.t. quantifications iff (a) X∩Y=∅and (b) Qτxi=Qτyiwith i= 1..n. Definition 2.3 (Specification) An if-and-only-if axiom is a formula of the form r(x1, ..., xn)⇔R(y1, ..., ym)(e.g. axioms for =,nocc and perm relation symbols in S). The symbol ris called the defined symbol. The atom r(x1, ..., xn)is called the left-hand side of the axiom and the (sub)formula R(y1, ..., ym)is called the right-hand side of the axiom. A specification for a relation symbol ris the set Drof all axioms with the same defined symbol. In the following, we use Dr,n to identify the nth axiom in Dr. Definition 2.4 (Context) A context Cis a set of types and specifications for relation symbols. Types are constructed from function symbols appearing in C.Cis atomically complete if, for every ground atom r(t1, ..., tn), either C ` r(t1, ..., tn) or C ` ¬r(t1, ..., tn).Chas isoinitial model Miff for every ground literal l,M|= liff C ` l. Therefore, the meaning of a relation rin Cis the set of all ground literals ldefined on rsuch that C ` l. Some authors have studied the problem of the existence of isoinitial models for theories in general [BMM83] and some effective criteria have been proposed to construct consistent theories. Following [LaO94], a context Cadmits an isoinitial model if and only if it is atomically complete. By hypothesis, we assume that our contexts are consistent in this way. APPIA-GULP-PRODE 2001     za  ,∀ SL   ,  ∀ 1 211  ⇔  ),,( zLan o c c  ),,( zSan o c c Figure 1: P arse(∀Nata, z∀Seq(Nat)L, S(nocc(a, L, z)⇔nocc(a, S, z))). Definition 2.5 (Folding Rule) A folding rule is a transformation rule intended for replacing a subformula by an atom. Let Sbe a formula and r(xj)⇔Rj(yj) be an axiom for rin C. We say that Sjis obtained from Sfolding with respect to r(xj)⇔Rj(yj)iff Sj=S|R r(xj)θjwhere (a) There exist subformula Rin S and substitution θsuch that R=Rj(yj)θjand (b) S|R r(xj)θjrepresents the textual replacement of Rby r(xj)θjin S. For example, the formula S≡(nocc(b, V, k)⇔nocc(b, W, k)) ∧v=b∧w=bcan be folded with respect to Dperm. Applying the substitution θ1={(L, V ),(S, W ),- (z, k),(a, b)}to the right-hand side of the axiom in Dperm we obtain the subformula R≡nocc(b, V, k)⇔nocc(b, W, k). Finally, applying textual replacement, we obtain perm(V, W )∧v=b∧w=b. 3 Similarity This section describes an automatic method to introduce recursion by a folding step. It is based on the notion of similarity. Basically, similarity represents a decidable relation between two parsed formulas. Definition 3.1 (Parsing Tree) Let Sbe a formula in prenex normal form. We say that P arse(S)(graphical example in figure 1) is the parsing tree for Siff it is a tree representation of Swhere (a) each leaf node in P arse(S)represents a literal in S. (b) each non-leaf node in P arse(S)represents either a quantified set of variables Qτx, ..., z or a logical connective (∧,∨,⇒,⇔) in Sand (c) each node in P arse(S) has unique identification by means of a number with format lx ···xp. The digit l represents the level where a node is located in P arse(S). The digit pdecides if the node is located either at the left-hand side (p= 1) or at the right-hand side (p= 2) of its parent (if it exists). By default, nodes without brother nodes have p= 1. The digits x···xrepresent the identification of the parent node. The root node is an exception, it has not any parent therefore we consider a fixed identification for it equal to 1. In this way, a node identification determines univocally the position of a node in a parsing tree. We say that a preterminal node in P arse(S)is any non-leaf node in P arse(S)with at least one leaf node as child. Folding by Similarity Two formulas can be compared by the structure of their quantifiers and logical connectives. These measures are called similarity with respect to quantification and similarity with respect to logical connectives respectively. In the following definitions, we consider that S1and S2are two formulas in prenex normal form. Definition 3.2 (Similarity Function) We say that fis a similarity function from the node identification domain of P arse(S1)to the node identification domain of P arse(S2)iff each non-leaf n1∈P arse(S1)is mapped to a non-leaf node n2= f(n1)∈P arse(S2)where quantifier/connective in n1coincides with quantifier/connective in n2and the level of n2is greater than or equal to the level of n1. Definition 3.3 (Similarity w.r.t. Quantification) We say that S2is similar to S1w.r.t. quantification iff for each non-leaf node n1∈P arse(S1)containing the quantified set of variables Qτx1, ..., xnthere exists a non-leaf node n2=f(n1)∈ P arse(S2)containing the quantified set of variables Qτy1, ..., ymsuch that (a) m≥ nand (b) there exist two sequences of nodes, M1from P arse(S1)and M2from P arse(S2), with M1=M−1 2where M1contains n1and its predecessors (from bottom to up) and M2contains n2and its predecessors (from bottom to up). (M−1 2is obtained by applying f−1, when defined, to elements in M2). If S2is similar to S1w.r.t. quantification then finduces a set of possible renaming substitutions for variables in S1(from variables in S2) which agrees w.r.t. quantification. If QτX is the set of quantified variables in n1and QτYis the set of quantified variables in n2=f(n1)then finduces substitutions of the form {(xj, yk)}with xj∈Xand yk∈Y. In figure 5, S2is similar to S1w.r.t. quantification: Q=∀Nat X={a, z}Y={b, k, v, w} Q=∀Seq(Nat)X={L, S}Y={V, W } and some examples of substitutions induced by fare: {(a, b),(z, k),(L, V ),(S, W )} {(a, k),(z, v),(L, W ),(S, V )}... Definition 3.4 (Similarity w.r.t. Logical Connectives) We say that S2is indepth similar to S1iff for each non-leaf node n1∈P arse(S1)containing a logical connective there exists a non-leaf node n2=f(n1)∈P arse(S2)and there exist two sequences of nodes, M1from P arse(S1)and M2from P arse(S2), with M1=M−1 2 where M1contains n1and its predecessors (from bottom to up) and M2contains n2 and its predecessors (from bottom to up). We say that S2is in-breadth similar to S1 iff for each level l > 1of P arse(S1)with N1,l ={lx1p1, ..., lxkpk}as the set of all nodes in lcontaining logical connectives, there exists a set of nodes in P arse(S2), possibly from several levels, say l1, ..., lj, of the form N2,{l1,...,lj}={π1f(x1)p1ς1,...,- πkf(xk)pkςk}where πiand ςi(i= 1..k)are (sub)sequences of numbers. If the node with identification 1(level l= 1) of P arse(S1)contains a logical connective then there exists a node identification in P arse(S2)of the form πf(1)ςin P arse(S2) where πand ςare (sub)sequences of numbers. We say that S2is similar to S1w.r.t. logical connectives iff S2is in-depth similar and in-breadth similar to S1. APPIA-GULP-PRODE 2001 1 ⇔ 1 ⇔ 2 1 1 ∧ 2 1 2 ∨ 2 1 1 ∨ 2 1 2 ∨ 3 2 1 1 1 ∧ 32112 ∧ L e v e l 1 L e v e l 2 L e v e l 3 Figure 2: S2is similar to S1with respect to logical connectives. For example, in figure 2 we show an example of similarity with respect to logical connectives between the formulas S1and S2(for legibility reasons, each rirepresents a ground literal): S1: (r1∧r2)⇔(r3∨r4) S2: ((r5∧r6)∨(r7∧r8)) ⇔(r9∨r10)) In-depth similarity: f(1) = 1 M1={1}M2={1}M−1 2={1} f(211) = 32111 M1={211,1}M2={32111,211,1}M−1 2={211,1} f(212) = 212 M1={212,1}M2={212,1}M−1 2={212,1} In general, if fexists then it may not be unique. For example, the node n211 ∈ P arse(S1) can also be mapped to the node n32112 ∈P arse(S2) obtaining in this way another f. In-breadth similarity (in relation to the definition 3.4, bold numbers have been used for xjpjin N1,l and for f(xj)pjin N2,{l1,...,lj}): l= 2 (level 2), x1= 1, p1= 1, x2= 1, p2= 2, N1,2={211,212} f(1) = 1, π1= 32, ς1= 1, π2= 2, ς2=∅, N2,{2,3}={32111,212} In figure 3 we show an example of non-similarity (non in-depth similarity) with respect to logical connectives between the formulas S3and S4. S3: (r1∧r2)⇔(r3∨r4) S4: ((r5∧r6)∨(r7∧r8)) ⇔r9 Non in-depth similarity: f(1) = 1 M1={1}M2={1}M−1 2={1} f(212) = 211 M1={212,1}M2={211,1}M−1 2={212,1} f(211) = 32111 M1={211,1}M2={32111,211,1}M−1 2={211,212,1} f(211) = 32112 M1={211,1}M2={32112,211,1}M−1 2={211,212,1} Folding by Similarity 1 ⇔ 1 ⇔ 2 1 1 ∧ 2 1 2 ∨ 2 1 1 ∨ 3 2 1 1 1 ∧ 32112 ∧ L e v e l 1 L e v e l 2 L e v e l 3 Figure 3: S4is not similar to S3with respect to logical connectives. There is not any fsuch that M1=M−1 2for the node n211 ∈P arse(S3). In figure 4 we show another example of non-similarity (non in-breadth similarity) with respect to logical connectives between the formulas S5and S6: S5: (r1∧r2)⇔(r3∨r4) S6: (r5∧r6)∨(r7⇔((r8∨r9)∧(r10 ∧r11))) In-depth similarity: f(1) = 211,M1={1}M2={211},M−1 2={1} f(211) = 4321222,M1={211,1}M2={4321222,32122,212,1},M−1 2={211,1} f(212) = 4321221,M1={212,1}M2={4321221,32122,212,1},M−1 2={212,1} Non in-breadth similarity: l= 2 (level 2), x1= 1, p1= 1, x2= 1, p2= 2, N1,2={211,212} f(1) = 212, π1= 43, ς1= 1, π2= 43, ς2= 2, N2,{4}={4321221,4321222} Definition 3.5 (Similarity) Let S2be similar to S1w.r.t. quantification and logical connectives by a function f. Let Lbe the set of all literals in S1. Let NLeaf1 be the set of all preterminal nodes in P arse(S1). Let NLeaf2be the set of nodes n2∈P arse(S2)with n2=f(n1)and n1∈NLeaf1. Let Leaf2be the set of leaf nodes in subtrees of P arse(S2)with root node n2∈NLeaf2. We say that S2is similar to S1iff there exist a SLeaf2⊆Leaf2, with Kas the set of literals in nodes of SLeaf2, and a substitution σinduced by fsuch that Lσ =K. For example, in figure 5, we show the similarity between S1≡nocc(a, L, z)⇔ nocc(a, S, z) and S2≡(v=b∧nocc(b, V, k))⇔(w=b∧nocc(b, W, k)). Similarity w.r.t to quantification: f(1) = 1 f(211) = 211 Similarity w.r.t. logical connectives (In-depth similarity): APPIA-GULP-PRODE 2001 1 ⇔ 1 ∨ 2 1 1 ∧ 2 1 2 ∨ 2 1 1 ∧ 2 1 2 ⇔ 4 3 2 1 2 2 1 ∨ 4321222 ∧ L e v e l 1 L e v e l 2 L e v e l 3 32122 ∧ L e v e l 4 Figure 4: S6is not similar to S5with respect to logical connectives. 1 za  ,∀ 2 11 SL   ,  ∀ 3 2 111 ⇔ 4 3 2 1111 4 3 2 1112 ),,( zLan o c c ),,( zSan o c c 1 wvkb  ,,,∀ 2 11 WV   ,  ∀ 3 2 111 ⇔ 4 3 2 1111 4 3 2 1112 ∧ ∧ 5 4 3 2 11111   = 5 4 3 2 11112 ),,( kVbn o c c 5 4 3 2 1112 1   = 5 4 3 2 1112 2 ),,( kWbn o c c      Figure 5: An example of similarity. Folding by Similarity f(32111) = 32111 M1=M−1 2={32111,211,1} Similarity w.r.t. logical connectives (In-breadth similarity): l= 3 f(211) = 211 N1,3={32111}N2,{3}={32111} NLeaf1={32111}NLeaf2={32111} Leaf2={543211111,543211112,543211121,543211122} SLeaf2={543211112,543211122} Substitution σinduced by f: σ={(a, b),(z, k),(L, V ),(S, W )} L={nocc(a, L, z), nocc(a, S, z)}, K ={nocc(b, V, k), nocc(b, W, k)}, Lσ =K 3.1 Algorithmic Justification for Similarity The constructive nature of definitions 3.3, 3.4 and 3.5 can be justified in an algorithmic way. Different searching algorithms can be proposed for the construction of the similarity function f. We propose a construction following an incremental style. First, fis constructed in order to decide only about similarity w.r.t. quantifiers. Then, we search for a substitution induced by (this incomplete) f. Finally, we search for a remaining part of fwhich decides about similarity w.r.t. logical connectives. Our searching algorithm follows a generate-and-test strategy. It is possible to explore the complete search space due to the finite number of quantifiers and logical connectives in a formula. Initially, a sequence of non-leaf node identifications is constructed by traversing P arse(S1) in a breadth-first way. For example, for P arse(S1) in figure 5 we obtain SeqS1: SeqS1={1,211,32111} From this sequence, the subset of nodes containing quantified set of variables is selected. Then, a generate and test strategy is suffice to construct (an incomplete due to the incremental construction) fwhich decides about similarity w.r.t. quantifiers. The generate-part generates a tentative ffor each node in this subset. Hence, each node containing a quantified set of variables of the form QτXin P arse(S1) is bounded to a node containing a quantified set of variables of the form QτY. The test part decides about conditions (a) and (b) in definition 3.3. If it is not possible to construct an fin these terms then we conclude that there is not any similarity w.r.t. quantification and then there is not any similarity f. For example, for P arse(S1) in figure 5, the subset of nodes containing quantified set of variables is equal to {1,211}. f(1) = 1 Qτ=∀Nat X={a, z}Y={b, k, v, w} f(211) = 211 Qτ=∀Seq(Nat)X={L, S}Y={V, W }