Combining lazy narrowing and simplification

Abstract. Languages that integrate functional and logic programming styles with a complete operational semantics are based on narrowing. In order to avoid useless computations and to deal with infinite data structures, lazy narrowing strategies have been proposed in the past. This paper presents an important improvement of lazy narrowing by incorporating deterministic simplification steps into lazy narrowing derivations. These simplification steps reduce the search space so that in some cases infinite search spaces are reduced to finite ones. We show that the completeness of lazy narrowing is not destroyed by the simplification process and demonstrate the improved operational behavior by means of several examples. 1 Introduction In recent years, a lot of proposals have been made to amalgamate functional and logic programming languages [19]. Functional logic languages with a sound and complete operational semantics are based on narrowing, a combination of the reduction principle of functional languages and the resolution principle of logic languages. Narrowing, originally introduced in automated theorem proving [34], is used to solve equations by finding appropriate values for variables occurring in arguments of functions. This is done by unifying (rather than matching) an input term with the left-hand side of some rule and then replacing the instantiated input term by the instantiated right-hand side of the rule. Example 1. Consider the following rules defining the addition of two natural numbers which are represented by terms built from 0 and s