You selected vickrey.pl
%------------------------------------------------------------------
% An automated proof of implementability on Vickrey's auction
%------------------------------------------------------------------
% vickrey.pl
% By Kenryo Indo (Kanto Gakuen University)
% 10-12 Sep 2004.
%----------------------------------
% symbolic model of the auction
%----------------------------------
% v: true valutation (of the agent) for the good for sale.
% s: reported valutation by the agent.
% r: reported valuation of the second highest price.
% w: max price over reported valuations by all agents.
% u: the payoff for the agent that
% u= v-r if s=w (and under random choice when tie).
% u= 0 otherwise.
% pseudeo-Prolog code for the rule of auction to decide a winner and payoffs:
% is_win(report(s),gain(u),yes):- second_highest(r), s>r, u is v-r, !.
% is_win(report(s),gain(0),no).
%------------------------
% sketch of the proof
%------------------------
% patterns of strategy:
% [st]: truth-telling, st=v.
% [s~]: over-valuation, s~>v.
% [s_]: under-valuation, s_ ut
% ).
% proof policy
% To compare the gain intervals induced by relation between [*] and r.
% More specifically, do the two step procedure as follows. First,
% extend the winner rule like above by inequality relation patterns among [s,v,r].
% Second, perturb strategy s and then compute new gain by matching the pattern.
:- dynamic reported_value/1,true_valuation/1,second_price/1.
reported_value(s).
true_valuation(v).
second_price(r).
% the main: spa/3.
spa(REL,result(T),utility(U)):-
reported_value(S),
true_valuation(V),
second_price(R),
generate_spa_order((S,V,R),REL),
check_consistency_of_order(REL),
spa_rule(REL,T,U).
spa_rule([(S,>,R),(V,E,R),(S,_F,V)],win,utility((V-R,E,0))).
spa_rule([(S,=,R),(V,=,R),(S,_F,V)],loss,utility(0)).
spa_rule([(S,=,R),(V,_E,R),(S,_F,V)],loss,utility(0)).
spa_rule([(S,<,R),(V,_E,R),(S,_F,V)],loss,utility(0)).
% older code:
spa_rule_old(S,R,T,U):-
is_win([S,R],T1),
T = T1,
payoff_of_spa(T,U).
% is_win/2
is_win([S,R],win):-
spa_order_0((R,'<',S)),
!.
is_win(_,loss).
%payoff_of_spa/2
payoff_of_spa(loss,0).
payoff_of_spa(win,(V-R,REL,0)):-
true_valuation(V),
second_price(R),
spa_order_0((V,REL,R)).
% testing implementability.
test_impl(strategic(D,E,F),truthful(A,B,C)):-
spa(A,B,C),A=[_P,Q,(S,=,V)],
spa(D,E,F),D=[_R,Q,(S,T,V)],
T \= '=',
critical_case_for_impl(E,C).
critical_case_for_impl(result(win),_).
critical_case_for_impl(_,utility((_,<,0))).
critical_case_for_impl(_,utility((_,=<,0))).
/*
?- test_impl(A,B).
A = strategic([ (s, >, r), (v, =, r), (s, >, v)], result(win), utility(utility((v-r, =, 0))))
B = truthful([ (s, =, r), (v, =, r), (s, =, v)], result(loss), utility(utility(0))) ;
A = strategic([ (s, >, r), (v, >, r), (s, >, v)], result(win), utility(utility((v-r, >, 0))))
B = truthful([ (s, >, r), (v, >, r), (s, =, v)], result(win), utility(utility((v-r, >, 0)))) ;
A = strategic([ (s, >, r), (v, >, r), (s, <, v)], result(win), utility(utility((v-r, >, 0))))
B = truthful([ (s, >, r), (v, >, r), (s, =, v)], result(win), utility(utility((v-r, >, 0)))) ;
A = strategic([ (s, >, r), (v, <, r), (s, >, v)], result(win), utility(utility((v-r, <, 0))))
B = truthful([ (s, <, r), (v, <, r), (s, =, v)], result(loss), utility(utility(0))) ;
No
*/
%-------------------------------------------------
% generate and test for consistent orders
%-------------------------------------------------
:- dynamic spa_order_0/1.
initialize_spa_order:-
abolish(spa_order_0/1).
generate_spa_order((S,V,R),VS):-
(var(S)->reported_value(S);true),
(var(V)->true_valuation(V);true),
(var(R)->second_price(R);true),
findall([(S,E,R),(V,F,R),(S,G,V)],
(
pairwise_inequality(E,S,R),
pairwise_inequality(F,V,R),
pairwise_inequality(G,S,V)
),
VSS),
member(VS,VSS),
initialize_spa_order,
forall(member((X,Y,Z),VS),
assert(
spa_order_0((X,Y,Z))
)
).
spa_order((X,Y,Z)):-
spa_order_1((X,Y,Z),_).
spa_order((X,Y,Z),H):-
spa_order_1((X,Y,Z),H).
%;spa_order_2((X,Y,Z),H).
% unified direction '=<' or '<' at the root
spa_order_1((X,Y,Z),[X,Y,Z]):- clause(spa_order_0((X,Y,Z)),_), member(Y,['<','=<']).
spa_order_1((X,'<',Z),[X,'<',Z]):- clause(spa_order_0((Z,'>',X)),_).
spa_order_1((X,'=<',Z),[X,'=<',Z]):- clause(spa_order_0((Z,'>=',X)),_).
% equality as bidirection
spa_order_1((X,'=<',Z),[X,'=<',Z]):- clause(spa_order_0((X,'=',Z)),_).
spa_order_1((X,'=<',Z),[X,'=<',Z]):- clause(spa_order_0((Z,'=',X)),_).
% reversing directions
spa_order_1((X,'>',Z),H):- spa_order((Z,'<',X),H1),reverse(H1,H).
spa_order_1((X,'>=',Z),H):- spa_order((Z,'=<',X),H1),\+ spa_order((Z,'<',X),_),reverse(H1,H).
% implications (1st order)
spa_order_1((X,'=<',Z),H):- spa_order((X,'<',Z),H).
spa_order_1((X,'>=',Z),H):- spa_order((X,'>',Z),H).
spa_order_1((X,'=',Z),[X,Y|H]):- spa_order((X,'=<',Z),[X,Y,Z]),spa_order((Z,'=<',X),H).
spa_order_2((X,Y,Z),H):-
spa_order_1((X,Y,Z),H).
% implications (higher order)
spa_order_2((X,Y,Z),[X,Y|H]):-
member(N,[1,2,3,4,5]),length(H,N),
a_hypothetical_comparison(X,Y,Z),
spa_order_2((W,'=<',Z),H),
W \= Z,
member(Y,['<','=<']),
spa_order_2((X,Y,W),[X,Y,W]),
X \= W,
\+ member(X,H). %,nl,write(1:(W,'=<',Z)).
spa_order_2((X,Y,Z),[X,'<'|H]):-
member(N,[1,2,3,4,5]),length(H,N),
a_hypothetical_comparison(X,Y,Z),
member(Y,['<','=<']),
spa_order_2((W,Y,Z),H),
W \= Z,
spa_order_2((X,'<',W),[X,'<',W]),
X \= W,
\+ member(X,H). %,nl,write(2:(W,Y,Z)).
a_hypothetical_comparison(X,Y,Z):-
pairwise_inequality(Y,X,Z),
reported_value(S),
true_valuation(V),
second_price(R),
member(X,[S,V,R]),
member(Z,[S,V,R]).
pairwise_inequality('=',A,B):-(number(A),number(B),(A is B; B is A));A==B;true.
pairwise_inequality('>',A,B):- (number(A),number(B),A>B);true.
pairwise_inequality('<',A,B):- (number(A),number(B),A=',A,B):- (number(A),number(B),A>=B);true.
%pairwise_inequality('=<',A,B):- (number(A),number(B),A=
return to front page.