I am trying to formalise Vickrey's 1961 result on equilibrium in second-price
auctions. (See Maskin's 2004 "The Unity of Auction Theory: Milgrom's
Masterclass", J. Ec. Literature for a concise presentation of this and other
results.)
Doing so involves:
(a) N = {1, ..., n}, a set of bidders;
(b) v in R^n_+, a vector of bidders' valuations;
(c) b in R^n_+, a vector of bids, formed by strategies mapping from valuations;
(d) x in bool^n, setting x[i] = T if the auction awards the good to bidder i,
and F otherwise;
(e) p in R^n, a vector of prices to be paid by the bidders, as specified by the
auction;
(f) an auction, a map from b, the bids, to x,p.
To establish the result, I wish to define:
(1) \bar{y} = max_{j in N} y_j for any y in R^n
(2) \bar{y}_{-i} = max_{j in N\{i}} y_j, also for any y in R^n
(3) u[i] (b,v,p) = -p[i] if x[i] = F, else v[i]-p[i], bidder i's payoff
In trying to define these, I have encountered two questions:
(i) is there a straightforward way of extending real_max to define the first
two objects?
(ii) how do I specify the role of the Boolean condition in u[i]? My naïve
attempt to just
let payoff = new_definition `(payoff:real^N->real^N->real^N) v p =
lambda i. (if ~(x:bool^N$i) then &0- p$i else v$i - p$i)`;;
yields a "typechecking error (initial type assignment)".
Any help with either of these questions would be gratefully appreciated.
Thank you,
Colin Rowat
University of Birmingham
p.s. A second-price auction (SPA) allocates the good to the highest bidder, who
pays the bid of the second highest bidder; no bidder other than the winner pays
anything. Vickrey's result is that SPA admit a type of equilibrium that makes
minimal informational assumptions about other bidders, known as an equilibrium
in weakly dominant strategies - such that each bidder is at least as well off
sticking to its bid, whatever else the other bidders are doing. (Contrast to a
[Bayesian] Nash equilibrium: the bidder is at least as well off with its bid,
given particular bids by others.) The equilibrium bids in an SPA have the
following form: bidders bid their valuations, so that b[i] = v[i], and the
auction is efficient (awarding the good to a bidder valuing it most highly).
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
