Prolog中单边统一的Quine算法

如何解决Prolog中单边统一的Quine算法

SWI-Prolog 的新版本 8.3.19 引入了单边统一在新的 Picat 样式规则中。这可能是任何受欢迎的补充序言系统。我想知道我们是否可以重写 Quine 算法

Quine 算法的 Prolog 实现
https://\stackoverflow.com/q/63505466/502187

Picat 样式规则以及这是否可行？如果是，如果 Quine 算法的编写变得更简单，那么 SWI-Prolog 可能这个添加对社区有很大帮助。

有人接受这个挑战吗？ SWI-Prolog 8.3.19 已经从 devel 提供。

解决方法

虽然正常统一又名两侧统一与内置 (=)/2 有着密切的关系，但模式匹配又名单侧统一和内置 (==)/2 之间存在类似的关系。这些引导程序会起作用：

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

如果我们查看 Quine 算法的代码，取自 here，我们会发现很多 (==)/2 用法。模式匹配可以直接完成的工作：

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

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

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

我们做了一些基准测试并验证了来自 Principia 的 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,fail; true)).
% Up 3,525 ms,GC 24 ms,Threads 3,500 ms (Current 02/14/21 11:42:50)
Yes

现在由 SWI-Prolog 新编译的模式匹配：

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

/* pattern matching */
?- time((between(1,0.531 CPU in 0.531 seconds (100% CPU,9298824 Lips)
true.

我期待编译的方法显示出更多的声音并且不仅保留了正常统一的性能？但无论如何，这是一个好的开始。

开源：

1847 年的布尔方法，Prolog 风格
https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole-pl

1847 年的布尔方法，皮卡式
https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole2-pl

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

来自 Principia 的 193 个命题逻辑测试用例
https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-principia-pl

除了使用基于 subsumes/2 的翻译进行单边统一之外的另一种方法是使用较低级别的单边统一。 SWI-Prolog 8.3.19 已经实现了，但我系统的另一个答案没有显示。

我们是否找到其他提供较低级别实现的 Prolog 系统单边统一？事实证明是的，例如 ECLiPSe Prolog：

4.6 匹配
在 ECLiPSe 中，您可以编写使用匹配（或单向统一）而不是头部统一的子句。这样的条款是用 ?- 函子而不是 :- 编写。匹配有属性调用者中的任何变量都不会被绑定。

ECLiPSe - 教程介绍
第 47 页（逻辑第 37 页）
http://eclipseclp.org/doc/tutorial.pdf

我们也在系统中添加了这样的操作符。规则现在写成如下：

if (member.guild.id === serverId) {
   // Your code
}

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

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

注意！

开源：

1847 年的布尔方法，ECLiPSe 风格
https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole3-pl