Indexed Categories and Bottom-Up Semantics of Logic Programs

Abstract. We propose a categorical framework which formalizes and extends the syntax, operational semantics and declarative model theory of a broad range of logic programming languages. A program is interpreted in an indexed category in such a way that the base category contains all the possible states which can occur during the execution of the program (such as global constraints or type information), while each fiber encodes the logic at each state. We define appropriate notions of categorical resolution and models, and we prove the related correctness and completeness properties. 1 Introduction One of the greatest benefits of logic programming is that it is based upon the notion of executable specifications. The text of a logic program is endowed with both an operational (algorithmic) interpretation and an independent mathematical meaning which agree each other in several ways. An operational interpretation is needed if we wish to specify programs which can be executed with some degree of efficiency, while a clear mathematical (declarative) meaning simplifies the work of the programmer, who can-to some extent- focus on "what to do " instead of "how". The problem is that operational expressiveness (i.e. the capability of directing the flow of execution of a program) tends to obscure declarative meaning. Research in logic programming strives to find a good balance between these opposite needs