Value & # 8594; in swi-prolog

Question

I have a program in swi-prolog and there is an operator (?) → that I met for the first time, and I don’t know what it does. There is a piece of code that I do not understand:

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

I found that when we have

 X -> Y ; Z 

then if X is true, then Y is executed, otherwise Z. But I do not see how this works in the case shown above.

Thanks in advance.

EDIT:

Honestly, this is part of the computer proof of Arrow's theorem (more precisely, of the base case), this is all the code (from the proof of proof theorem PROLOG, 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))). 

However, I do not know how to treat →. There is a chain of use X-> Y: swf - axioms - Pareto and swf - iia - member.

Answer 1

The Prolog statements only have syntactic sugar for nested terms.

those. instead of writing is(X, +(1,2)) we can write X is 1+2 , because there are corresponding op / 3 declarations for ( is ) / 2 and + . Another story is an interpretation related to such terms. To follow my example, there will be some kind of sentence like is(X, V) :- eval_expression(V, X).

Now it’s true that ( -> ) / 2 is the if / then / else statement (or better if / then, else is entered by the disjunction operator, (;) / 2) when used as the target, but in the code you show probably works as a template selector. That is, if there are other sentences of swf / 3, there is a possibility that the axioms / 3 will be invoked with this expression, which, I think, is an implied implication.

NTN

it displays an image of the code when placed in a SWI-Prolog IDE. The syntax color shows two problems:

• PP in axioms (arrow, V, F) is not used
• swf (F, X) is never called (parameter lost?)

and it seems that dictator / 2 is a recording proposal. I do not know the theorem (I do not have access to the documentation), but I would expect a prediction about social objects.

The first problem does not exist, because PP will be used in pareto / 1. The true problem should be the missing parameter for swf, should look like swf(F, L, X) :- ... but this will lead to a loop.