Formal Correctness of a Quadratic Unification Algorithm

Formal Correctness of a Quadratic Unification Algorithm Jos´e–Luis Ruiz–Reina, Francisco–Jes´us Mart´ın–Mateos, Jos´e–Antonio Alonso and Mar´ıa–Jos´e Hidalgo Computational Logic Group Dept. of Computer Science and Artificial Intelligence, University of Seville E.T.S.I. Inform´atica, Avda. Reina Mercedes, s/n. 41012 Sevilla, Spain E-mails: {jruiz,fjesus,jalonso,mjoseh}@us.es Abstract. We present a case study using ACL2 [5] to verify a non-trivial algorithm that uses efficient data structures. The algorithm receives as input two first-order terms and it returns a most general unifier of these terms if they are unifiable, failure otherwise. The verified implementation stores terms as directed acyclic graphs by means of a pointer structure. Its time complexity is O(n2) and its space complexity is O(n), and it can be executed in ACL2 at a speed comparable to a similar C implementation. We report the main issues encountered to achieve this formally verified implementation. 1. Introduction It is generally accepted that there is a trade-off between the efficiency of an implementation and the simplicity of its formal correctness proof: having more sophisticated control and data structures increases the effort needed to prove its correctness. That is the reason why most of the proofs about well-known algorithms that have been carried out using theorem provers are done reasoning about non-efficient naive implementations. Nevertheless, the ACL2 system [5] has already been demonstrated capable of efficient implementations of microarchitectural level processor models (see [4], for example) that can be executed at C–like performance. In this way, in addition to having a high-speed simulation model one has the additional benefit of being able to prove formal properties of that model. The core of the implementation is a “next state” function that receives as input a data structure representing the current state of the machine and returns an updated machine state. A single-threaded object (stobj in the following) is usually employed to represent the machine state. These data structures in ACL2 allow constant time access and destructive updates, while maintaining an applicative semantics for reasoning about it. In light of this, and given our previous experience in the development of formal theories related to symbolic computation systems [8], we decided to apply ACL2 to obtain a formally verified and efficient 2 implementation of some non-trivial algorithm in this area. Our goal was twofold: compare the execution efficiency obtained in ACL2 with other implementations done in other languages, and explore the main issues encountered during the verification effort of the correctness of that implementation. For this case study, we have chosen the implementation of a syntactic unification algorithm. The algorithm receives as input two first-order terms and it returns a most general unifier of these terms if they are unifiable, failure otherwise. Unification algorithms are both theoretically interesting and practically important, since they are at the heart of many symbolic computation systems [2]. The verified implementation stores terms as directed acyclic graphs (dags in the following) by means of a pointer structure stored in an array field of a stobj. In this way, we obtain a time complexity of O(n2) and a space complexity of O(n). We followed quite closely a Pascal implementation of the algorithm described in Section 4.8 of [1], which in turn is based on the exposition by Corbin and Bidoit [3]. It should be noted that we do not prove the complexity of our implementation in ACL2; a hand-proof of this complexity can be found in [1]. The main feature of our formal proof of the correctness of the algorithm is a clear separation between the logic of the process of unification, the data structures used, the specific execution control of the algorithm and the details related to its execution in ACL2. To cope with the complexity of the whole formal proof, we introduce each of these aspects in successive refinement steps. The description presented here is guided and motivated by these steps. This paper is a revised version of [10], presented at the ACL2 Workshop 2004. We do not present here details of the proofs, and some of the function definitions will be omitted. We urge the interested reader to consult [11], where the complete source code of the development (with detailed comments) is available. 2. An ACL2 Overview We now give a brief overview to the ACL2 system. ACL2 stands for “A Computational Logic for an Applicative Common Lisp.” Roughly speaking, ACL2 is a programming language, a logic and a theorem prover. Its programming language is an extension of an applicative subset of Common Lisp [12] (we will assume the reader familiar with this language). The ACL2 logic describes the programming language, with a formal syntax, axioms and rules of inference: the applicative subset of Common Lisp is a model of the ACL2 logic. Finally, the 3 theorem prover provides support for mechanized reasoning in the logic. Thus, the system constitutes an environment in which programs can be defined and executed, and their properties can be formally specified and proved with the assistance of a theorem prover. The logic is a first-order logic with equality. The syntax of its terms is that of Common Lisp and therefore uses prefix notation. Formulas are quantifier-free and their variables are considered to be universally quantified. For example, the following formula may be read as “for all natural numbers nand x, with xeven and n > 0, xnis even”: (defthm evenp-expt (implies (and (natp n) (> n 0) (natp x) (evenp x)) (evenp (expt x n))) The logic includes axioms for propositional logic and for a number of primitive Common Lisp functions and data types. Rules of inference include those for propositional calculus, equality, instantiation and a principle of proof by induction. By the principle of definition, new function definitions (using defun) are admitted as axioms only if there exists an ordinal measure in which the arguments of each recursive call (if any) decrease, thus proving its termination. This ensures that no inconsistencies are introduced by new definitions. The ACL2 theorem prover is an integrated system of ad hoc proof techniques, including simplification and induction among them. Simplification is a process combining term rewriting with some decision procedures (linear arithmetic, type set reasoner, etc.) Sophisticated heuristics for discovering an (often suitable) induction scheme is one of the key features in ACL2. The command defthm starts a proof attempt, and, if it succeeds, the theorem is stored as a rule (in most cases, a conditional rewriting rule). For example the above theorem evenp-expt, once proved, would allow the prover to rewrite an instance of the term (evenp (expt x n)) to the boolean constant t(true), provided that the corresponding instantiated conditions of the rule can be established. The theorem prover is automatic in the sense that, once defthm is submitted, the user can no longer interact with the system. However, in some sense, it is interactive. Often, non-trivial results can not be proved on a first attempt, and then the role of the user is important: she has to guide the prover by a suitable collection of definitions and lemmas, used in subsequent proofs as rewriting rules. These lemmas are suggested by a preconceived hand proof (at a higher level) or by inspection of failed proofs (at a lower level). This kind of interaction 4 is called “The Method” by the authors of the system [5]. We followed “The Method” to obtain the results presented in this paper. A relevant feature of ACL2 is executability: since its axioms and rules of inference describe a subset of Common Lisp, most ground expressions in the logic are directly executable in the host Lisp (as opposed to deducing their values via the axioms). Nevertheless, this simple relationship is complicated by the fact that not all Common Lisp functions are defined on all inputs: the Common Lisp standard introduces the notion of “intended domain” of a primitive function. Outside this intended domain the behavior of a function is not specified. In contrast, in the ACL2 logic functions are total: that is, every application of a function defined has a completely specified result. ACL2 formalizes the notion of intended domain by means of guards. The guard of a function (primitive or defined) is a formula describing its intended domain. Guard verification is the process of proving that if a function is called on an input satisfying its guard, then the evaluation of this call will proceed without any guard violation. Roughly speaking, the proof obligations generated by the guard verification process state that the guard of a function implies the guards of its definition body. Guards have no effect from the logical point of view, but they provide a means of (formally supported) direct execution in the host Common Lisp, For more information on ACL2, the best reference is [5]. For a detailed and updated description of all the system details, we also recommend visiting the ACL2 home page [6] and the user’s manual in it. 3. Syntactic Unification Let us recall in this section some basic concepts and results about syntactic unification of first-order terms, our target example. A complete description of the theory of unification can be found in [2]. An equation is an ordered pair of first-order terms, denoted as t1≈ t2, and a system of equations is a finite set of equations. A substitution σis a solution of the equation t1≈t2if σ(t1) = σ(t2). We say that a substitution is a solution of a system of equations Sif it is a solution of every equation in S. We say that the system is solvable if it has a solution. Usually, a solvable system has more than one solution, but we will be interested in most general solutions. Given two substitutions σ and δ, we say that σis more general than δif there exists a substitution γsuch that δ=γ◦σ, where ◦denotes functional composition. We say 5 that a solution of Sis a most general solution (mgs in the following) if it is more general than any other solution of S. As a particular case, we say that two terms t1and t2are unifiable if there exists a solution (called unifier) of the system {t1≈t2}. A most general unifier (mgu in the sequel) of t1and t2is a most general solution of that system. Finally, a (syntactic) unification algorithm is an algorithm that decides whether two given terms are unifiable, and in that case it returns a most general unifier. In the literature, it is quite common to describe syntactic unification algorithms by means of the relation ⇒ugiven by the transformation rules presented in Figure 1. This set of rules is known as the MartelliMontanari transformation system. The rules act on pairs of systems of equations of the form S;U(the symbol ⊥represents unification failure). Intuitively, the system Scan be seen as a set of equations to be solved, and the system Uas a (partially) computed unifier. We call the pair S;Uaunification problem. Note that we are identifying a system of equations of the form {x1≈t1,...,xn≈tn}, where the xi are variables, with the substitution {x17→ t1,...,xn7→ tn}. If none of the xiappear in any of the tj, we say that the system is in solved form. Note that every system in solved form is an mgs of itself. The intuitive idea is that, in order to find a most general solution of a system of equations S, we can iteratively apply (in a “don’t care” nondeterministic manner) the rules of ⇒u, starting with the unification problem S;∅, until either a unification problem of the form ∅;Uor ⊥is obtained. It can be proved that this process must terminate and that Sis solvable if and only if ⊥is not derived; in that case Uis a most general solution of S. Note that the transformation relation ⇒udoes not describe any concrete unification algorithm. Roughly speaking, a unification algorithm can be designed by using a data structure to represent first-order terms and substitutions, and choosing a strategy to apply the rules, starting with the pair of systems {t1≈t2};∅(where t1and t2are the two given input terms). This transformation based specification of the unification process allows us to concentrate on its logical properties without the burden of data structures or control issues. 4. Formalization of the Unification Transformation Relation The first step is to formalize in ACL2 the transformation relation ⇒u and prove its main properties. It turns out that these properties are more easily proved if we consider a “natural” representation of firstorder terms and substitutions, even though this representation may 6 Delete: {t≈t} ∪ R;U⇒uR;U Occur-check: {x≈t} ∪ R;U⇒u⊥if x∈ V(t) and x6=t Eliminate: {x≈t} ∪ R;U⇒uθ(R); {x≈t} ∪ θ(U) if x∈X,x /∈ V(t) and θ={x7→ t} Decompose: {f(s1, ..., sn)≈f(t1, ..., tn)} ∪ R;U⇒u {s1≈t1, ..., sn≈tn} ∪ R;U Clash: {f(s1, ..., sn)≈g(t1, ..., tm)} ∪ R;U⇒u⊥ if n6=mor f6=g Orient: {t≈x} ∪ R;U⇒u{x≈t} ∪ R;Uif x∈X,t /∈X Figure 1. Martelli–Montanari transformation system not be the most efficient. In particular, in this first stage terms are represented in prefix notation, using lists (except variables, which are represented by atomic objects). For example, the term f(x, g(y), h(x)) is represented by the list (f x (g y) (h x)). Substitutions are represented as association lists, and systems of equations as lists of dotted pairs of terms. A unification problem is a list with two elements: a system and a substitution. The failure ⊥is represented as nil. In the sequel, this representation of terms and substitutions in prefix form, using lists, will be referred to as prefix representation or prefix notation. Let us now briefly describe how we have formalized in ACL2 the relation ⇒u. Note that one step of transformation of ⇒uis determined by the rule applied and the equation where that rule is applied. To formalize this intuitive idea in ACL2, we define ⇒uby means of operators. In this context, an operator is a dotted pair of the form (name .i)where name is one of the rule names in Figure 1 and i is a natural number, corresponding to the i-th equation of the system. Thus, the transformation ⇒ucan be seen as applying one operator to a unification problem. Not every operator can be applied to every unification problem, since rules have some conditions that have to be met. For example, the operator (eliminate . 5) can be applied to a unification problem only if it has at least five equations to be solved and its fifth equation is of the form x≈t,xbeing a variable and not occurring in t. These considerations lead us to formalize in ACL2 the relation ⇒uby means of two functions: −(unif-legal-p upl op), checking the conditions required to apply a given operator op to a unification problem upl (in prefix notation). −(unif-reduce-one-step-p upl op), returning the transformed unification problem (in prefix notation) after applying op to upl. 7 With this operator-based representation, we proved in ACL2 the main properties of ⇒u: 1. The set of solutions of a unification problem is preserved in each transformation step. 2. If the second system of a unification problem is in solved form, then the transformed unification problem has its second system in solved form. 3. The transformation relation is terminating. For example, these are the ACL2 theorems establishing property 1 above: (defthm mm-preserves-solutions-1 (implies (and (unif-legal-p upl op) (solution sigma (both-systems upl))) (solution sigma (both-systems (unif-reduce-one-step-p upl op))))) (defthm mm-preserves-solutions-2 (implies (and (unif-legal-p upl op) (unif-reduce-one-step-p upl op) (solution sigma (both-systems (unif-reduce-one-step-p upl op)))) (solution sigma (both-systems upl)))) (defthm mm-preserves-solutions-3 (implies (and (unif-legal-p upl op) (not (unif-reduce-one-step-p upl op))) (not (solution sigma (both-systems upl))))) Having proved the main properties of one-step transformations, we can easily extend these properties to finite sequences of transformations1. In particular we prove that given two terms t1and t2and a substitution σ, if {t1≈t2};∅∗ ⇒u∅;σ, then σis an mgu of t1and t2, and if {t1≈t2};∅∗ ⇒u⊥, then t1and t2are not unifiable. This result is the key to prove the correctness of a given unification algorithm: it suffices to show that the results computed by the algorithm can be described by the iterative application of a sequence of operators (although the algorithm does not necessarily have to deal explictly with operators). Most of the results about the relation ⇒uhave been reused from a previous formalization of the main properties of the lattice of first-order 1Note that in our formalization, a sequence of transformations can be identified with a list of operators. Each of these operators has to be applicable to the result obtained by the previous one. 8 terms with respect to subsumption [9]. As part of that work, we had defined and verified a unification algorithm based on the transformation system ⇒uacting on terms in prefix notation. For a detailed description of the proofs and a precise statement of the properties mentioned above, we refer the reader to the supporting materials. 5. Representing Terms as Directed Acyclic Graphs Using the prefix representation, a unification algorithm may have exponential complexity in some situations, both in time and space. Consider, for example, the following standard parameterized unification problem, which we will call Un: p(xn,...,x2, x1)≈p(f(xn−1, xn−1),...,f(x1, x1), f(x0, x0)) An mgu of this problem is {x17→ f(x0, x0), x27→ f(f(x0, x0), f(x0, x0)),...} mapping each variable xito a complete binary tree of height i. This mgu is obtained by repeatedly applying the Eliminate rule of ⇒u. Using the prefix representation of terms, it would be necessary to reconstruct the instantiated systems of equations, for each application of the rule. The standard approach to deal with this problem is to use term dags, a kind of pointer structures representing terms where variables can be shared. For example, the graph below represents the equation f(x, g(v, h(x)), h(y)) ≈f(h(u), g(y, v), z). Nodes are labeled with function and variable symbols, and outgoing edges connect every node with dags representing its immediate subterms. We can naturally identify the root node of a term dag with the whole term. Note also that there is a certain amount of structure sharing, at least for the repeated variables: f g x vhy h h f gz u 9 To implement a unification algorithm with this term representation, the main idea is never to build new terms but only create pointers. In particular, the Eliminate rule can be implemented introducing a pointer linking the variable with the term to which this variable is bound; in that way no reconstruction of the term is required in the application of a substitution. In the graph above, these pointers are represented by dashed arrows. The binding for a variable can be determined by following the pointers traversing the graph depth first, from left to right. In this case, the substitution represented is {x7→ h(u), y 7→ h(h(u)), z 7→ h(h(h(u))), v 7→ h(h(u))}, which is an mgu of f(x, g(v, h(x)), h(y)) and f(h(u), g(y, v), z). In ACL2, we have represented a term dag as a list of nodes. In particular, if gis a list representing a term dag, each of its elements represents a node in the graph, uniquely identified by its position index. The nodes store information about its label and its successors, in the following way: −If node irepresents an unbound variable x, then (nth ig) (that is, the i-th element of g) is a dotted pair of the form (x. t)2. −If node irepresents a bound variable, then (nth ig) is an index npointing to the root node of the term to which the variable is bound. −If node iis the root node of a non-variable term f(t1, . . . , tn), then (nth ig) is a dotted pair of the form (f.l), where lis the list of the indices corresponding to the root nodes of t1, . . . , tn. For example, we can represent the term equ(f(x, g(v, h(x)), h(y)), f(h(u), g(y, v), z)) by a list with the following elements (for a better understanding, we marked each element with its position index): 0 8 9 (Y . T) (EQU . (1 9)) (F . (2 3 7)) 1 2 (X . T) 3 (G . (4 5)) 4 (V . T) 5 (H . (6)) 6 2 7 (H . (8)) (F . (10 12 15)) (H . (11)) 10 1211 (U . T) 13 (G . (13 14)) 14 8 4 15 (Z . T) Although with the above conventions one can represent every firstorder term as a list of nodes, the converse is not true. Thus, we need 2We could have used any non-list value as the second element in this dotted pair to distinghish it from the representation of non-variable terms. 16 (defun unif-legal-q-identify (i j g) (and (natp i) (< i (len g)) (term-dag-non-variable-p i g) (natp j) (< j (len g)) (term-dag-non-variable-p j g) (not (equal i j)) (equal (dag-as-term t i g) (dag-as-term t j g)))) (defun unif-reduce-one-step-q-identify (i j S sol g) (list S sol (update-nth i j g))) The functions unif-legal-q and unif-reduce-one-step-q define the extended transformation relation. Note that this extended relation is defined on a term dag representation and includes all the transformation rules of ⇒uas well as identifications: (defun unif-legal-q (upl op) (if (equal (first op) ’identify) (unif-legal-q-identify (second op) (third op) (third upl)) (unif-legal-d upl op))) (defun unif-reduce-one-step-q (upl op) (if (equal (first op) ’identify) (unif-reduce-one-step-q-identify (second op) (third op) (first upl) (second upl) (third upl)) (unif-reduce-one-step-d upl op))) The following theorems establish the main properties of this extended transformation relation: (defthm unif-reduce-one-step-q-preserves-well-formed-upl (implies (and (well-formed-upl upl) (unif-legal-q upl op)) (well-formed-upl (unif-reduce-one-step-q upl op)))) (defthm unif-reduce-one-step-q-for-identifications (implies (and (well-formed-upl upl) (unif-legal-q upl op) (equal (first op) ’identify)) (equal (upl-as-pair-of-systems (unif-reduce-one-step-q upl op)) (upl-as-pair-of-systems upl)))) That is: −Well-formedness of the dag unification problem is preserved. Note again that this result is not trivial: it means that updating a node by a legal identification do not create cycles in the graph. −An identification does not change the unification problem in prefix form represented by the dag unification problem. That is, no “harm” is done by identifications, from the point of view of the unification problem. 17 From these theorems and the results of the previous section, it is not difficult to prove that for every sequence of these transformation steps (including identifications) performed at the dag level, there exists a sequence of transformation steps of ⇒uperformed at the corresponding prefix representation. Therefore, every algorithm whose computation can be described as the iterative application of these rules on dag unification problems is a correct unification algorithm. 8. An Improved Occur Check Before defining the quadratic unification algorithm in the next section, we must fix another technical detail that could cause exponential behavior. Assume that at some point of the unification process, a variable is bound to a term of exponential size, but this term is stored in the term dag in linear size because its subterms are shared. If we have to check the occurrence of a variable in this term, we should avoid visiting these shared subgraphs repeatedly. This exponential behavior may appear with the naive implementation of occur check defined by the function occur-check-d given in Section 5: we do not take care of repeated visits to the same subgraph. To optimize this implementation, we follow the idea given in [1]. We will use a stamp list of integers: the number in position iof this list represents the last time node iof the term dag was visited for occur check. We also use a time counter that will be incremented every time the unification procedure calls to the occur check function. Before visiting a subgraph to check the occurrence of a variable, we check if its stamp information is equal to time. If that is the case we simply return nil, without traversing the subgraph; otherwise we traverse the subgraph, updating the stamp information if the variable does not occur in the subgraph. The definition below implements in ACL2 this improved occur check. Note that it returns a list of two elements: the first is a boolean indicating occurrence and the second is the (possibly modified) stamp list. (defun occur-check-q (flg x h g stamp time) (if (dag-p g) (if flg (let ((p (nth h g))) (if (integerp p) (occur-check-q flg x p g stamp time) (let ((args (cdr p))) (cond ((equal args t) (list (equal x h) stamp)) ((equal (nth h stamp) time) (list nil stamp)) (t (let* ((bool-stamp 18 (occur-check-q nil x args g stamp time)) (bool (first bool-stamp)) (stamp (second bool-stamp))) (if bool bool-stamp (list nil (update-nth h time stamp))))))))) (if (endp h) (list nil stamp) (let* ((bool-stamp (occur-check-q t x (car h) g stamp time)) (bool (first bool-stamp)) (stamp (second bool-stamp))) (if bool bool-stamp (occur-check-q nil x (cdr h) g stamp time))))) (list ’undef stamp))) The following theorem establishes that the result computed by the improved function occur-check-q is consistent with the result computed by the function occur-check-d. (defthm occur-check-d-occur-check-q (implies (occur-check-invariant x h g stamp time) (equal (first (occur-check-q t x h g stamp time)) (occur-check-d t x h g)))) The function occur-check-invariant in this theorem describes an invariant condition that we will prove that is met in every step of our implemented unification algorithm. Roughly speaking, all the numbers in the stamp list have to be strictly smaller than the time counter. 9. A Quadratic Unification Algorithm It is time to define our implementation of a quadratic unification algorithm. That is, having proved the main properties of the rule-based specification of the unification process on term dags, we deal with control issues. Not surprisingly, we simply choose a certain strategy to apply the rules of the extended transformation relation: in our case, we always select the first equation to be solved. To avoid exponential complexity, we need some technical details in order to do identifications properly and also we use the improved occur check defined in the previous section. The function dag-transform-mm-q defines the individual steps of transformation performed by the algorithm. This is the main component of the algorithm. Roughly speaking, the implemented algorithm will apply this function until there are no equations to be solved or failure is detected. 19 (defun dag-transform-mm-q (ext-upl) (let* ((ext-S (first ext-upl)) (equ (first ext-S)) (R (rest ext-S)) (U (second ext-upl)) (g (third ext-upl)) (stamp (fourth ext-upl)) (time (fifth ext-upl))) (if (equal (first equ) ’id) (let ((g (update-nth (second equ) (third equ) g))) ;;; IDENTIFY (list R U g stamp time)) (let ((t1 (dag-deref (car equ) g)) (t2 (dag-deref (cdr equ) g))) (if (equal t1 t2) (list R U g stamp time) ;;; DELETE (let ((p1 (nth t1 g)) (p2 (nth t2 g))) (cond ((dag-variable-p p1) (let* ((bool-stamp (occur-check-q t t1 t2 g stamp time)) (bool (first bool-stamp)) (stamp (second bool-stamp))) (if bool nil ;;; OCCUR-CHECK (let ((g (update-nth t1 t2 g))) (list R (cons (cons (dag-symbol p1) t2) U) g stamp (1+ time)))))) ;;; ELIMINATE ((dag-variable-p p2) (list (cons (cons t2 t1) R) U g stamp time)) ;;; ORIENT ((not (equal (dag-symbol p1) (dag-symbol p2))) nil) ;;; CLASH1 (t (let* ((pairs-bool (pair-args (dag-args p1) (dag-args p2))) (pairs (first pairs-bool)) (bool (second pairs-bool))) (if bool (list (append pairs (cons (list ’id t1 t2) R)) U g stamp time) ;;; DECOMPOSE nil)))))))))) ;;; CLASH2 This function receives as input what we call an extended unification problem. An extended unification problem is a list with five elements: an extended indices system, an indices substitution, a term dag, a stamp list and a time counter. An extended indices system is an indices system that could include also some identification marks of the form (id i j). In this function, the transformation step to apply is determined by the first element of the extended indices system. If this first element is an ordinary equation between indices, then the corresponding rule of ⇒uis applied. If it is an identification mark of the form (id i j), then an identification of the nodes iand jis applied. In order to guarantee that identifications are always done with root nodes of already unified subterms, identification marks are included at every application of the 20 Decompose rule, just after the equations pairing4the arguments of the nodes to be unified. In this way, extended indices systems can be seen as a stack: when an identification mark is at the top of the stack, we are sure that the nodes to be identified have successfully been unified. The function dag-transform-mm-q has to be iteratively applied until the system of equations to be solved is empty or until nil (unsolvability) is obtained. The following function solve-upl-q does this job: (defun normal-form-syst (ext-upl) (not (and (consp ext-upl) (consp (first ext-upl))))) (defun solve-upl-q (ext-upl) (declare (xargs :measure (unification-measure-q ext-upl))) (if (unification-invariant-q ext-upl) (if (normal-form-syst ext-upl) ext-upl (solve-upl-q (dag-transform-mm-q ext-upl))) ’undef)) The condition (unification-invariant-q ext-upl) in the above definition is needed for termination. Among many other properties, it includes the dag-p condition. Termination of solve-upl-q is not trivial at all, and a lexicographic measure has to be supplied to instruct the prover in the termination proof. This measure (given by the function unification-measure-q, omitted here) is mainly based on the measure that justifies the termination of ⇒u. In addition, the function unification-invariant-q defines the properties needed to ensure that the function dag-transform-mm-q is applying a legal transformation step of the extended transformation relation5. Note that this is trivial for the case of non-identification transformations, because the applicability conditions are explicitly checked. Nevertheless, that is not the case for identifications. Recall that an identification can be applied only when the terms pointed by the identified nodes are equal. But this applicability condition is not checked (and that is essential for the efficiency of the algorithm). The key point is that, due to the way the successive transformation steps are carried out, it is guaranteed that every time an identification step is performed, this identification is legal. In other words, there is some “well-formedness” conditions on the extended unification problem that can be seen as an invariant of the unification process, and this invariant condition implies that every transformation step performed 4Given two lists (l1. . . ln)and (m1. . . mk)the auxiliary function pair-args returns the list (((l1.m1)... (ln.mk)) t) if n=k,(nil nil) otherwise. 5And also that we can safely use the improved occur check function. 21 by dag-transform-mm-q is a legal transformation step with respect to the extended transformation relation defined in Section 7. The following theorems establish this fact6: (defthm unification-invariant-q-preserved (implies (and (not (normal-form-syst ext-upl)) (unification-invariant-q ext-upl)) (unification-invariant-q (dag-transform-mm-q ext-upl)))) (defthm transform-mm-q-applies-a-legal-operator (implies (and (not (normal-form-syst ext-upl)) (unification-invariant-q ext-upl)) (unif-legal-q (ext-upl-to-upl ext-upl) (dag-transform-mm-q-op ext-upl)))) (defthm transform-mm-q-applies-an-operator (implies (unification-invariant-q ext-upl) (equal (ext-upl-to-upl (dag-transform-mm-q ext-upl)) (unif-reduce-one-step-q (ext-upl-to-upl ext-upl) (dag-transform-mm-q-op ext-upl))))) We save the reader from the definition of the function unification-invariant-q. It is a very long definition (more than 300 lines of code) including well-formedness properties such as acyclicity of the term dag, the occur-check invariant and the correct placement of the identification marks in the extended indices system stack. Due to this, the above theorem unification-invariant-q-preserved turns out to be the most difficult to prove of all the verification effort. In the above theorems, the function dag-transform-mm-q-op returns the corresponding “witness” operator justifying that dag-transform-mm-q is applying a rule of the extended transformation relation. This means that the exhaustive iteration of dag-transform-mm-q, as implemented by solve-upl-q, is a correct unification procedure. Thus, we are almost done. But before we need to deal with some technical issues related to the execution of the algorithm in ACL2. 10. Execution of the Algorithm in ACL2 The function solve-upl-q in the previous section can be executed in ACL2. But from the practical point of view, this execution is completely unfeasible, mainly for two reasons: 6The function ext-upl-to-upl removes the identification marks, the stamp list and the time counter of an extended dag unification problem. 22 −The term dag is stored in a list. This means that accessing (with nth) and updating (with update-nth) the information of the nodes are not done in constant time. Moreover, updates are not destructive and need copying. −As we have seen, some of the recursive functions implemented have expensive well-formedness conditions (like dag-p or unification-invariant-q) in their bodies, needed for termination. And these conditions would be evaluated in every recursive call. Fortunately, we can fix these two problems. To deal with the first, we will use a single-threaded object. In ACL2, it is possible to declare some objects in the language as single-threaded (stobjs) and perform destructive updates on them. When an object is declared to be single-threaded, ACL2 enforces certain syntactic restrictions on its use, ensuring that in every moment, only one copy of the object is needed. With these restrictions, the destructive updates are consistent with the applicative functional semantics of ACL2. Using stobjs we can combine efficient imperative implementations with the semantic of functional languages to reason about them. The following creates a stobj called terms-dag with two resizable array fields to store the term dag and the stamp: (defstobj terms-dag (dag :type (array t (0)) :resizable t) (stamp :type (array integer (0)) :initially -1 :resizable t)) The effect of this ACL2 form is to introduce the stobj terms-dag and its associated recognizers, creator, accessors, updaters, and length and resize functions for the array fields. In particular, given an index i, the expressions (dagi iterms-dag) and (update-dagi i v terms-dag) respectively access and update (with value v) the i-th cell of the dag array. Similarly, functions stampi and update-stampi are introduced. These operations are executed in constant time and the update is destructive (at the price of syntactic restrictions on the use of terms-dag). Now, we redo all the definitions of the implemented algorithm, taking into account that the term dag is stored in this stobj. It is worth pointing out that the syntactic requirements needed to ensure the single-threadedness of the ACL2 functions that use stobjs are naturally met in this algorithm. The function dag-transform-mm-st below is the stobj counterpart of dag-transform-mm-q. The key point is that from the logical point of view, the dag and stamp arrays of the stobj are lists. Thus it is straightforward to translate the already proved properties about the list version of the algorithm to the stobj version. 23 (defun dag-transform-mm-st (S U terms-dag time) (declare (xargs :stobjs terms-dag) ...) (let* ((equ (car S)) (R (cdr S))) (if (equal (car equ) ’id) ;;; IDENTIFY (let ((terms-dag (update-dagi (second equ) (third equ) terms-dag))) (mv R U t terms-dag time)) (let* ((t1 (dag-deref-st (car equ) terms-dag)) (t2 (dag-deref-st (cdr equ) terms-dag)) (p1 (dagi t1 terms-dag)) (p2 (dagi t2 terms-dag))) (cond ((= t1 t2) (mv R U t terms-dag time)) ;;; DELETE ((dag-variable-p p1) (mv-let (oc terms-dag) (occur-check-st t t1 t2 terms-dag time) (if oc ;;; OCCUR-CHECK (mv nil nil nil terms-dag nil) (let ((terms-dag (update-dagi t1 t2 terms-dag))) (mv R (cons (cons (dag-symbol p1) t2) U) t terms-dag (1+ time)))))) ;;; ELIMINATE ((dag-variable-p p2) (mv (cons (cons t2 t1) R) U t terms-dag time)) ;;; ORIENT ((not (eql (dag-symbol p1) (dag-symbol p2))) (mv nil nil nil terms-dag nil)) ;;; CLASH1 (t (mv-let (pairs bool) (pair-args-mv (dag-args p1) (dag-args p2)) (if bool (mv (append pairs (cons (list ’id t1 t2) R)) U t terms-dag time) ;;; DECOMPOSE (mv nil nil nil terms-dag nil))))))))))) ;;; CLASH2 Another optimization for execution that is worth pointing out is the use of multivalues in functions that returned several values in a list, such as occur-check-q or pair-args. In the stobj version of the algorithm, we used mv and mv-let to handle this (see [6] for details on multivalues). Again, there is no difference from the logical point of view, since according to the logic, mv returns a list. Nevertheless, a list is never created for storing multiple return values during execution, making it more efficient. Let us now deal with the second problem, or how to get rid of the expensive well-formedness conditions in the bodies of some of the recursive functions of our implementation. These conditions are only needed for the logical definitions: they can be safely removed in execution because they are preserved in each recursive call. For that purpose, we use defexec and mbe: this ACL2 feature allows us to associate an “executable body” with a (possibly different) “logical body”. This association will be allowed by the system after proving that on the 24 intended domain of the function the executable body and the logical body are equal. Let us explain this in more detail. In the logic, the expression (mbe :logic logic body :exec exec body)is equal to logic body; the value of exec body is ignored. Nevertheless, for execution in the host Lisp this form macroexpands simply to exec body. The guard verification mechanism plays a key role here. Roughly speaking, the guard proof obligations generated by the above call of mbe are (equal logic body exec body)along with those generated by the executable body. Therefore, whenever a function defined using mbe is called on an input satisfying its guard, then exec body may be safely used in the host Common Lisp to obtain a result, since it is provably equal in the ACL2 logic to logic body. In addition, defexec generates a proof obligation ensuring that the executable body terminates on its intended domain. For example, the following is the complete definition of the function solve-upl-st, the stobj counterpart of the function solve-upl-q defined in the previous section7. Note that the expensive unification- -invariant-q condition is removed in the executable body. (defexec solve-upl-st (S U terms-dag time) (declare (xargs :stobjs terms-dag :guard (and (true-listp S) (unification-invariant-q (list S U (dag-component-st terms-dag) (stamp-component-st terms-dag) time))) ...)) (mbe :logic (if (unification-invariant-q (list S U (dag-component-st terms-dag) (stamp-component-st terms-dag) time)) (if (endp S) (mv S U t terms-dag time) (mv-let (S1 U1 bool terms-dag time1) (dag-transform-mm-st S U terms-dag time) (if bool (solve-upl-st S1 U1 terms-dag time1) (mv S U nil terms-dag time)))) (mv S U nil terms-dag time)) :exec (if (endp S) (mv S U t terms-dag time) (mv-let (S1 U1 bool terms-dag time1) (dag-transform-mm-st S U terms-dag time) 7The functions dag-component-st and stamp-component-st collects in a list the contents of the dag and stamp arrays of the stobj. 25 (if bool (solve-upl-st S1 U1 terms-dag time1) (mv S U nil terms-dag time)))))) The guard verification of this function is not trivial. We have to prove that the property unification-invariant-q is preserved in every recursive call. But essentially, that is the theorem unification- -invariant-q-preserved discussed in the previous section. In general, we used defexec and mbe in the definition of all the recursive functions that need well-formedness conditions in their logical bodies whenever these conditions can be safely removed for execution. In particular, in dereferencing, in occur checking and in the function that builds a term in prefix form from the contents of a term dag. Finally, the top level function of our implemented algorithm is called dag-mgu. This function receives as input two terms t1 and t2 in prefix notation and computes its most general unifier (or failure) in the following way (see the supporting materials for the definitions): 1. It creates terms-dag as a local stobj, resizing the dag and stamp arrays according to the sizes of t1 and t2. 2. It stores both terms in the dag array, as directed acyclic graphs, building an initial dag unification problem. 3. Applies the function solve-upl-st to the initial unification problem. 4. If failure is detected, it returns (mv nil nil); otherwise, it returns (mv t σ), where σis the most general unifier (in prefix notation) obtained from the final indices substitution computed by solve-upl-st. It is worth pointing out that the input and output of this top level function are in prefix notation, although the main process of the algorithm is performed with the dag representation. The guard of the function dag-mgu is quite simple, and only checks that the two input terms are in prefix form. In contrast, the guards of the intermediate functions are quite complicated and expensive, including the well-formedness conditions and invariants described in the preceding sections. But since guards are verified these intermediate guards are never evaluated. The following three theorems establish the correctness of the implemented unification algorithm, showing that it computes a most general unifier of two given terms, whenever they are unifiable, and failure otherwise: