16 Oct 2003 raph   » (Master)

Voting

The Independent has a story reinforcing my recent comments about shady dealings in electronic voting. It's nice to see this story getting more widespread attention.

I have one nutty idea about how to maybe make a difference: take out an ad in the IACREOT newsletter. Unlike the NYT full-page ad idea that's floating around in blogspace, it would only cost a few hundred bucks, and it would give a good opportunity to roundly criticize election officials for rolling over for corrupt corporate merchants of tamper-friendly voting machines, and encourage them to clearly take sides. I imagine that very few election officials actively want to preside over one of the darkest eras in democracy facing this country.

Google failure

A couple of followups on my piece on Google's vulnerability to DNS abuse. Charles Cox points out a WebmasterWorld post from a Google person this March that clearly points out that they're aware of the problem and are trying to fix it. I'm not sure exactly why they're still so vulnerable, then.

Also, Andrew Clausen sent me his draft paper analyzing the attack-resistance of Google and its PageRank algorithm. I haven't had a chance to study it in detail yet, but from a skim it looks very good. If you're at all interested in trust issues, it's a must-read

Proofs

Thanks, chalst, for your link to the Girard book. I will indeed study it, which should help clear up my ignorance of the finer points of consequence relations and consistency proofs.

I haven't been writing much about my thoughts on proof systems, but I have been continuing to play with them quite a bit. I've been chipping away at a prototype of the ideas I wrote about here. It's all based very solidly on Metamath, but adds a sound definitional framework (so that axioms and definitions are clearly separated), and the outline of a modular system so that individual proofs can import and export "interfaces", and then you can just wire a big mesh (acyclic network) of these proofs my making the interfaces match up. I think that my current design can do this, but I'm never certain about things until I implement them.

And perhaps there my goal is a bit overly ambitious for my current level of ability. I'm trying to cook up not just one set of axioms but three (based on Z2, HOL, and ZFC, in order of increasing strength), so that you can write individual proofs using the least powerful axiomatization necessary, but then use those proofs in any system at least as strong. Not only that, but I want the theorems proved to be polymorphic. For example, some of the theorems most interesting to me are over the structures induced by pairs and "options" (typically defined as either None or Some x). These include sequences, dictionaries, trees, graphs, and so on, in other words the usual space of "data structures".

All the axiom systems listed above can easily support these data structures, but just proving your theorems in Z2 is not fully satisfying. If you prove a general theorem about trees, there's no reason it shouldn't work for, say, trees of transfinite ordinals, even though there's no way to represent transfinite ordinals in Z2. Most people designing proof systems just pick an axiomatization. That's part of the reason why it's traditionally difficult to port proofs from one system to another - there's no guarantee you can when the underlying axiomatizations differ. If I'm successful, then proof authors and proof users will be subject to a form of Postel's Law: be conservative in what axioms you need, but liberal in what axioms you can work with.

Pairs and options in three axiomatizations

I've never seen these all together like this, and I consider them pretty. They're particularly simple variants of functions that pair up primitive values, and set up option types. The specification of correctness is:

pair(a, b) = pair(a', b') <-> a = a' ^ b = b'
some(a) = some(a') <-> a = a'
some(a) != none().

Z2:
pair(a, b) = (a + b) * (a + b) + b * b
some(a) = a + 1
none() = 0

HOL:
pair(a, b) = \lambda x \lambda y. x = a ^ y = b
some(a) = \lambda x. x = a
none() = \lambda x. false

ZFC:
pair(a, b) = {{a}, {a, b}}
some(a) = {a}
none() = {}

Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!