Narrowing Approximations as an Optimization for Equational Logic Programs

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 paper, we formulate a narrowing-based equation solving calculus which makes use of a top-down abstract interpretation strategy to control the branching of the search tree. We define a refined, but still complete, equation solving procedure which allows us to reduce the branching factor. Our main idea consists of building an abstract narrower for equational theories and executing the set of equations to be solved in the approximated narrower. 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. Thus we define a strategy which computes such a set and uses the substitutions in it for cutting down the search space of the program without losing completeness. We also report on experimental results which demonstrate that our optimization can result in significant speed-ups in program execution. © Springer-Verlag Berlin Heidelberg 1993.