Extensional Higher Order Prolog

I've just published a draft paper on an entirely different approach to the same problem: instead of creating a higher-order Prolog, we've discovered a functional (and so higher-order) analogue of Datalog, a more limited language (http://www.rntz.net/files/datafun.pdf, on github at https://www.github.com/rntz/datafun)

This idea of a higher-order Prolog is very interesting! But it's not clear to me how it can be truly extensional without further limiting the language. For there is another reason why Prolog is not extensional: non-termination. As a simple example, consider this program:

    q(X) :- q(X).
    q(adam).
    p(adam).

`p` and `q` are logically equivalent (the line `q(X) :- q(X).` is a no-op; of course a predicate implies itself). But in Prolog, `q` is a useless, nonterminating predicate. This problem is not a simple quirk: provability in even first-order Horn logic is undecidable if you augment it with compound terms & unification (as Prolog does), so there is no general algorithm for deciding Prolog queries.

It looks like extensional higher-order prolog should have the same problem. The article doesn't address it, so I'll go read the papers.

EDIT: The relevant research papers on Higher-Order Prolog, if anybody is interested: http://arxiv.org/abs/1106.3457 "Extensional Higher-Order Logic Programming"; http://arxiv.org/abs/1405.3792 in which they extend it to negation; https://github.com/acharal/hopes the implementation's github repo

Good to see Prolog getting a mention!