Constructing Recursions by Similarity

Constructing Recursions by Similarity 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 [4], [5], [6],[7], [8], [16], [2]. 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 [1], [5], [13], [15], [14], [18]. 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 S defines a (many-sorted) first-order language with types Nat (natural numbers) constructed from the function symbols 0 and s and 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 = {Types : Nat generated by 0; s Seq (Nat) generated by empty; conc D= : 0 = 0  true0 = 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))} F. J. Galán, J. M. Cañete and V. J. Diaz Madrigal Dept. of Languages and Computer Systems. Faculty of Computer Science of Seville Dept. de Lenguajes y Sistemas Informáticos. Av. Reina Mercedes s/n. 41012.Sevilla. fax:34 954557139 e-mail:[email protected] 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, S and z in Dperm, we obtain D1 and then unfolding D1 w.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: 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 dificult to achieve an “automatic answer” to these questions. Our method follows a constructive approach. A comparison based on the notion of similarity between D2 and Dperm is needed to decide about first question. Only if first question is answered affirmatively then a similarity-based folding rule is applied to D in order to answer second question. Our work is explained in the following manner. Section 2 defines the form of our specifications and a nonconstructive 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. DEFINITION 2.1 (SYNTAX OF A FORMULA) A many sorted (typed) first order language is assumed to write our formulas. A formula where is a universal or existential quantifier defined on a type is different from for , and F contains 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, 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 [12]. For legibility reasons, we omit subscripts when a type can be induced clearly in a formula and expressions such as can be collapsed into equivalent expressions . For example, the formula can be collapse into the equivalent formula . 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 v is a variable and t is a (ground) term. A substitution is a set of variable substitutions. and be two sets of variables where is different from and is different from . Let and be two sets of quantifiers for variables in X and Y respectively. We say that is a renaming substitution which agrees w.r.t. quantifications iff (a) X Y = and (b) with . DEFINITION 2.3 (SPECIFICATION) An if-and-only-if axiom is a formula of the form (e.g. axioms for =, nocc and perm relation symbols in ). The symbol is called the defined symbol. The atom ( , ...; ) is called the left-hand side of the axiom and the (sub)formula R() is called the right-hand side of the axiom. A specification for a relation symbol is the set D of all axioms with the same defined symbol. In the following, we use to identify the axiom in D . Definition 2.4 (Context) A context is a set of types and specifications for relation symbols. Types are constructed from function symbols appearing in . is atomically complete if, for every ground atom , either or . has isoinitial model M iff for every ground literal . Therefore, the meaning of a relation r in is the set of all ground literals defined on r such that . 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))) 11 1 Some authors have studied the problem of the existence of isoinitial models for theories in general [3] and some effective criteria have been proposed to construct consistent theories. Following [11], a context admits an isoinitial model if and only if it is atomically complete. By hypothesis, we assume that our contexts are consistent in this way. Definition 2.5 (Folding Rule) A folding rule is a transformation rule intended for replacing a subformula by an atom. Let be a formula and be an axiom for in . We say that is obtained from folding with respect to where (a) There exist subformula in and substitution such that and (b) represents the textual replacement of in . For example, the formula can be folded with respect to . Applying the substitution to the right-hand side of the axiom in we obtain the subformula . Finally, applying textual replacement, we obtain perm . 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 S be a formula in prenex normal form. We say that Parse(S) (graphical example in figure 1) is the parsing tree for S iff it is a tree representation of S where (a) each leaf node in Parse(S) represents a literal in S. (b) each non-leaf node in Parse(S) represents either a quantified set of variables or a logical connective ( ) in S and (c) each node in Parse(S) has unique identification by means of a number with format . The digit l represents the level where a node is located in Parse(S). The digit p decides 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 represent 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 Parse(S) is any non-leaf node in Parse(S) with at least one leaf node as child. 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 and are two formulas in prenex normal form. DEFINITION 3.2 (SIMILARITY FUNCTION) We say that f is a similarity function from the node identification domain of Parse() to the node identification domain of Parse() iff each non-leaf Parse() is mapped to a non-leaf node Parse() where quantifier/connective in coincides with quantifier/ connective in and the level of is greater than or equal to the level of . DEFINITION 3.3 (SIMILARITY W.R.T. QUANTIFICATION) We say that is similar to w.r.t. quantification iff for each non-leaf node Parse() containing the quantified set of variables there exists a non-leaf node Parse() containing the quantified set of variables such that (a) m n and (b) there exist two sequences of nodes, from Parse() and from Parse( ), with where contains and its predecessors (from bottom to up) and contains and its predecessors (from bottom to up). ( is obtained by applying , when defined, to elements in ). If is similar to w.r.t. quantification then f induces a set of possible renaming substitutions for variables in (from variables in ) which agrees w.r.t. quantification. If is the set of quantified variables in and is the set of quantified variables in then f induces substitutions of the form with and . In figure 5, is similar to w.r.t. quantification: and some examples of substitutions induced by f are: Definition 3.4 (Similarity w.r.t. Logical Connectives) We say that is in-depth similar to iff for each nonleaf node Parse() containing a logical connective there exists a non-leaf node Parse( ) and there exist two sequences of nodes, from Parse() and from Parse( ), with where contains and its predecessors (from bottom to up) and contains and its predecessors (from bottom to up). We say that is in-breadth similar to iff for each level of Parse() with as the set of all nodes in containing logical connectives, there exists a set of nodes in Parse( ), possibly from several levels, say , of the form and are (sub)sequences of numbers. If the node with identification 1 (level = 1) of Parse() contains a logical connective then there exists a node identification in Parse() of the form in Parse() where and are (sub)sequences of numbers. We say that is similar to S1 w.r.t. logical connectives iff is in-depth similar and in-breadth similar to . For example, in figure 2 we show an example of similarity with respect to logical connectives between the formulas and (for legibility reasons, each represents a ground literal): In general, if f exists then it may not be unique. For example, the node Parse() can also be mapped to the Parse() obtaining in this way another f. In-breadth similarity (in relation to the definition 3.4, bold numbers have been used for in and for in : In figure 3 we show an example of non-similarity (non in-depth similarity) with respect to logical connectives between the formulas and . There is not any f such that for the node . In figure 4 we show another example of non-similarity (non in-breadth similarity) with respect to logical connectives between the formulas and : DEFINITION 3.5 (SIMILARITY) Let be similar to w.r.t. quantification and logical connectives by a function f. Let L be the set of all literals in . Let N Lea be the set of all preterminal nodes in Parse( ). Let N Lea be the set of nodes Parse() with and . Let Lea be the set of leaf nodes in subtrees of Parse() with root node . We say that is similar to iff there exist a , with K as the set of literals in nodes of , and a substitution induced by f such that . For example, in figure 5, we show the similarity between and S2 Similarity w.r.t to quantification: Similarity w.r.t. logical connectives (In-depth similarity): 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, f is 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 f which 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 Parse() in a breadth-first way. For example, for Parse() in figure 5 we obtain : From this sequence, the subset of nodes containing quantified set of variables is selected. Then, a generate and test strategy is su±ce to construct (an incomplete due to the incremental construction) f which decides about similarity w.r.t. quantifiers. The generate-part generates a tentative f for each node in this subset. Hence, each node containing a quantified set of variables of the form in Parse() is bounded to a node containing a quantified set of variables of the form . The test part decides about conditions (a) and (b) in definition 3.3. If it is not possible to construct an f in 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 Parse(S1) in figure 5, the subset of nodes containing quantified set of variables is equal to . The set of all tentative substitutions induced by (our incomplete) f is computed in the following manner. For each pair of quantified set of variables and by f, the set of all possible substitutions is calculated by means of a cartesian product. Then, the set of all tentative substitutions induced by f is calculated by the cartesian product of these substitutions. The calculation of is a terminating problem due to the finite number of variables in a formula. For example, in our example (fig. 5): Then, we select the sets of literals L from Parse( ) and K from Parse(). Then is any substitution in such that . A generate and test strategy is suffice to explore the search space. Only if K does not exist or there is not any such that then we conclude that there is not similarity w.r.t. quantification and then there is not any similarity f. In a similar way, we construct the remaining part of f which is intended to decide about similarity w.r.t. logical connectives. A generate and test strategy is suffice to explore the search space. The generate-part generates a tentative (remaining part of) f. A breadth-first search is suffice to construct tentative f’s. The test-part decides about in-depth and in-breadth similarities induced by each tentative f. The search space for the remaining part of f is finite due to the finite number of logical connectives in a formula. In our example, the remaining part of f is only determined by the selection f (32111) = 32111. Finally, for our example (fig. 5): Only if the remaining part of f can not be constructed then we conclude that there is not similarity w.r.t. logical connectives and then there is not any similarity f. 4 Similarity-based Folding Rule In this section, a similarity-based folding rule is defined. Basically, it is a constructive definition of the folding rule in definition 2.5. DEFINITION 4.1 (EVALUATION RULE) Let S be a formula in the language of the context constructed from literals . We say that is obtained from S evaluating the set of literals if and only if is of the following form: For example, let be a formula in the language of . Let and be two literals in S. Then A formula S(true; false; ) constructed from literals and propositions true, false is transformed into the formula Srew by application of rewrite rules repeatedly. For example, let be a formula. represents the simplified form of S obtained after the application of (6), (5) and (9) rewrite rules. DEFINITION 4.3 (SIMILARITY-BASED FOLDING RULE) Let S be a formula in the language of . Let be a relation in . Let be an axiom in . We say that is obtained from S folding by similarity with respect to 1. The variables appearing only in but not in do not appear in S. 2. K is the set of all literals in S. 3. S is similar to , where Lj is the set of all literals in and is a (sub)set of literals of S and is the substitution such that . 4. ( ( ))rew is obtained from S evaluating (definition 4.1) literals not in and then applying rewrite rules (definition 4.2) repeatedly. For example, let be a formula in the language of . Let be the axiom in is the set of all literals in S. S is similar to (definition 3.5). Let be the set of literals in the right-hand side of the axiom in and let be the set of literals in such that Then, let THEOREM 4.1 (CORRECTNESS OF THE EVALUATION RULE) Let be a formula in the language of constructed from literals . Let be the formula obtained from evaluating the set of literals . Let M be an isoinitial model for . Then Proof 4.1 Proof of . The evaluation rule (definition 4.1) constructs by means of mutually exclusive disjunctions representing all possible evaluation cases for literals in . Suppose (by absurdum) that is model for a ground instance of S and it is not model for the respective ground instance of . By hypothesis, is atomically complete (definition 2.4) and then there exists a proof in for the ground instance of S but there is not a proof in for the ground instance of . Hence, we conclude that does not consider all possible evaluations for literals in S. Proof of . If M is model of a ground instance of then M is model of only one instance of their disjunctions and then, by construction, it is a model of the respective ground instance of S. Definition 4.2 (Rewrite Rules) In order to simplify specifications, we consider a set of rewrite rules of the form in presence of negations and false and true propositions. A formula constructed from literals and propositions true, false is transformed into the formula Srew by application of rewrite rules repeatedly. rew where THEOREM 4.2 (CORRECTNESS OF THE SIMILARITY-BASED FOLDING RULE) Let S be a formula in the language of . Let r be the relation in . Let be an axiom in . Let S be the formula obtained from S folding by similarity with respect to (definition 4.3). Then Proof 4.2 The similarity between S and implies the existence of a substitution such that where represents the set of all literals in and represents a (sub)set of literals in S (definition 4.3). The formula represents the evaluation of S with respect to literals not in and by theorem 4.1, this formula is equivalent to S. This formula is composed by disjunctions . Applying rewrite rules on each disjunction, we obtain a formula of the form: 5 Conclusions The objective of applying transformations is to filter out a new version of the specification where recursion may be introduced by a folding step. Several (nonconstructive) j