Higher-Order Functional-Logic Programming: A Systematic Development

We develop an effective model for higher-order functional-logic programming by refining higher-order narrowing calculi. The refinements reduce the high degree of non-determinism in narrowing calculi, utilizing properties of functional(-logic) programs. These include convergent and left-linear rewrite rules. All refinements can be combined to a narrowing strategy which generalizes call-by-need as in functional programming. Furthermore, we consider conditional rewrite rules which are often convenient for programming applications. 1. Introduction We present a systematic development of a calculus which integrates higher-order functional and logic programming, based on narrowing. Narrowing is a general method for solving equations modulo a set of rewrite rules. Functional-logic languages with a sound and complete operational semantics are mainly based on narrowing. For a survey on the topic we refer to [9]. In our higher-order equational logic we use a rewrite relation due to Nipkow [18],..