Narrowing and unification in functional programming —An evaluation mechanism for absolute set abstraction

The expressive power of logic programming may be achieved within a functional programming framework by extending the functional language with the ability to evaluate absolute set abstractions. By absolute set abstraction, logical variables are introduced into functional languages as first class objects. Their set-valued interpretations are implicitly defined by the constraining equations. Narrowing and unification can be used to solve these constraining equations to produce the satisfying instantiations of the logic variables. In this paper, we study an execution mechanism for evaluating absolute set abstraction in a first order (non-strict) functional programming setting. First, we investigate the semantics of absolute set abstraction. It is shown that absolute set abstraction is no more than a setvalued expression involving the evaluation of function inversion. Functional equality is defined coinciding with the semantics of the continuous and strict equality function in functional programming. This new equality means that the well known techniques for equation solving can be adopted as a proper mechanism for solving the constraining equations which are the key to the evaluation of absolute set abstraction. The main result of this paper lies in the study of a particular narrowing strategy, called lazy pattern driven narrowing, which is proved to be complete and optimal for evaluating absolute set abstraction in the sense that a complete set of minimal solutions of the constraining equations can be generated by a semantic unification procedure based on this narrowing strategy. This indicates that a mechanism for equation solving can be developed within a functional programming context, producing a more expressive language.