Narrowing Approximations as an Optimization for Equational Logic
Programs
Author
María Alpuente, Moreno Falaschi, María José Ramis and
Germán Vidal
Abstract
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.
Keywords
Abstract interpretation,
equational logic programming, term rewriting systems, universal
unification.