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.