peteg's blog

Gonzo: The life and work of Dr. Hunter S. Thompson

/noise/movies | Link

There's an interview with the director at Salon.

The X Files: I Want to Believe

/noise/movies | Link

Man on Wire

/noise/movies | Link

Quantum of Solace

/noise/movies | Link

In a massive cinema at Greater Union on George St, with Jen.

Stories by Nhat Linh

/noise/books | Link

The Việt Nam Literature Project hosts some translations of Nhat Linh's stories by Greg and Monique Lockhart. His Going to France is a great period-piece written at perhaps the height of French colonisation of Indochina, roughly when Hồ Chí Minh was in Europe and Northern Asia.

How to lose friends and alienate people

/noise/movies | Link

Casino Royale

/noise/movies | Link

All Quiet on the Western Front

/noise/movies | Link

/noise/politics | Link

Today I signed up as a life member of the EFA, the Australian version of the Electronic Frontier Foundation. This is the one — and perhaps only — good thing about joining the cashed-up classes, being able to funnel some resources to worthy organisations. Damned if Conroy is going to get an easy ride on this silly filtering idea, when even the previous bunch of muppets had the much better idea of freely providing local-to-your-computer filters to those who wanted them; far more congruent with things-as-they-are-and-should-be.

/noise/beach/2008-2009 | Link

An after-work dip at Gordons Bay. Quite pleasant watching the clouds mount from the west while paddling lazily around. I somewhat regretted not wearing a wife-beater.

/noise/beach/2008-2009 | Link

First non-wetsuit swim of the season, at Coogee. A moderate on-shore wind made for some fairly-hefty-by-Coogee standards waves, which proved my judgement to be quite rusty. The water was very pleasant once in, with a wife-beater, and the evening quite tranquil. Hopefully this sets the mold of after-work beach going.

May's Theorem in Isabelle

/choice/social-choice | Link

Tobias Nipkow has written an article about mechanising some recent proofs of Arrow's Theorem and Gibbard-Satterthwaite in Isabelle, and has kindly cited my clumsy attempts at similar things. In an attempt at differentiation I have polished up my proofs from Sen's magnum opus and added one of May's Theorem. As one might expect from a positive result in social choice theory there are endless reworkings of the original conditions in the literature since 1952, and I am not entirely sure what the state of the art is.

The proof itself is fairly straightfoward, although Sen makes an uncharacteristic slip by unnecessarily arguing by contradiction in his proof of my anonymous_neutral_indifference. When I'm next bored and idle I'll see if that makes any difference in the bigger scheme of things.

The hope is to get all of this into the Archive of Formal Proofs and obtain some feedback on the nastier parts of the mechanisation.

Once more:

arrows_theorem.pdf
An Isabelle-generated document of the development.
darcs get http://peteg.org/isabelle/arrows_theorem/
A darcs repository for the development.

An interested soul has written a great overview of May's life work.

Rule Number One

/noise/movies | Link

Heaven and Earth

/noise/movies | Link