Значение -> in swi-prolog

Question

У меня есть программа в swi-prolog и есть оператор (?) ->, с которым я встречался в первый раз, и я не знаю, что он делает , Существует фрагмент кода, который я не понимаю:

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

Я обнаружил, что, когда мы имеем

X -> Y ; Z 

тогда, если X истинно, то Y выполняется, иначе Z. Но дон Посмотрите, как это работает в случае, показанном выше.

Заранее спасибо.

EDIT:

Честно говоря, это часть компьютерного доказательства теоремы Эрроу (точнее - базовый случай), это весь код (из доказательства теоремы Эрроу на Прологе Kenryo индо) :

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 - аксиом - парето и swf - iia - член.

Answer 1

В операторе Prolog есть только синтаксический сахар для вложенных терминов.

I.e. вместо того, чтобы писать is(X, +(1,2)), мы можем написать X is 1+2, потому что есть соответствующие op/3 объявления для (is)/2 и +. Другая история - это интерпретация, связанная с такими терминами. Для того, чтобы последовать моему примеру, там будет где-то пункт как is(X, V) :- eval_expression(V, X).

Теперь это правда, что (->)/2 это если/то/иначе оператор (или лучше, если/то, то еще вводится оператором дизъюнкции , (;)/2) при использовании в качестве цели, но в коде, который вы показываете, он работает как селектор паттернов, возможно. То есть если есть другие предложения swf/3, есть вероятность, что аксиомы/3 будут вызваны с этим выражением, что, я думаю, имеет значение implication.

НТН

редактировать здесь картина кода при размещении в SWI-Prolog IDE. Синтаксис цвет показывает две проблемы:

• PP в аксиомах (стрелка, V, F) не используется
• швейцарских франков (F, X) не вызывается (параметр потерял?)

и кажется, что диктатор/2 является пунктом предложения. Я не знаю теорему (у меня нет доступа к документации), но я бы ожидал предикатов о социальных объектах.

Первая проблема не существует, потому что PP будет использоваться в pareto/1. Истинная проблема должна быть отсутствующим параметром для swf, должна выглядеть как swf(F, L, X) :- ..., но это приведет к циклу.