[SOLVED] What does higher-order semantics give you in λProlog?

What does higher-order semantics give you in λProlog?

λProlog is a higher-order dialect of Prolog. On the other hand, HiLog is said to use higher-order syntax with first-order model theory. In other words, they both have higher-order syntax, but only λProlog has higher-order semantics.

What does higher-order semantics give you in λProlog (beyond what you already get with higher-order syntax alone)? What would be a simple example in λProlog that illustrates these gains?

Solution

Most likely, λProlog implements more than HiLog. HiLog seems to me what we nowadays more or less see in every Prolog system, some call/n and some library(lambda).

The call/n and library(lambda) can do a kind of beta-reduction. But in λProlog there is a rule AUGMENT and a rule GENERIC, not covered by beta-reduction. This enhances the underlying logic:

G, A |- B
------------ (AUGMENT)
G |- A -: B

G |- B(c)
------------- (GENERIC) c ∉ G
G |- ∀xB(x)

A typical example for the AUGMENT rule is hypothetical reasoning. This answers "what-if" questions. Some deductive databases, even implemented on top of ordinary Prolog can do that as well. Here a simple example:

grade(S) :-
   take(S, german),
   take(S, french).
grade(S) :-
   take(S, german),
   take(S, italian).

take(hans, french).

The above rules express when somebody can grade. And we have also some information about "hans". We can now ask hypothetical questions directly in the top-level, without modifying the fact database.

?- take(hans, german) -: grade(hans).
Yes
?- take(hans, italian) -: grade(hans).
No

I guess one could also make a case for higher order unification. The λProlog book contains some higher oder unification examples, that probably also don't work in HiLog.