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.
|Software (msc 68Nxx), Logic programming (msc 68N17), Specification and verification (program logics, model checking, etc.) (msc 68Q60)|
|CWI. Probability, Networks and Algorithms [PNA]|
Bezem, M.A. (1999). Extensionality of simply typed logic programs. CWI. Probability, Networks and Algorithms [PNA]. CWI.