%------------------------------------------------------------------ % 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=