Algebraic Semantics for Higher-Order Functional-Logic Programming

Makoto Hamana


In this paper we give semantics of higher-order functional-logic programming in the framework of typed universal algebra. The functional-logic language concerned here is a form of so-called applicative term rewriting system that does not have lambda abstraction. Therefore ordinal first-order narrowing can be used to solve higher-order query. Initial model of a functional-logic program in a class of all algebraic models is obtained by a quotient of term algebra. Moreover another model, called ``minimal applicative Herbrand model'', is constructed by fixed point techniques. The semantics domain of minimal applicative Herbrand model forms a cpo and contains partially defined terms, infinite terms and continuous functions on these terms. The soundness and completeness of narrowing for both initial and minimal applicative Herbrand model is shown. We discuss the requirements of ``minimal'' for applicative Herbrand model, which means any elements in the domain must be denotation of some terms, is need to obtain completeness of narrowing in applicative case of functional-logic programming.

Last modified: Tue Apr 29 05:45:41 JST 1997