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

Question

λ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?

Answer 1

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.

See also:

An Overview of λProlog
Miller & Nadathur - 1988
https://www.researchgate.net/publication/220986335

A Logic for Hypothetical Reasoning
Bonner - 1988
http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.1451

Answer 2

That's a hard nut.

The two ideas for getting Prolog to "do more" taken by HiLog and Lambda-Prolog are very different, so a program in one wouldn't necessarily make sense in the other.

Not also that Lambda-Prolog is not really a "dialect", it is a different "Prolog" in the same way that ASP is a different "Prolog".

Now, finding programs that differ in semantics means first finding programs that are comparable, so "intent to do the same thing" (barring "unimportant syntactic details") from the programmer's perspective, so one would have to restrict oneself to a common subset of both languages.

On the other hand, even though the proof procedure of Lamba Prolog is not (or better, doesn't map to) "resolution refutation", the whole idea is to capture the intuition of a logic deduction. This should also be the case in HiLog.

"Fundamentally different" thus means "fundamentally breaking the expectation of the programmer's intuition" in one or the other, possibly in both, cases.

It's a good occasion to re-read the papers I guess.