Technical Report DSIC-II 32/93, DSIC, Technical University of Valencia, 1993
Solving equations in equational theories is a relevant programming paradigm which integrates logic and equational programming into one unified framework. Efficient methods based on narrowing strategies to solve systems of equations have been devised. In this work, we define an abstract narrower for equational theories which can be used to obtain a finite description of the set of solutions. We define a generic technique of loop detection to ensure termination of our method. We prove that the set of answers computed by the abstract narrower has the property that each concrete solution of the set of equations is an instance of one of the substitutions in the answer set. We also introduce a parallel composition operator which can be used to perform computations and analysis incrementally in a Constraint Equational setting and show that the test of satisfiability in this setting can be done in parallel. Then, we define several applications of the framework. On one hand, we show a refined, but still complete, equation solving procedure which allows us to reduce the branching factor. On the other hand, we show how groundness and sharing information can be derived from the partial solutions of the abstract narrower. Finally, we give some benchmarks which show the usefulness of the method.
Keywords: Abstract interpretation, equational logic programming, term rewriting systems, universal unification, semantic analysis, compositionality, concurrency and parallelism, constraints
Available: PDF BibTeX-Entry