April 28, 2009
Emilio Gallego
We present a new algebraic semantics for constraint logic programming based on Freyd’s allegories. Our objectives are twofold:
- To build an executable algebraic model for CLP, in the spirit of other algebraic abstract machines.
- To apply existing improvements in categorical semantics to CLP languages.
Starting with Asperti and Martini in 1989, several algebraic models for logic programming have been proposed in the literature. Most of these proposals are based on some form of indexed monoidal categories, already presented at Theory Lunch by James Lipton.
A different proposal using distributive relational algebras was done by Broome and Lipton. The keystone is to interpret predicates as a co-reflexive binary relations. Generalization of this approach to a categorical setting allows us to forget about some of the structure present in the IMC methods, concretely, the indexation functor and the monoidal structure are no longer needed.
In order to build a tabular additive allegory suitable for logic programming, we start with a category and require its HomSets to be equipped with intersection, union, and dual, thus each HomSet becomes a complete lattice. The regular category built from the free Lawvere theory of theprogram’s signature becomes an ideal candidate. The translation from logic programs to co-reflexive relations is as follows: predicates are arrows and ∧ is interpreted as arrow composition. This similarity with categorical semantics of other paradigms (think of functional programming) opens up the door to exploring some new constructions over logic programs. Outline of the talk:
- -Introduction and basic definitions.
- -A Categorical Abstract Machine.
- -Advanced examples: monads, types.