Algebra of Logic Programming

A declarative programming language has two kinds of semantics. The tract helps in reasoning about speci cations and correctness, while an operational semantics determines the manner of program exeA 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- rst strategy of Prolog. An alternative strategy is breadth- rst search, which shares many of the same laws. Both strategies are shown to be special cases of the most general strategy, that for tree searching. The three strategies are de ned 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.

• Type: Conference
• Year: 1999
• Where: ICLP
• Authors: Silvija Seres, J. Michael Spivey, C. A. R. Hoare
• Keywords: Algebraic Semantics, Automated Reasoning, Declarative Programming Language, ExeA Correct Program, ICLP 1999