标签: logical-purity

可能是一个愚蠢的问题,但我无法在任何地方找到任何文档.有没有办法在prolog中执行if,例如,如果变量为0,则执行某些操作(将文本写入终端).甚至不需要else,但我找不到if的任何实现.

different(Xs, Ys) :-
   member(X, Xs),
   non_member(X, Ys).
different(Xs, Ys) :-
   member(Y, Ys),
   non_member(Y, Xs).

虽然这个定义使用member/2和non_member/2几乎是¹从声明的观点完美的,它产生于特定查询的冗余解决方案,并选择留点周围.

什么是改进的定义(以纯粹的方式可能使用if_/3和(=)/3),使得完全相同的解决方案集被描述different/2但至少对于地面查询是确定的(因此不会留下任何无用的选择点)并且省略(如有可能)任何多余的答案？

¹ _{实际上,different([a|nonlist],[]), different([],[b|nonlist])成功了.它同样可能失败.所以两者都失败的解决方案很好(甚至可能更精细).}

该谓词if_/3似乎在Stack Overflow的Prolog部分的少数主要贡献者中相当受欢迎.

这个谓词是这样实现的,由@false提供:

if_(If_1, Then_0, Else_0) :-
   call(If_1, T),
   (  T == true -> call(Then_0)
   ;  T == false -> call(Else_0)
   ;  nonvar(T) -> throw(error(type_error(boolean,T),_))
   ;  /* var(T) */ throw(error(instantiation_error,_))
   ).

但是,我一直无法找到这个谓词的作用的清晰,简单和简洁的解释,以及它与Prolog的经典if-then-else结构相比有什么用处if -> then ; else.

我发现的大多数链接直接使用这个谓词,并且提供了很少的解释,为什么它被使用,Prolog中的非专家可以轻松理解.

lcs([ H|L1],[ H|L2],[H|Lcs]) :-
    !,
    lcs(L1,L2,Lcs).
lcs([H1|L1],[H2|L2],Lcs):-
    lcs(    L1 ,[H2|L2],Lcs1),
    lcs([H1|L1],    L2 ,Lcs2),
    longest(Lcs1,Lcs2,Lcs),
    !.
lcs(_,_,[]).

longest(L1,L2,Longest) :-
    length(L1,Length1),
    length(L2,Length2),
    (  Length1 > Length2
    -> Longest = L1
    ;  Longest = L2
    ).

到目前为止这是我的代码.我怎样才能优化它以便打印前缀,例如:

["interview", "interrupt", "integrate", "intermediate"]

应该回来 "inte"

Prolog有点生疏,有一段时间没做过:)

memberchk/2是一个通常定义的谓词,它是这样定义的member/2:

memberchk(X, Xs) :-
   once(member(X, Xs)).

因此它只能成功地获得第一个答案member/2.它的完整程序意义不适合纯粹的关系.作为其非关系行为的一个例子考虑

?- memberchk(b, [X,b]), X = a.
false.

?- X = a, memberchk(b, [X,b]).
X = a.

另一方面,在许多情况下,memberchk/2将使用充分实例化的参数调用,其中可以将其视为纯关系的有效近似.

背后的一个纯粹的关系是memberd/2(使用if_/3):

memberd(E, [X|Xs]) :-
   if_(E = X, true, memberd(E, Xs) ).

memberchk/2对于充分实例化的案例,是否还有其他可以近似的纯关系？

换句话说:是否是memberd/2一个完整的,声明性的替代品,memberchk/2或者是否仍然存在memberchk/2无法替代的合法案例memberd/2？

如果我想确保两个变量不实例化到同一个术语,那么首选方法是什么？

假设我需要在图中找到有向边,并且节点不能有自己的边:

node(a, x, y). node(b, z, x). node(c, y, y).

(这里的边是 - > c,b - > a,但不是 c - > c)

以下作品:

edge(A, B) :- node(A, _, X), node(B, X, _), A \== B.

这也有效[swi-prolog]:

edge(A, B) :- dif(A, B), node(A, _, X), node(B, X, _).

这显然不起作用(因为A和B都没有被实例化？):

edge(A, B) :- A \== B, node(A, _, X), node(B, X, _).

我想我的第一个解决方案的问题是,使用更复杂的node谓词,在edge失败之前可能会发生许多不必要的统一.在dif另一方面,是在图书馆,这表明它并不意味着在这种简单的情况下使用(虽然它,我似乎在寻找精确的功能).

（根据@repeat的建议）考虑一个纯程序的查询¹ ?- G_0.如果有的话，这个查询?- G_0, G_0.有什么用？

^{脚注
1 没有表格（为了安全），约束是可以的。
上一篇关于这个主题的帖子。}

什么是"逻辑纯度"(在Prolog编程的背景下)？该逻辑纯度标记信息说,"使用程序只喇叭条款",但随后又怎么会谓词喜欢if_/3出线,使用因为它切为多,和各种元逻辑(什么是适当的术语？var/1和这样)谓词,即低级别的东西.

我明白它实现了一些"纯粹"的效果,但这究竟是什么意思呢？

有关更具体的说明,请解释如何if_/3符合逻辑纯度,在使用中看到,例如在此答案中？

我已经阅读了很多关于Prolog的失败否定的内容,其中Prolog是为了证明\+Goal持有试图证明Goal失败.

这与CWA(近距离世界假设)高度相关,例如,如果我们查询\+P(a)(在哪里P是arity 1的谓词),并且我们没有线索导致证明P(a)Prolog假定(由于CWA)not P(a)如此\+P(a)成功.

从我所搜索的内容来看,这是一种解决经典逻辑弱点的方法,如果我们对此毫无头绪,P(a)那么我们无法回答是否\+P(a)持有.

上面描述的是在Prolog中引入非单调推理的方法.此外,有趣的部分是Clark证明Negation by Failure与经典否定相容/类似仅适用于地面条款.我明白这个例子:

X=1, \+X==1.:应该在Prolog中返回false(在经典逻辑中).

\+X==1, X=1.:应该在经典逻辑中返回false,但是在检查NF的时候它在Prolog中成功,X不受约束,这与classic-Pure Logic不同.

\+X==1.:在X绑定之前,不应该给经典逻辑中的任何答案,但在Prolog中它返回false(可能打破经典逻辑的弱点),这与纯逻辑不相同/兼容.

我的尝试是模拟经典否定,感谢评论中的@false的建议,目前的实施是:

\\+(Goal) :- when(ground(Goal), \+Goal). 

一些测试:

?- \\+(X==1).
when(ground(X), \+X==1).

?- X=1, \\+(X==1).
false.

?- \\+(X==1), X=1.
false. 

我的问题:

以上是对经典否定的正确解释吗？(是否有任何明显的极端情况,它错过了？当使用/ 2时我也关注逻辑纯度,可以安全地假设上面是纯粹的吗??).

到目前为止,我一直坚持 Prolog程序意味着:

如果对于一个查询Q,有一个subterm S,使得存在一个术语T,使?- S=T, Q. 成功虽然?- Q, S=T. 失败,然后通过调用一个谓词Q是不踏实.

直觉上,我因此坚定地表示我们不能使用实例化来"欺骗"谓词来提供解决方案,否则这些解决方案不仅不会被给予,而是被拒绝.注意非终止程序的区别!

特别是,至少在我看来,逻辑纯度总是意味着坚定不移.

例子.为了更好地理解坚定性的概念,考虑这个属性的几乎经典的反例,在将高级学生引入Prolog的操作方面时经常引用,使用两个整数之间关系的错误定义及其最大值:

integer_integer_maximum(X, Y, Y) :-
        Y >= X,
        !.
integer_integer_maximum(X, _, X).

这个中的一个明显错误 - 我们应该说" 摇摆不定 " - 定义当然是以下查询错误地成功:

?- M = 0, integer_integer_maximum(0, 1, M).
M = 0. % wrong!

而交换目标产生了正确的答案:

?- integer_integer_maximum(0, 1, M), M = 0.
false.

这个问题的一个很好的解决方案是依靠 …