Algebraic Semantics for Higher-order Functional-Logic Programming

In this paper we give a semantics of higher-order functional-logic programming in the framework of typed universal algebra. The functional-logic language concerned here is an applicative term rewriting system in which there is no lambda abstraction mechanism. Therefore ordinary first-order narrowing can be used to solve higher-order query. The soundness and completeness of narrowing for both the initial and minimal applicative Herbrand model is shown. We discuss the requirements of "minimal" for applicative Herbrand model, which means that any elements in the domain must have denotations of some terms, is need to obtain the completeness of narrowing in the applicative case of functional-logic programming. 1. Introduction Semantics of first-order functional-logic programming has been deeply investigated. Two approaches are known for giving semantics. One approach is based on term rewriting. In this approach, a program of functional-logic languages is regarded as a conditional term rew..