hopes

And the scary thing is that one can do even better: https://billwadge.wordpress.com/2016/01/18/extensional-highe... https://github.com/acharal/hopes

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: prova