A Categorical Abstract Machine for Logic Programming

March 20, 2012

Emilio Gallego


A Categorical Abstract Machine for Logic Programming

Time:   11:00am
Location:   Meeting room 302 (Mountain View), level 3

We present an efficient declarative execution mechanism for Logic Programming. Our machine is based on the categorical version of the calculus of relations — allegory theory. In particular, we use tabular allegories, whose main property is that every relation is tabulated by a pair of functions. For an allegory R, the set of tabulations is a regular category called Map(R).

A suitable allegory for Logic Programming is generated from a regular completion of a Lawvere Category of a logic program. Lawvere Categories represent algebraic theories and in our setting they capture the signature of the program. The new notion of “Regular Lawvere Category” is a perfect candidate for the category of maps of a given allegory.

Our machine is fully based on relation composition. This single primitive encompasses unification, garbage collection, parameter passing, environment creation and destruction.

In this talk, we will quickly survey the categorical foundations and motivations for the work. After that, we will present the compilation procedure, machine specification, the correspondence of categorical structures with implementation concepts such as pointers, registers and instructions. Last, we will discuss some of the extensions to our computational model such as constraints, types, functions and monads.