Prolog:f(X)= X是否统一？

Question

我对统一的理解有点不完整.我理解基本的统一,但是我遇到了一些问题,但是我的问题并非一致.

我正在观看关于统一的youtube教程,该教程说明如果变量试图与包含该变量的术语进行统一,那么它就不是统一的.

然而,当我输入?- f(X) = Xprolog时,它返回的内容符合......f(f(f(f(f(f(...)))))) ?

我明白为什么会这样......但是我不明白这是否意味着它是不可统一的,正如我所预料的那样,如果它不是可以统一的话,它就会返回'不'.我是否正确地认为尝试统一f(X)= X会失败发生检查,从而使它们不能统一？

Answer 1

是的,你是对的:在逻辑上,一个变量X,当然不是与术语语法unifiable F(X) ,理由是变量本身的发生是由于严格的subterm的F(X) .

因此,所谓的发生检查会导致统一失败.

正如在该文章中正确指出的那样,Prolog实现通常会因效率原因而省略发生检查,这可能导致不正确的推论.

但是,你可以随时进行统一与发生在Prolog的使用ISO谓词检查unify_with_occurs_check/2.正如预期的那样,你所询问的统一在这种情况下失败了:

?- unify_with_occurs_check(X, f(X)).
false.

请注意,在某些Prolog系统中,您可以设置一个标志以启用所有统一的发生检查.

例如,在SWI-Prolog中:

?- set_prolog_flag(occurs_check, true).
true.

?- X = f(X).
false.

我建议您启用此标志以获得声音结果.

需要进行检查的统一通常表示编程错误.因此,您可以将标志设置为抛出错误而不是静默失败.

另请参阅上述评论中与@false 相关的相关问题以及引用的参考文献.