Algebra of Logic Programming

Silvija Seres, Michael Spivey and Tony Hoare:

A declarative programming language has two kinds of semantics. The more abstract helps in reasoning about specifications and correctness, while an operational semantics determines the manner of program execution. A correct program should reconcile its abstract meaning with its concrete interpretation.

To help in this, we present a kind of algebraic semantics for logic programming. It lists only those laws that are equally valid for predicate calculus and for the standard depth-first strategy of Prolog. An alternative strategy is breadth-first search, which shares many of the same laws. Both strategies are shown to be special cases of the most general strategy, that for free searching. The three strategies are defined in the lazy functional language Haskell, so that each law can be proved by standard algebraic reasoning. The laws are an enrichment of the familiar categorical concept of a monad, and the links between such monads are explored.