Horn Clause Programs with Polymorphic Types: Semantics and Resolution

by Michael Hanus

Proc. of the International Conference on Theory and Practice of Software Development (TAPSOFT'89), Springer LNCS 352, pp. 225-240, 1989
© Springer-Verlag
Revised and extended version

This paper presents a Horn clause logic where functions and predicates are declared with polymorphic types. Types are parameterized with type variables. This leads to an ML-like polymorphic type system. A type declaration of a function or predicate restricts the possible use of this function or predicate so that only certain terms are allowed to be arguments for this function or predicate. The semantic models for polymorphic Horn clause programs are defined and a resolution method for this kind of logic programs is given. It will be shown that several optimizations in the resolution method are possible for specific kinds of programs. Moreover, it is shown that higher-order programming techniques can be applied in our framework.

DVI (86 KB) Postscript (260 KB) BibTeX-Entry