(*
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