是否可以仅使用纯 Prolog、cut 和 `false` 编写不一致的 Prolog 程序？

Question

这个引起了我对理论的兴趣：

是否可以编写一个不一致的 Prolog 程序，即一个程序根据查询的方式同时回答 false 和 true，只使用纯 Prolog，cut和false?

例如，可以查询p(1)，Prolog 处理器会说false。但是当查询p(X) 时，Prolog 处理器会给出一组答案1、2、3。

这可以通过“计算状态检查谓词”轻松实现，例如var/1（最好称为fresh/1）+ el cut：

p(X) :- nonvar(X),!,member(X,[2,3]).
p(X) :- member(X,[1,2,3]).

然后

?- p(1).
false.

?- p(X).
X = 1 ;
X = 2 ;
X = 3.

如果这是高保证软件，就会出现“哎哟时间”。自然地，任何命令式程序在其他所有行上都会像这样脱轨。

所以。没有那些“计算状态检查谓词”能做到吗？

附言

上面说明了Prolog的所有谓词实际上都带有一个“计算状态”的线程隐藏参数：

p(X,StateIn,StateOut).

可以用来解释var/1和朋友们的行为。当 Prolog 程序只调用既不咨询也不修改 State 的谓词时，它就是“纯”的。好吧，至少这似乎是了解正在发生的事情的好方法。我想。

Answer 1

这是一个非常简单的：

f(X,X) :- !, false.
f(0,1).

然后：

| ?- f(0,1).

yes
| ?- f(X,1).

no
| ?- f(0,Y).

no

因此，Prolog 声称对于带有变量的查询没有解决方案，尽管 f(0,1) 是正确的并且将是两者的解决方案。

Answer 2

这是一次尝试。基本思想是 X 是一个变量，如果它可以与 both a 和 b 统一。但是我们当然不能把它写成X = a, X = b。所以我们需要一个“统一”的测试，它不需要像=/2那样绑定变量就可以成功。

首先，我们需要自己定义否定，因为它是不纯的：

my_not(Goal) :-
    call(Goal),
    !,
    false.
my_not(_Goal).

仅当您的纯 Prolog 概念包含 call/1 时，这才是可接受的。假设它确实如此:-)

现在我们可以使用=/2 和“not not”模式来检查统一性，以在撤消绑定时保持成功：

unifiable(X, Y) :-
    my_not(my_not(X = Y)).

现在我们有了定义var/nonvar检查的工具：

my_var(X) :-
    unifiable(X, a),
    unifiable(X, b).

my_nonvar(X) :-
    not(my_var(X)).

让我们检查一下：

?- my_var(X).
true.

?- my_var(1).
false.

?- my_var(a).
false.

?- my_var(f(X)).
false.

?- my_nonvar(X).
false.

?- my_nonvar(1).
true.

?- my_nonvar(a).
true.

?- my_nonvar(f(X)).
true.

剩下的只是你的定义：

p(X) :-
    my_nonvar(X),
    !,
    member(X, [2, 3]).
p(X) :-
    member(X, [1, 2, 3]).

这给出了：

?- p(X).
X = 1 ;
X = 2 ;
X = 3.

?- p(1).
false.

编辑：call/1的使用不是必须的，不用它写出解决方案很有趣：

not_unifiable(X, Y) :-
    X = Y,
    !,
    false.
not_unifiable(_X, _Y).

unifiable(X, Y) :-
    not_unifiable(X, Y),
    !,
    false.
unifiable(_X, _Y).

查看每个谓词的第二个子句。他们是一样的！以声明的方式阅读这些子句，任何两个术语都不统一，而且任何两个术语都是统一的！当然，由于剪切，您不能以声明的方式阅读这些条款。但我发现这特别引人注目，因为它说明了剪辑是多么的不纯。