1

我正在尝试研究在无类型语言上使用自定义类型推理语言的项目的可行性。（语言本身并不重要，但它恰好是 PHP）。我的第一个想法是对此运行类型统一。我在 Haskell 中编写了一些程序，所以我知道从最终用户的角度来看类型统一是如何工作的，但我从未深入研究过算法的细节。

此时，我可以解析一个 PHP 代码文件，构建一组相应的规则，并希望开始针对这些规则运行统一算法。与其重新发明轮子，我想我会使用现有的统一算法，而 AFIAK，Prolog 是目前最强大的统一算法之一。

我现在已经到了这样的程度，如果我传入一个可验证的正确输入，Prolog 就会返回“true”。如果我传入不正确的内容，它会返回“错误”。现在我在那种情况下真正想要的是得到一条错误消息，指出为什么类型没有统一。如果我在 SWI-Prolog 中打开“跟踪”模式，我或多或少会得到我想要的东西，逐步解释为什么类型没有统一。我的核心问题是，是否可以通过编程方式获取这些信息？如果需要的话，我愿意编写一个 C 扩展并直接链接到 Prolog 编译器。此外，我与 SWI-Prolog 没有任何联系，它只是我在 google 上找到的第一个。

另外，作为一个完整的问题，有没有人知道序言中的任何好的教程，无论是网络格式还是作为一本真正的书？

4

1 回答 1

2

我的感觉是，通过跟踪，您不会获得统一失败的详细信息，但您会获得目标失败的信息。

如果后面的信息是您想要的，您可以自己执行此操作，因为您可以检测您的代码。只需替换每个目标

 .. A ..

通过以下代码：

 .. in(A), A, out(A) ..

具有以下定义：

 in(A) :- write('call '), write(A), nl.
 in(A) :- write('fail '), write(A), nl, fail.

 out(A) :- write('exit '), write(A), nl.
 out(A) :- write('redo '), write(A), nl, fail.

当然，您可以将 write/1 和 nl/0 语句替换为适合您的语句。这是一个例子。首先是检测的 Prolog 文本：

?- [user].
mem(X,[X|_]).
mem(X,[_|Y]) :- in(mem(X,Y)), mem(X,Y), out(mem(X,Y)).
^D

现在检测查询：

?- in(mem(X,[1,2])), mem(X,[1,2]), out(mem(X,[1,2])).
call mem(_G1479,[1,2])
exit mem(1,[1,2])
X = 1 ;
redo mem(1,[1,2])
call mem(_G1479,[2])
exit mem(2,[2])
exit mem(2,[1,2])
X = 2 ;
redo mem(2,[1,2])
redo mem(2,[2])
call mem(_G1479,[])
fail mem(_G1479,[])
fail mem(_G1479,[2])
fail mem(_G1479,[1,2])
false.

再见

于 2013-04-01T07:09:18.327 回答