Lambda the Ultimate

Ludics is tremendously interesting from a proof theoretic point of view. I don't understand more than the first chunk of it yet, and that part is still full of wonderfully productive and useful ideas. It is evidence that there's a whole lot more yet to be done in proof theory.

A single example: the daimon. The core idea is really simple -- if you look at a logic as an algebraic structure, then you'll notice that it lacks certain completeness properties (in order to maintain the consistency of the logic). So, you can introduce rules (the daimon) that make the logic-as-structure complete, but which make it inconsistent as a logic. Now, you can prove theorems which do structural manipulations on proofs, which rely on the completeness properties for their correctness. Then, at the end of the day you throw out any proofs that used the bad rules.

This takes the core insight of structural proof theory -- that proofs are just another kind of mathematical object, like groups or lattices -- and takes it really seriously.

This takes the core insight of structural proof theory -- that proofs are just another kind of mathematical object, like groups or lattices -- and takes it really seriously.

I take it as a given that we ALREADY take this idea really seriously, even before we go "ludic". (You know, proof = program)

I'm not sure why the next step can't be taken incrementally, though, rather than starting over with a whole new set of terminology. The first few pages of the paper look to me like a bunch of familiar ideas renamed to emphasize some new direction.

This approach is great when you want to appear revolutionary, but terrible when you want to be evolutionary and build on previously developed knowledge.

Could this be the beginning of another category theory / set theory type split in the community? I certainly hope not.

(I'm also starting to guess what pressures in the field brought about the new "dialogue semantics" sections in Lectures on the Curry-Howard Isomorphism...)

Reworking old results in a new formalism is great for keeping PhD candidates busy (and for allowing established scholars to make their mark), but it isn't necessarily great for advancing the state of human knowledge.

Do you have any examples of new results (rather than re-interpreted ideas) that have resulted from this new approach Neel?

...I hope to be submitting one pretty soon. I'll toss a link here when the draft is written. :)

Anyway, what Girard is doing bridges the gap between two different strands of research. There's the denotational game semantics kind of stuff, and there's the operational focalization stuff, which he's integrating together. I only really have a firm grasp on the second half, and I'm excited precisely because ludics gives me an angle on understanding the first half and why it's important and enlightening. This isn't the first time he's done it, too -- linear logic was born when Girard started looking for a proof theory corresponding to a denotational doohickey (coherence spaces) that he had cooked up.

It's true that in Locus Solum he's making us jump through hoops for the treat, but he has a track record that makes me confident that it'll be tasty. So hop hop hop for me. :)

I've only skimmed it so far, but it does remind me of Bjarne Stroustrop's famous paper on whitespace-overloading!

"New Impressions of Africa" by Roussel made me comfortable with Scheme!!

The basic construction of each of the work's four cantos is the same: a brief "impression of Africa" is interrupted midway by a parenthesis; this new passage is then interrupted by a further parenthesis and so on until a maximum number of five parentheses is reached and they begin to close again.

"an imagination that joins the mathematicians’ delirium to the poets’ logic"

w