Extensionality of simply typed logic programs

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.