Disequalities May Help to Narrow

A constructor-based rewriting logic (CRWL) has been recently proposed as an appropriate basis for functional logic programming. In this paper we extend such framework, to cope with disequality constraints, which are a useful and expressive resource from the point of view of programming. As an important application of the enhanced framework, we show how to express within it a sophisticated narrowing strategy which is widely accepted to be appropriate for lazy functional logic languages, but which previously suffered the lack of a formal justification in the original framework. This is achieved by means of a simple, incremental program transformation which can be proved to preserve the semantics of the original program