Search code examples
prologlogic-programminglambda-prolog

λProlog rejecting hypothetical reasoning queries?

I suspect that teyjus, the main implementation of λProlog, might be a bit of abandonware, but λProlog is a fascinating Prolog that is supposed to let you use higher-order logic, hypothetical reasoning and other things, which is why I'm trying to use it.

File "example.sig":

sig example.

kind person, language type.

type hans person.
type german, french, italian language.

type grade person -> o.
type take person -> language -> o.

File "example.mod":

module example.

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

take hans french.

However, when I compile and load it, while it appears to work, hypothetical reasoning queries get rejected:

[example] ?- take X Y.

The answer substitution:
Y = french
X = hans

More solutions (y/n)? y

no (more) solutions

[example] ?- grade X.

no (more) solutions

[example] ?- (take hans german) => (grade hans).
(1,19) : Error : Symbol => is not permitted within terms

I was expecting a "yes" at the end there. What am I doing wrong?

Solution

  • Extend "example.sig" by:

    type whatif language -> o.

    Extend "example.mod" by:

    (whatif Q) :- ((take hans Q) => (grade hans)).

    And then it works:

    enter image description here

    Looks like λProlog is lazyware, I raised an issue #122.
    Or there are some fundamental problem that it doesn't work,
    like typing problems or compiler optimizations?

    P.S.: I was living dangerously, and downloaded tjsim.exe etc.. from here:
    http://www.eecs.ucf.edu/~leavens/Windows/usr-local-bin/