- >在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.但我不在上面的情況下，看不出它是如何工作的。

在此先感謝。

編輯：

說實話，這是阿羅定理的計算機輔助證明的一部分（更準確地說 - 基本情況），這是整個代碼（由PROLOG證明阿羅定理，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 - 公理 - pareto和swf - iia - 成員。

Answer 1

在Prolog運算符中，嵌套術語只是語法糖。

I.e.我們可以寫X is 1+2，而不是寫is(X, +(1,2))，因爲（is）/ 2和+有適當的op/3聲明。另一個故事是與這些術語相關的解釋。按照我的實例，會某處條款像is(X, V) :- eval_expression(V, X).

現在這是真的，（->）/ 2這是一個的if/then/else語句運營商（或者更好，如果/那時，否則由脫節運營商推出，（;）/ 2），當用作目標，但在代碼中顯示它可用作模式選擇器，可能是。即如果還有其他從句swf/3，那麼公理/ 3有可能被這個表達式調用，我猜的意思是暗示。

HTH

編輯這裏是代碼的圖像放置在SWI-Prolog的IDE時。語法顏色說明兩個問題：

• PP在公理（箭頭，V，F）不使用
• SWF（F，X）永遠不會被調用（參數丟失了？）

似乎獨裁者/ 2是入口條款。我不知道這個定理（我沒有權限訪問文檔），但我期望對社會實體有一個預言。

第一個問題不存在，因爲PP將在pareto/1中使用。真正的問題應該是swf的缺失參數，應該像swf(F, L, X) :- ...那樣讀取，但這會導致循環。