prolog - swi-prolog 中 -> 的含义

Question

我在swi-prolog中有一个程序，里面有一个operator(?) ->，第一次遇到，不知道是干什么的。有一段代码，我不明白:

swf([PP->Q|F], [PP|L], X):- swf(F, L, X), axioms(X, PP->Q, F).

我发现当我们有

X -> Y ; Z

然后，如果 X 为真，则执行 Y，否则执行 Z。但我不明白它在上面显示的情况下是如何工作的。

提前致谢。

编辑:

老实说，这是 Arrow 定理的计算机辅助证明的一部分(更准确地说是基本情况)，这是完整的代码(来自 PROLOG 的 Proving Arrow 定理，Kenryo Indo):

p(Q) :- permutation(Q, [a, b, c]).

p((X, Y), Q) :- p(Q), append(_, [X|B], Q), member(Y, B).

pp((Q1,Q2)) :- p(Q1), p(Q2).

all_pp(L) :- findall(QQ, pp(QQ), L).

axioms(arrow, V, F) :- p(Q), V=(PP->Q), pareto(V), iia(V, F).

swf([], [], _).
swf([PP->Q|F], [PP|L], X):- swf(F, L, X), axioms(X, PP->Q, F).
swf(F, X) :- all_pp(L), swf(F, L, X).

pp(XY, agree, (Q1,Q2)) :- p(XY, Q1), p(XY, Q2).
pp((X, Y), opposite, (Q1, Q2)) :- p((X, Y), Q1), p((Y, X), Q2).

pareto(PP->R) :- \+ (pp(XY, agree, PP), \+ p(XY, R)).

dictator(J, F) :- member(J:PP, [1:(P, _), 2:(_, P)]),
\+ (member(PP->R, F), pp(_, opposite, (P, R))).


agree(+, XY, QQ) :- pp(XY, agree, QQ).
agree(-,(X,Y), QQ) :- pp((Y, X), agree, QQ).

iia(PP->R, F) :- \+ (F \= [], pp(XY, A, PP), member(QQ->S, F),
pp(XY, A, QQ), \+ agree(_, XY, (R, S))).

仍然，我不知道如何治疗 ->。 X->Y 有一个用法链:swf - axioms - pareto 和 swf - iia - member。

Answer 1

在 Prolog 中，运算符只是嵌套术语的语法糖。

即我们可以写 is(X, +(1,2)) 而不是写 X is 1+2 因为有适当的 op/3 ( is)/2 和 + 的声明。另一个故事是与这些术语相关的解释。按照我的示例，某处会有一个子句，例如is(X, V) :- eval_expression(V, X)。

当用作 < em>目标，但在您显示的代码中它用作模式选择器，可能。 IE。如果还有其他子句 swf/3，则有可能使用该表达式调用 axioms/3，我猜这意味着 implication。

HTH

编辑 这里是放置在 SWI-Prolog IDE 中的代码图片。语法颜色显示两个问题:

• 公理中的PP(arrow, V, F)没有被使用
• swf(F, X) 从未被调用(参数丢失？)

似乎 dictator/2 是入口子句。我不知道这个定理(我无权访问文档)，但我希望有一个关于社会实体的断言。

第一个问题不存在，因为pareto/1中会用到PP。真正的问题应该是 swf 缺少参数，应该读作 swf(F, L, X) :- ...，但这会导致循环。