1

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

MWB
  • 11,740
  • 6
  • 46
  • 91
  • Does HiLog have a type system? Check this new question https://stackoverflow.com/questions/65275015/is-there-a-%CE%BBprolog-that-wouldnt-need-a-type-system –  Dec 13 '20 at 11:26

2 Answers2

4

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

  • is `-:` a typo? BTW I rephrased the question to make it clearer. I'm asking for *a valid λProlog* example that illustrates the gains from higher-order semantics. – MWB Dec 05 '20 at 22:10
  • I converted your example into actual λProlog (teyjus). It compiles and loads. However, when I issue the queries, I get `Error : Symbol :- is not permitted within terms`. Same for `=>`. And `==>` is undefined. – MWB Dec 06 '20 at 06:18
  • `Error : Symbol => is not permitted within terms`, as I mentioned. It's not allowed in a query, even though it's allowed in modules. Feel free the roll back or edit as you please. It's your answer. I thought my edit was an improvement. – MWB Dec 06 '20 at 12:34
  • Yes. They may have changed the language, or I'm using it wrong somehow (It seems to work for other stuff though) – MWB Dec 06 '20 at 12:39
  • `Some deductive databases, even implemented on top of ordinary Prolog can do that as well.` Did you have any particular ones in mind? – MWB Dec 06 '20 at 20:46
  • Datalog Educational System http://des.sourceforge.net/ , See "Hypothetical reasoning" –  Dec 06 '20 at 20:49
  • Datalog is much more limited than Prolog though, as I understand it: no functions/structs, so not Turing-complete. – MWB Dec 06 '20 at 20:57
  • If you don't mind that A is automatically universal quantified in (A -: B), you could also try: http://www.jekejeke.ch/idatab/doclet/prod/en/docs/15_min/10_docu/02_reference/04_examples/01_bonner.html You could define (A -: B) as assumez(A, B), it will automatically do a retrire/1 after B succeeded. It doesn't have any Datalog restriction. Its also possible to make an (A :- B) where the variables communicate, but I didn't show that. The example would be (p(X) -: p(3)) gives X = 3. –  Dec 06 '20 at 21:30
  • But its not a complete Lambda-Prolog solution, a few pieces are currently missing. –  Dec 06 '20 at 21:49
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.

David Tonhofer
  • 14,559
  • 5
  • 55
  • 51
  • I rephrased the question to make it clearer. I'm asking for *a valid λProlog* example that illustrates the gains from higher-order semantics. – MWB Dec 05 '20 at 22:10