prolog - λProlog 拒绝假设的推理查询？

Question

我怀疑 λProlog 的主要实现 teyjus 可能有点废弃软件，但 λProlog 是一个迷人的 Prolog，它应该让你使用高阶逻辑、假设推理和其他东西，这就是为什么我试图用它。

文件“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.

文件“example.mod”：

module example.

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

take hans french.

但是，当我编译和加载它时，虽然它似乎可以工作，但假设的推理查询被拒绝：

[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

我期待在最后一个“是”。我究竟做错了什么？

Answer 1

当前版本的 Teyjus 不允许将查询中的含义直接输入到顶层。Gopalan Nadathur 和我的书（使用高阶逻辑编程）在附录中提到了这个问题和解决方法（见下面的摘录）。

A.4.2 与本书假设语言的偏差（第 287 页）

[...]

Teyjus 不允许在顶级目标中使用含义。当编译模型也扩展到这些目标时，这个特性可能会在将来发生变化，但就目前而言，这意味着某些示例（例如，在第 3.2 节中）不能直接使用该系统运行。请注意，仅在顶级目标中不允许使用含义：它们可以在出现在程序子句主体中的目标中自由使用。因此，可以通过首先构建一个合适的程序子句然后使用它来提出所需的查询来克服这个限制。例如，而不是提出查询

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

可以创建子句

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

然后使用查询

?- test X.

Answer 2

通过以下方式扩展“example.sig”：

type whatif language -> o.

通过以下方式扩展“example.mod”：

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

然后它起作用了：

看起来 λProlog 是惰性软件，我提出了一个问题#122。
还是有一些根本问题不起作用，
比如打字问题或编译器优化？

PS：我的生活很危险，从这里下载了 tjsim.exe 等：
http ://www.eecs.ucf.edu/~leavens/Windows/usr-local-bin/