Algebra of Binary Relations

Appeared in Volume 9/4, November 1996

dwyer@cs.adelaide.edu.au
Barry Dwyer
11th June 1996

Does any reader of comp.lang.prolog have an interest in programming languages based on the algebra of binary relations? Briefly, the advantages are a combination of the so-called transparancy of functional languages, with the backtracking capability of Prolog, plus a programming style that resembles specification languages such as Z. For more details, see my home page:

http://www.cs.adelaide.edu.au/~dwyer

fjh@mundook.cs.mu.oz.au
Fergus Henderson
11th June 1996

How does this differ from a unified equational (combined logic/functional) language that supports higher-order programming, such as say Lambda-Prolog or Mercury?

I will selectively quote parts of your description of Libra accessible from your URL, and comment upon them.

You write:
On the other hand, Prolog has its own difficulties. Although a subset of Prolog can be understood in terms of predicate calculus, most useful Prolog programs need to use extra-logical predicates, which can only be understood with reference to a specific model of program execution.

That's true, but Prolog is fairly old now. More modern logic programming languages, such as Goedel and Mercury, address most/all of these problems.

You continue:
10.1 Type-Checking and Inapplicability

The first lesson - which came as a surprise to the author - is that although the relational programs developed as examples are quite short, they were surprisingly tricky to get right. Some of the difficulties arose because the interpreter was under development, some were due to the author's unfamiliarity with relational programming, and some due to the design of Libra itself. The main problem in the design is the notion of inapplicability. If a relation is presented with an argument to which it does not apply, it simply produces no result. It is fundamental to relational programming that this should occur, but it means that if a programming error leads to the wrong type of argument being passed, then the program as a whole typically produces no result. It is not easy to deduce exactly where the problem lies from an empty output.

There would seem to be several solutions to this problem. They all involve some kind of type-checking.
...
The author's personal view is that static type-checking is unduly restrictive. Although it can detect many programming errors, it is just one of many checks that could be made.

Are you aware of Lee Naish's paper "Types and the Intended Meaning of Logic Programs" in Types in Logic Programming (edited by Frank Pfenning)? He illustrates how types are necessary if the standard implementations of many simple predicates such as append/3 are to correctly implement their intended semantics. This work shows, in my opinion, that types are an integral part of the semantics.