CLG, CCIA, University of Seville
We present the definition and formal verification in ACL2 of a unification algorithm acting on terms represented as directed acyclic graphs (dags). This implementation is done using single-threaded objects (stobjs) to store a dag representation of first-order terms.
ACL2 books used in this development:
These books are part of a library of results about the subsumption lattice of first-order terms, represented using lists, in the standard prefix form.
Described as a set of operators, we represent the transformation relation of Martelli and Montanari, specifying the behavior of a family of unification algorithms. In this case, this transformation relation acts on system of equations (unification problems) represented using the standard list/prefix representation of terms. We prove its main properties, concluding that some sequences of transformations lead to most general unifiers of unification problems, whenever they are solvable.
In this book we introduce the representation of first-order terms as directed acyclic graphs. These graphs are represented as lists of nodes and these nodes contain information about the symbol of the node and also indices pointing to its neighbor nodes. We also define a measure function that will allow us to do recursive definitions on acyclic graphs following a schema very similar to recursion on the structure of the terms they represent.
In this book, we define and verify a set of rules of transformation designed to obtain most general solutions of system of equations, when these systems of equations are represented as directed acyclic graphs (dags). The main result we prove establishes the relation between the transformation rules acting on the list/prefix representation and the transformation rules acting on the dag representation: every transformation step given at the "dag level" corresponds to a transformation step given at the "list/prefix level". Having proved this fundamental result, it is easy to conclude that some sequences of transformation rules acting on term dags lead to find the most general solution (whenever it is solvable) of the system represented by the initial dag. This is a key result to design a unification algorithm acting on term dags.
In this book, we define and verify a function that builds the directed acyclic graph corresponding to the unification of two given terms. We prove that the obtained graph is a directed acyclic graph representing the terms received as input. Surprisingly, it turns out to be a very hard proof effort.
Since we now have a function to build dags representing unification problems, and that we have proved that applying transformation rules to dags we can obtain most general unifiers, it is easy to implement a dag based unification algorithm. In this book we define and verify that algorithm.
So far, we have represented our graphs using lists, each of its elements representing a node. It is much more efficient to use a single-threaded object for that purpose. In this book we define a stobj called terms-dag, with one array field, each of its cells used to store a node. In this way, the space needed to represent a unification problem is constant and accesses and updates can be done in constant time.
Finally, it is now possible to define and verify an algorithm analogue to the one defined on dags using lists, but now using the terms-dag stobj to store the directed acyclic graph. This is what we do in this book, by simply translating the results of the book dag-unification-l.lisp.
The previous algorithm it is still exponential in time (although it is the most used in practice). With some modifications we can do it quadratic. For the moment we have it in program mode and therefore without verification. We also present some examples and its execution time (really fast!!!)