(* Auction Theory Toolbox (http://formare.github.io/auctions/) Authors: * Manfred Kerber * Christoph Lange * Colin Rowat * Marco B. Caminati Dually licenced under * Creative Commons Attribution (CC-BY) 3.0 * ISC License (1-clause BSD License) See LICENSE file for details (Rationale for this dual licence: http://arxiv.org/abs/1107.3212) *) header {* combinatorial Vickrey auction *} theory CombinatorialVickreyAuction imports CombinatorialAuction CombinatorialAuctionTieBreaker Maximum begin section {* value-maximising allocation (for winner determination) *} text {* the set of value-maximising allocations (according to the bids submitted), i.e.\ the arg max'' of @{const value_rel} on the set of all possible allocations *} definition winning_allocations_rel :: "goods \ participant set \ bids \ allocation_rel set" where "winning_allocations_rel G N b = arg_max' (value_rel b) (possible_allocations_rel G N)" (* CL: probably not needed, neither for close-to-paper nor for computable version definition winning_allocations_fun :: "goods \ participant set \ bids \ allocation_fun set" where "winning_allocations_fun G N b = { (Y,potential_buyer) . value_fun b (Y,potential_buyer) = max_value G N b }" *) text {* the unique winning allocation that remains from @{const winning_allocations_rel} after tie-breaking (assuming relational allocations) *} fun winning_allocation_rel :: "goods \ participant set \ tie_breaker_rel \ bids \ allocation_rel" where "winning_allocation_rel G N t b = t (winning_allocations_rel G N b)" (* CL: probably not needed, neither for close-to-paper nor for computable version definition winning_allocation_fun :: "goods \ participant set \ tie_breaker_fun \ bids \ allocation_fun" where "winning_allocation_fun G N t b = t (winning_allocations_fun G N b)" *) text {* algorithmic version of @{const winning_allocations_rel} *} fun winning_allocations_alg_CL :: "goods \ participant set \ bids \ allocation_rel list" where "winning_allocations_alg_CL G N b = (arg_max_alg_list (possible_allocations_alg G N) (value_rel b))" text {* alternative algorithmic version of @{const winning_allocations_rel} *} fun winning_allocations_alg_MC :: "goods \ participant set \ bids \ allocation_rel list" where "winning_allocations_alg_MC G N b = (let all = possible_allocations_alg G N in map (nth all) (max_positions (map (value_rel b) all)))" text {* algorithmic version of @{const winning_allocation_rel} *} fun winning_allocation_alg_CL :: "goods \ participant set \ tie_breaker_alg \ bids \ allocation_rel" where "winning_allocation_alg_CL G N t b = t (winning_allocations_alg_CL G N b)" text {* alternative algorithmic version of @{const winning_allocation_rel} *} fun winning_allocation_alg_MC :: "goods \ participant set \ tie_breaker_alg \ bids \ allocation_rel" where "winning_allocation_alg_MC G N t b = t (winning_allocations_alg_MC G N b)" text {* payments *} text {* the maximum sum of bids of all bidders except bidder @{text n}'s bid, computed over all possible allocations of all goods, i.e. the value reportedly generated by value maximization problem when solved without n's bids *} fun \ :: "goods \ participant set \ bids \ participant \ price" where "\ G N b n = Max ((value_rel b) ` (possible_allocations_rel G (N - {n})))" text {* algorithmic version of @{text \} *} fun \_alg :: "goods \ participant set \ bids \ participant \ price" where "\_alg G N b n = maximum_alg_list (possible_allocations_alg G (N - {n})) (value_rel b)" (* CL: probably not needed, neither for close-to-paper nor for computable version definition winners'_goods_fun :: "goods \ participant set \ tie_breaker_fun \ bids \ participant option \ goods" where "winners'_goods_fun G N t b = inv (snd (winning_allocation_fun G N t b))" *) (* CL: probably not needed, neither for close-to-paper nor for computable version definition remaining_value_fun :: "goods \ participant set \ tie_breaker_fun \ bids \ participant \ price" where "remaining_value_fun G N t b n = (\ m \ N - {n} . b m (winners'_goods_fun G N t b (Some m)))" *) text {* the sum of bids of all bidders except bidder @{text n} on those goods that they actually get, according to the winning allocation *} fun remaining_value_rel :: "goods \ participant set \ tie_breaker_rel \ bids \ participant \ price" where "remaining_value_rel G N t b n = (\ m \ N - {n} . b m (eval_rel_or ((winning_allocation_rel G N t b)\) m {}))" text {* algorithmic version of @{text remaining_value_rel} *} fun remaining_value_alg :: "goods \ participant set \ tie_breaker_alg \ bids \ participant \ price" where "remaining_value_alg G N t b n = (\ m \ N - {n} . b m (eval_rel_or (* When a participant doesn't gain any goods, there is no participant \ goods pair in this relation, but we interpret this case as if 'the empty set' had been allocated to the participant. *) ( (* the winning allocation after tie-breaking: a goods \ participant relation, which we have to invert *) (winning_allocation_alg_CL G N t b)\) m (* evaluate the relation for participant m *) {} (* return the empty set if nothing is in relation with m *) ))" (* CL: probably not needed, neither for close-to-paper nor for computable version definition payments_fun :: "goods \ participant set \ tie_breaker_fun \ bids \ participant \ price" where "payments_fun G N t = \ G N - remaining_value_fun G N t" *) text {* the payments per bidder *} fun payments_rel :: "goods \ participant set \ tie_breaker_rel \ bids \ participant \ price" where "payments_rel G N t = \ G N - remaining_value_rel G N t" text {* algorithmic version of @{text payments_rel} *} fun payments_alg :: "goods \ participant set \ tie_breaker_alg \ bids \ participant \ price" where "payments_alg G N t = \_alg G N - remaining_value_alg G N t" text {* alternative algorithmic version of @{text payments_rel}, working around an Isabelle2013 bug *} section {* the Combinatorial Vickrey Auction in relational form *} (* TODO CL: revise the following as per https://github.com/formare/auctions/issues/35 *) (* TODO CL: we may need nVCG-specific notions of "valid input" *) text {* combinatorial Vickrey auction in predicate form, where \begin{itemize} \item input is a valid input to an nVCG auction, and \item outcome is obtained from input according to the definitions above. \end{itemize} *} definition nVCG_pred :: "tie_breaker_rel \ goods \ participant set \ bids \ allocation_rel \ payments \ bool" where "nVCG_pred t G N b x p \ valid_input G N b \ x = winning_allocation_rel G N t b \ p = payments_rel G N t b" text {* Checks whether a combinatorial auction in relational form, given some tie-breaker, satisfies @{const nVCG_pred}, i.e.\ is a combinatorial Vickrey auction. For such a relational form we need to show that, given an arbitrary but fixed tie-breaker, for each valid input, there is a unique, well-defined outcome. *} definition nVCG_auction :: "tie_breaker_rel \ combinatorial_auction_rel \ bool" where "nVCG_auction t = rel_sat_pred (nVCG_pred t)" text {* The combinatorial Vickrey auction in relational form *} definition nVCG_auctions :: "tie_breaker_rel \ combinatorial_auction_rel" where "nVCG_auctions t = rel_all (nVCG_pred t)" end