Prolog中单面统一的Quine算法

Question

SWI的新版本8.3.19在新的Picat样式规则中引入了单边统一。这可能是对任何Prolog系统的欢迎添加。我在想我们能不能重写奎因算法

Quine算法的Prolog实现

https://\stackoverflow.com/q/63505466/502187

皮卡特风格的规则和这是否可行？如果是的话，如果Quine算法的编写变得更简单，那么simpler可能通过这个添加对社区产生了很大的帮助。

对这个挑战有什么看法吗？SWI-Prolog 8.3.19已经可以从devel获得。

Answer 1

通常的统一--也称双面统一--与内建(=)/2密切相关，而模式匹配(也称为单边非化)与内建(==)/2之间有类似的关系。

=(X,X) :- true.
==(X,X) => true.

如果我们查看Quine的代码，即从here获取的代码，我们就会发现很多(==)/2使用的代码。模式匹配可以直接完成的任务：

simp(A, A) :- var(A), !.
simp(A+B, B) :- A == 0, !.
simp(A+B, A) :- B == 0, !.
Etc..

所以我们试了一试，把所有的规则转换成模式匹配。最初的var/1保护不再需要，(==)/2也不再需要了。但是我们观察到，我们需要更多的(=)/2来返回函数值：

simp(0+B, X) => X = B.
simp(A+0, X) => X = A.
Etc..

我们做了一个小小的基准测试，验证了来自原则的193个命题逻辑测试用例。我们测试了正常统一和模式匹配。我们还与尚未编译的模式匹配变体进行了比较，这种扩展使用了subsumes/2：

首先，通过subsumes/2进行扩展，它不编译模式匹配：

/* Jekejeke Prolog 1.5.0 */
/* normal unification */
?- time((between(1,380,_), test, fail; true)).
% Up 996 ms, GC 6 ms, Threads 984 ms (Current 02/14/21 11:30:28)
Yes

/* pattern matching */
?- time((between(1,380,_), test, fail; true)).
% Up 3,525 ms, GC 24 ms, Threads 3,500 ms (Current 02/14/21 11:42:50)
Yes

现在，SWI提供了新的编译模式匹配：

/* SWI-Prolog 8.3.19 */
/* normal unification */
?- time((between(1,380,_), test, fail; true)).
% 4,940,000 inferences, 0.547 CPU in 0.534 seconds (102% CPU, 9033143 Lips)
true.

/* pattern matching */
?- time((between(1,380,_), test, fail; true)).
% 4,940,000 inferences, 0.531 CPU in 0.531 seconds (100% CPU, 9298824 Lips)
true.

我以为编译后的方法会显示出更大的震动，而不仅仅是保持正常统一的表现？不过，这是一个良好的开端。

开放来源：

Boole方法从1847年开始，Prolog风格的

https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole-pl

Boole 1847年的方法，Picat

https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole2-pl

Picat展开

https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-picat-pl

193个命题逻辑测试用例来自

https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-principia-pl

Answer 2

另一种方法是使用较低层次的单面统一，而不是使用基于包含/2的单面统一。SWI 8.3.19已经实现了这一点，但是我的系统的另一个答案没有显示出来。

我们是否发现其他Prolog系统也提供了较低级别实现的单边统一？结果是肯定的，例如，ECLiPSe Prolog：

4.6匹配

在ECLiPSe中，您可以编写使用匹配(或单向统一)代替头统一的子句。这样的从句是用?-函子写的，而不是:-。匹配具有一个属性，即调用方中的任何变量都不会被绑定。

ECLiPSe -教程简介

第47页(逻辑第37页)

http://eclipseclp.org/doc/tutorial.pdf

我们还在我们的系统中增加了这样一个操作员。现将这些规则写成如下：

simp(0+B, X) ?- !, X = B.
simp(A+0, X) ?- !, X = A.
Etc..

现在我们又回到了通常的表现：

/* Jekejeke Prolog 1.5.0 */
?- time((between(1,380,_), test, fail; true)).
% Up 1,067 ms, GC 11 ms, Threads 1,032 ms (Current 02/14/21 21:43:56)
Yes

太棒了！

开放来源：

Boole 1847年的方法，ECLiPSe Style

https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole3-pl