[isabelle] Started auction theory toolbox; announcement, next steps, and questions



Dear Isabelle community,

We are pleased to announce our first step towards building an auction theory toolbox: a complete formalisation of William Vickrey's 1961 theorem on second price auctions (see http://cs.bham.ac.uk/research/projects/formare/code/auction-theory/Vickrey.thy for the code). This has been done as part of our ForMaRE project (Formal Mathematical Reasoning in Economics); see http://cs.bham.ac.uk/research/projects/formare/.

This mail outlines our result and our next steps. We'd also like to ask you for some Isabelle-specific advice on our next steps, and to share and discuss the experiences we've had.

AUCTION THEORY

In second price (or Vickrey) auctions, bidders submit sealed bids; the highest bidder wins, and pays the highest bid of the _remaining_ bids; the losers pay nothing. (See http://en.wikipedia.org/wiki/Vickrey_auction for more information, including a discussion of variants used by eBay, Google and Yahoo!.) Vickrey proved that 'truth-telling' (i.e. submitting a bid equal to one's actual valuation of the good) was a weakly dominant strategy. This means that no bidder could do strictly better by bidding above or below its valuation _whatever_ the other bidders did. Thus, the auction is also efficient, awarding the item to the bidder with the highest valuation.

Vickrey was awarded Economics' Nobel prize in 1996 for his work. High level versions of his theorem, and 12 others, were collected in Eric Maskin's 2004 review of Paul Milgrom's influential book on auction theory ("The unity of auction theory: Milgrom’s master class", Journal of Economic Literature, 42(4), pp. 1102–1115). Maskin himself won the Nobel in 2007.

OUR RESULT AND PLANS

We began our formalisation by rewriting Maskin's proof in a more machine-friendly format (http://cs.bham.ac.uk/research/projects/formare/code/auction-theory/vickrey-paper.pdf). As the proof is case based, this allowed a simple translation to Isabelle.

We plan to formalise the other theorems in Maskin's paper, adding them to an auction theory toolbox, with the eventual goal of proving new theorems about old and new types of auctions.

This will require both re-arrangements of our current formalisation into multiple theories, and generalisations. For example, we now model bidders as an integer range 1,…,n, and their bids as an n-vector of real numbers (actually, as a function from 1,…,n to reals). However, Vickrey's theorem does not assume any _order_ among the participants. It is thus sufficient to treat them as a set, but it must be possible to remove elements from such a set (which we currently do by skipping components of a vector).

QUESTIONS FOR ISABELLE COMMUNITY

We would like to contribute our formalisation to the AFP, but are unsure about the procedure: once accepted and published, can we submit updates? We could imagine submitting this formalisation soon (as it is self-contained and covers a relevant field), but still we are planning to evolve and improve it.

As this was our first major Isabelle formalisation, we may have got a lot of things wrong. We would be grateful if any of you were able to look into the source and tell us of any "anti-patterns" we shouldn't use. I will also follow up on this mail with a number of mails asking specific questions on how certain things in Isabelle work, and with some jEdit bug reports.

COMMENTS ON ISABELLE EXPERIENCE

Overall, we have been quite satisfied with how Isabelle works so far, but we are also trying to take the perspective of our end users (economists with little computer science background), who may find it harder to use. Here are some preliminary notes (some of which may be based on wrong assumptions):

* jEdit gives good feedback about syntax errors and certain semantic errors.
* When developing the structure of a proof, "show ?thesis sorry" placeholders proved useful.
* sledgehammer is very useful for finding justifications for proof steps.
* Local renamings with "let" proved useful in complex proofs.
* It would be nice to be able to introduce proper types (not just type_synonyms) for things such as non-negative real vectors. * In statements such as "!x. p x --> q x" it is tedious (and always the same) to break their structure down to a level where the actually interesting work starts.

Cheers, and thanks in advance for your feedback,

Christoph & Colin & Manfred

--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec, Skype duke4701

→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
  2–5 April 2013, Exeter, UK.  Deadlines 10 Dec (stage 1), 14 Jan (st. 2)
  http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.