λProlog rejecting hypothetical reasoning queries?

Question

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?

Answer 1

Extend "example.sig" by:

type whatif language -> o.

Extend "example.mod" by:

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

And then it works:

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/

Answer 2

The current version of Teyjus does not allow implications in queries to be entered directly to the top-level. The book by Gopalan Nadathur and me (Programming with Higher-Order Logic) mentioned this problem and a workaround in the Appendix (see excerpt below).

A.4.2 Deviations from the language assumed in this book (page 287)

[...]

Teyjus does not permit implications to be used in top-level goals. This is a characteristic that may change in the future when the compilation model is extended also to these goals but, for now, it means that some of the examples presented, eg, in Section 3.2, cannot be run directly using this system. Notice that implications are disallowed only in top-level goals: they can be used freely in goals that appear in the body of program clauses. Thus, this limitation can be overcome by first building a suitable program clause and then using it to pose the desired query. For example, instead of posing the query

?- p a => p b => p X.

one can create the clause

test X :- p a => p b => p X.

and then use the query

?- test X.