CODEWITHSUNDEEP
prolog
Grzes
Grzes

Reputation: 971

Meaning of -> in swi-prolog

I have a program in swi-prolog and there is an operator(?) ->, which I have met for the first time and I don't know what it is doing. There is a fragment of code, which I don't 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 don't see how it works in the case shown above.

Thanks in advance.

EDIT:

To be honest, this is a part of computer-aided proof of Arrow's theorem (more precisely - the base case), this is entire code (from Proving Arrow’s theorem by 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))).

Still, I don't know how to treat ->. There is a chain of usages of X->Y: swf - axioms - pareto and swf - iia - member.

Upvotes: 3

Views: 6323

Answers (1)

CapelliC
CapelliC

Reputation: 60014

In Prolog operators are just syntax sugar for nested terms.

I.e. instead of writing is(X, +(1,2)) we can write X is 1+2 because there are proper op/3 declarations for (is)/2 and +. Another story is the interpretation associated to such terms. To follow my example, there will somewhere a clause like is(X, V) :- eval_expression(V, X).

Now it's true that (->)/2 it's a if/then/else operator (or better if/then, the else is introduced by the disjunction operator, (;)/2), when used as a goal, but in the code you show it works as pattern selector, probably. I.e. if there are other clauses swf/3, there are chances that axioms/3 get called with that expression, that I guess is meaning implication.

HTH

edit here is the picture of the code when placed in SWI-Prolog IDE. Syntax color shows two problems:

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

enter image description here

and it seems that dictator/2 is the entry clause. I don't know the theorem (I don't have access to documentation), but I would expect a predication about social entities.

The first problem doesn't exists, because PP will used in pareto/1. The true problem should be the missing parameter to swf, should read like swf(F, L, X) :- ..., but that would result in a loop.

Upvotes: 4

Related Questions