Logic programming beyond Prolog

TL;DR

This paper introduces relational programming, a method that separates logical specifications, algorithms, and code to improve abstraction and correctness in logic programming beyond traditional Prolog.

Contribution

It presents a new relational programming approach that enhances abstraction and correctness by separating axioms, theorems, and code, extending logic programming capabilities.

Findings

Relational programming offers higher abstraction than pure Prolog.

It maintains model-theoretic and fixpoint semantics similar to Prolog.

It allows sorting of any data satisfying linear order axioms in C++.

Abstract

A logic program is an executable specification. For example, merge sort in pure Prolog is a logical formula, yet shows creditable performance on long linked lists. But such executable specifications are a compromise: the logic is distorted by algorithmic considerations, yet only indirectly executable via an abstract machine. This paper introduces relational programming, a method that solves the difficulty with logic programming by a separation of concerns. It requires three texts: (1) the axioms, a logical formula that specifies the problem and is not compromised by algorithmic considerations, (2) the theorem, a logical formula that expresses the idea of the algorithm and follows from the axioms, and (3) the code, a transcription of the theorem to a procedural language. Correctness of the code relies on the logical relationship of the theorem with the axioms and relies on an accurate transcription of the theorem to the procedural language. Sorting is an example where relational programming has the advantage of a higher degree of abstractness: the data to be sorted can be any data type in C++ (the procedural language we use in our examples) that satisfies the axioms of linear order, while the pure-Prolog version is limited to data structures in the form of linked cells. We show another advantage of relational programs: they have a model-theoretic and fixpoint semantics equivalent to each other and analogous to those of pure Prolog programs.