We set up a framework for the study of extensionality in the context of higher-order logic programming. For simply typed logic programs we propose a novel declarative semantics, consisting of a model class with a semi-computable initial model, and a notion of extensionality. We show that the initial model of a simply typed logic program, in case the program is extensional, collapses into a simple, set-theoretic representation. Given the undecidability of extensionality in general, we develop a decidable, syntactic criterion which is sufficient for extensionality. Some typical examples of higher-order logic programs are shown to be extensional.

Software (msc 68Nxx), Logic programming (msc 68N17), Specification and verification (program logics, model checking, etc.) (msc 68Q60)
CWI
CWI. Probability, Networks and Algorithms [PNA]

Bezem, M.A. (1999). Extensionality of simply typed logic programs. CWI. Probability, Networks and Algorithms [PNA]. CWI.