A categorical model for logic programs: Indexed monoidal categories

Abstract

We propose a simple notion of model for Logic Programs based on indexed monoidal categories. On the one hand our proposal is consistent with well-known techniques for providing a categorical semantics for logical systems. On the other hand, it allows us to keep the effectiveness of the Horn Clause Logic fragment of first order logic. This is shown by providing an effective construction of the initial model of a program, obtained through the application of a general methodology aimed at defining a categorical semantics for structured transition systems. Thus the declarative view (as logical theory) and the operational view (as structured transition system) of a logic program are reconciled in a highly formal framework, which provides interesting hints to possible generalizations of the logic programming paradigm.