Universal Quantification in Categorical Logic Programming

As the subject of logic programming has grown, demand for more expressive power and efficiency has led language designers to import constructs from other programming paradigms. Given the substantial gap between semantic methods in the functional, imperative and declarative programming communities, it is hard to evaluate the effectiveness of proposals to add imported features to logic programming, unless there is an agreed-upon common framework. A categorical foundation for logic programming is an essential tool in this endeavour. In this work we show how to handle universal quantification in categorical logic programming via indexed categories. We define categorical syntax via tau-categories, and resolution over such categories for hereditarily Harrop programs and goals, and give a categorical operational semantics with respect to which resolution is shown sound and complete. Our model theory is a categorical generalization of the Kowalski-Van Emden fixed point semantics based on indexing over programs in order to capture program augmentation and state change. This framework is sufficiently broad to handle constraint logic programming and also a treatment of abstract datatypes.