We develop an algebraic framework, Logic Programming Doctrines, for
the syntax, proof theory, operational semantics and model theory of
Horn Clause logic programming based on indexed premonoidal
categories. Our aim is to provide a uniform framework for logic
programming and its extensions capable of incorporating constraints,
abstract data types, features imported from other programming language
paradigms and a mathematical description of the state space in a
declarative manner. We define a new way to embed information about
data into logic programming derivations by building a sketch-like
description of data structures directly into an indexed category of
proofs. We give an algebraic axiomatization of bottom-up semantics in
this general setting, describing categorical models as fixed points of
a continuous operator.
Keywords: Categorical logic; Indexed categories; Logic programming;
Abstract data types; Constraint logic programming