On the Completeness of Narrowing as the Operational Semantics of Functional Logic Programming

This paper is a continuation of [10]. It presents soundness and completeness results for a higher-order (HO) functional logic language which has a domain-based declarative semantics and uses conditional narrowing (for applicative, constructor based rewriting systems) as operational semantics. HO-unification is avoided by for bidding λ-abstractions in the language. However, narrowing must include a mechanism for binding HO logic variables to simple functional patterns built by partial application. A deeper investigation of lazy strategiees and infinite narrowing derivations is foreseen.