There's an interview with the director at Salon.
In a massive cinema at Greater Union on George St, with Jen.
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.
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.
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.
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.
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.
An interested soul has written a great overview of May's life work.
