如何使用 Prolog 代码检查确定性

问题描述

我们希望通过自动确定性来检测我们的 Prolog 代码 检查。因此,本着 Ciao 断言的精神,我们将宣布 :- pred <functor>/<arity> is <determinism>,其中 <determinism> 可以取值:

价值 说明
检测 只有一个解决方案,那么该模式是确定性的
半人半 要么没有解,要么只有一个解,那么那个模式是半确定的
至少有一个解决方案,但可能有更多,那么这种模式就是多解决方
nondet 有零个或多个解,那么该模式是不确定的

https://www.mercurylang.org/information/doc-latest/mercury_ref/Determinism-categories.html

这是一个预期行为示例,以这个 Prolog 文本输入为例:

:- pred r/1 is multi.
r(b).
r(c).
r(c).

然后这个查询输出

?- r(a).
Error: UnkNown pattern: assertion_failure(multi)
?- r(b).
Yes
?- r(c).
Yes ;
Yes

由于大多数 Prolog 系统都有术语扩展和目标扩展,因此在编译时通过某些 Prolog 代码本身注入此类断言似乎是一种合适的语言。人们将如何着手并实施这样的工具?

解决方法

我们可以通过它们需要检测的错误情况来分析确定性类别。有两种不同的错误情况跨越所有确定性类别。错误情况指的是使用给定谓词指示符调用的目标:

价值 有限失败 多种解决方案
检测 禁止 禁止
半人半 允许 禁止
禁止 允许
nondet 允许 允许

对于确定性类别“nondet”,无需执行任何操作。对于其他确定性类别,我们安装了一个包装器。这个包装器将拥有给定的谓词指示符并调用一个辅助谓词来收集给定谓词指示符的规则。对于有限失效,我们在文献中找到了这个建议:

enter image description here

使用注解调试 Prolog
M. Kula - 2000 年出版
https://pdfs.semanticscholar.org/0d14/e5c3d88cf280ca5b37fae15b58fde9986544.pdf

但我们只是简单地使用软剪辑:

(Call *-> true; assertion_failure)

对于多个解决方案,我们使用 call_nth/2,同时在许多 Prolog 系统中也可以找到它:

call_nth(Call,Count),(Count > 1 -> assertion_failure; true)

最后给出了带有相应重写代码的链接。最后还给出了示例集合。我们可以再展示两个例子。以这个 Prolog 文本输入为例:

:- pred p/1 is semidet.
p(b).
p(c).
p(c).

:- pred q/1 is det.
q(b).
q(c).
q(c).

包装器产生以下结果:

?- p(a).
No
?- p(b).
Yes
?- p(c).
Yes ;
Error: Unknown pattern: assertion_failure(semidet)

?- q(a).
Error: Unknown pattern: assertion_failure(det)
    q/1
?- q(b).
Yes
?- q(c).
Yes ;
Error: Unknown pattern: assertion_failure(det)

开源:

断言包装
https://gist.github.com/jburse/d5e95099e3d83f6f09b2cb2a91da719c#file-assertion-pl

断言演示
https://gist.github.com/jburse/d5e95099e3d83f6f09b2cb2a91da719c#file-demo-pl