University of Cambridge

Logic
&
Semantics

Unifying Theories for Logic Programming

By Tony Hoare (26th November 1999)

A theory of programming is intended to support the practice of programming by relating each program to the specification of what it is intended to achieve. An unifying theory is one that is applicable to a general paradigm of computing, and classifies many particular programming languages as correct instances of the paradigm. The logic programming paradigm is characterised by producing a collection of answers for each problem, allowing the later parts of the program to select between them. A specification is therefore just a predicate describing, the size, content, and other properties of the set of options offered. Offer sets may be combined by intersection or union, which are symmetrically defined to permit parallel implementation. Equally simple definitions can be given of features like negation and the cut.

A common feature of many logic and constraint languages is that they enumerate the solutions of simultaneous equations in some mathematical space. Particular languages differ in the choice of space, in their solution method, and in their representation of the set of solutions offered. For example, Prolog solves equations in a free algebra, and presents the solutions as a sequence. Such a particular language is related to the general paradigm by the general technique of data abstraction.

To prove total correctness of a program, a specification language must be able to describe all the ways that a program can go wrong. In logic programming, these include finite and infinite failure. Prolog also allows infinite success - producing an infinite sequence of answers. This requires an asymmetric version of union and intersection, which is necessarily more complicated. Nevertheless, the operators often enjoy surprisingly elegant algebraic properties, which aid both programmer comprehension and mechanical optimisation. Some of these laws are proved directly from the definitions, and are applicable to specifications and designs as well as programs. Other laws have to be postulated as healthiness conditions, which are proved to be preserved by all the operators of the programming language. Because the laws are shared by different languages, they help to classify them, and thereby contribute to the unification of their theories.

LS Home page or Talks in 1999/2000