与发生检查的差异答案

【问题标题】：dif with occurs check与发生检查的差异
【发布时间】：2020-09-29 14:53:49
【问题描述】：

是否存在带有发生检查的差异？这在这里有效：

Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.7)

?- set_prolog_flag(occurs_check, true). 
true.

?- dif(X,f(Y)), X = Y.
X = Y.

但上述不可行，因为发生检查是一个全局标志，我得到以下信息：

SWI-Prolog console for thread 3

?- X=f(X).
false.

【问题讨论】：

Here 是一个实现的草图。
这不应该被认为是 SWI 中的一个错误吗？
我的意思是(=)/2相当于unify_with_occurs_check/2，而OC是true。

标签： prolog prolog-dif occurs-check

【解决方案1】：

现在，Scryer 支持 dif/2 在设置相应标志时进行发生检查：

?- use_module(library(dif)).
   true.
?- set_prolog_flag(occurs_check, true).
   true.
?- dif(-X,X).
   true.
?- dif(-X,Y).
   dif:dif(- X,Y).
?- dif(-X,X), X = a.
   X = a.

【讨论】：

好。除此之外，一个专用的dif_with_occurs_check/2 也很好 - 很好地平行于unify_with_occurs_check/2...
@repeat：还有 unify_without_occurs_check/2 吗？将是最好的 subsumes_term/2
好的，但是可能有些系统在没有循环的情况下无法实现unify_without_occurs_check/2。而subsumes_term/2 内部的实现方式可能有所不同。
@repeat：具有循环算法的系统必须以不同的方式实现它。但是，是的，它可能只适用于具有理性树的系统。顺便说一句，当发生检查关闭时，您是否了解 Tau 中到底发生了什么？

【解决方案2】：

在我的系统中，我创建了一个新的谓词dif_with_occurs_check/2。顾名思义，它是dif/2，带有发生检查，因此无需设置标志。但是还有一个额外的好处，dif/2 进行了优化，可以监听更少的变量：

/* listens only to changes in X */
?- dif(X, f(Y)).
/* listens to changes in X and Y */
?- dif_with_occurs_check(X, f(Y)).

这是必要的，以便我们可以在将变量Y 更改为Y = X 时唤醒dif_with_occurs_check/2。然后dif_with_occurs_check/2 将删除它自己的约束X = f(Y)，它已成为X = f(X)，因此已过时。

?- dif(X,f(Y)), X = Y.
X = Y,
dif(Y, f(Y))
?- dif_with_occurs_check(X,f(Y)), X = Y.
X = Y

开源：模块“herbrand”
https://github.com/jburse/jekejeke-devel/blob/master/jekmin/headless/jekmin/reference/term/herbrand.p

【讨论】：