Extensional Higher Order Prolog

One big issue in the logic programming vs functional programming debate is logic programming’s (or at least the original Prolog’s) restriction to first order logic. To functional programmers this constraint is intolerable; even the simplest Haskell programs are higher order (although this is often due to currying).

Can this be fixed? Yes, but you have to be careful.

Two higher order systems appeared a while ago – HiLog and λ-Prolog. Both are useful but they have the same flaw. They are intensional. They have (say) predicate variables, but these variables range not over predicates in the mathematical sense, namely arbitrary sets of ground terms. Instead they range over names of predicates, names that appear in the program (so that higher order clauses are context sensitive). In logic terminology, they are not extensional.

Intensionality / context sensitivity can cause a lot of problems. It interferes with modularity. For example, if you have two sets of clauses that logically appear to do the same thing, it is not necessarily safe to swap them in the context of a program. And adding clauses to a program might break it, because it might change the scope of predicate variables.

One symptom of these programs is that the languages don’t have a minimum model semantics. So what? So: it means clauses don’t have a logical reading. You can’t understand them as logic, and as I once raised eyebrows at a conference for saying,

Logic Programming – Logic = Programming

Fortunately, a while back I discovered a subset of extensional higher order Horn logic that works as logic programming and has a minimum model semantics. The key idea is to restrict what can appear on the left hand side.

To see the problem with unrestricted higher order extensional Horn logic, consider the following clauses

q(b) :- r(q).

What is the result of the query :- q(b). ?

At first sight, p and q are both true of a alone. They both denote the set {a}. They have the same extension, and should be interchangeable. Since the system is extensional, and r is true of p, r must be true of q. But then p and q are no longer extensionally equivalent, and there is no reason for r(q) to succeed. Thus q(b) fails, but then p and q are equivalent …

There are two solutions to this paradox. One is to make r(p) succeed, and r(q) fail, even though p and q have the same extension. This is what the intensional systems do.

The alternative, which I presented way back in 1991, is to forbid rules like r(p) which single out particular predicates for special treatment. It is too much to ask an implementation to identify other predicates as having the same extension as the one in the spotlight.

So I disallowed rules in which predicate constants (and other non ground expressions) appear in the head. I also disallowed rules in which a higher order variable is repeated in the head, because that implies an (uncomputable) equality test. (Here “higher” means >0).

The result is that the higher order variables are basically formal parameters, and the clause takes the form of a definition.

These definitions can be powerful. For example, suppose you want to check whether a list is in numerical order. In first order Prolog, it’s easy:

numordered([X,Y|T]) :- X<Y, numordered([Y|T]).

Fine, except suppose you have some lists of strings and you want to check if  they are alphabetically ordered. You have to write code for another predicate alfordered. Another three lines, identical except that X<Y is replaced by alf(X,Y). Then you have lists of lists that should be ordered (by subset) as if they represented sets. Another predicate, setordered. More cut and paste.

By now the functional programmers are laughing. They write one set of axioms, for a function with a binary relation argument.

Well, we can do the same in Definitional Higher order Prolog (DHP):

ordered([X,Y|T],R) :- R(X,Y), ordered([Y|T],R).

Then we use ordered with appropriate arguments: ordered([5,6,…],<), ordered([‘dick’,’tom’,…],alf) or ordered([[5,3],[3,4,5],…],sub).

Another example is the join operation (on two binary predicates, yielding a third, their join).

join(P,Q)(X,Y) :- P(X,Z),Q(Z,Y).

DHP has been implemented (with some syntactic variations) as part of the system HOPES developed by Angelos Charalambidis in his PhD dissertation at the University of Athens, Greece. Currently Angelos and his group at the Demokritos Institute (again, Athens) are working on adding negation.

And now its time to have a laugh at the functional programmers expense. In their grim regimented world, function can be used in only one way. In logic programming no parameters have fixed roles. For example, we can define a relation r on a, b, c and d:

r(a,b). r(a,c). r(b,d). r(c,d).

and then ask the query


and get all the lists that are in order according to L. Starting with the empty list and proceeding through singletons we eventually get [a,b,d] and [a,c,d].

Even more impressive, we can query ordered([a,b,c,d],R) and get the equivalent  of


What does this mean? It’s not the only value for R that does the job, you can add any tuples you want to this set and still get an order that satisfies the query. This is true even if the tuples contain atoms other than a, b, c, and d. So there are in fact infinitely many solutions.

The reason the interpreter displays the one given above is because it is minimal. No subset of it works. In general, there may be more than one minimal solution, so they are presented sequentially, but in an unpredictable order.

The intentional systems can’t do this because they don’t consider R as ranging over all predicates, just over the ones named in the system. So if you haven’t already defined a predicate that does the job, you’re out of luck.

(Incidentally my original proposal didn’t allow this. I thought it was complex and unusual. Boy was I wrong. My successors corrected my mistake.)

As a slightly more interesting example, suppose we have a collection of facts about some musicians, say singer(pam) or drummer(rajiv). We want to put together a band, with the constraint that a band must have a singer, a keyboardist, and either a bass or a drummer. Being a band is a second order predicate, a predicate of predicates. We can axiomatic it with

band(B) :- B(X), singer(X), B(Y), keyboard(Y), B(Z), rhythm(Z).
rhythm(Z) :- bass(Z).
rhythm(Z) :- drum(Z)

Then if we present the query band(B) the implementation will start producing lasts of band. And not many, because the bands presented will be minimal.

This feature really comes into its own when combined with negation. Instead of a band, think of a development teams. We could have all sorts of complex criteria, say that Keisha and Andre can’t both be on the team, that we need either a Javascript or PHP expert but nor both, that they have a language in common, and so on. The interpreter will produce a list of minimal teams.

(HOPES is available on github. Ironically, the implementation is written in Haskell.)


About Bill Wadge

I am a Professor in Computer Science at UVic.
This entry was posted in research. Bookmark the permalink.

2 Responses to Extensional Higher Order Prolog

  1. Ulrich Neumerkel says:

    Please note that current Prolog systems support higher-order programming by call/N which was first proposed in 1984 by Richard O’Keefe (http://www.complang.tuwien.ac.at/ulrich/iso-prolog/#plstd) join is now defined as: join(P,Q,X,Y) :- call(P,X,Z),call(Q,Z,Y).

    • Sure Prolog has call and Lisp and Javascript have eval as well – but these are simply and escape-hatch to to allow meta-programming, where you can roll your own higher-order programming paradigms, rather than first-class support of a particular higher-order programming model.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s