Advisor meeting with Frank went fine. He pointed out that there might be a consumer of irrelevance foo in Karl, for TILT stuff. Maybe. Idunno. My summer flare-up of irritation with proof irrelevance as a concept has all but vanished. Perhaps catamorphism might have something to say about continuing to work on senior-thesis research, though? (this was mine) In any event, it would be a good excuse for learning compiler guts. I have been all about "good excuses" lately. It's so easy to want to know all sorts of things, but hard to feel compelled to learn them without some sort of extrinsic motivator. Pretending that I have any chance at making progress on the MELL question has been pretty fruitful as a motivator, though: now I have some understanding the proofs of the decidability of Petri Net reachability and the undecidability of Petri Net equivalence and Hilbert's Tenth Problem, and I think I'll soon dig through some literature on higher order unification and matching soon just to make my mental toolbox of problems-to-reduce-to-and-from a bit bigger. Mmmath. I mean, ahahaha, theoretical computer science. Yes, the thing with computers. Very useful. Yes. Not just pure wanking. Hahaha.
I was almost a good little grad student and went straight to doing the complexity theory homework after class but instead I visited the lounge and then wandered around Wean trying to find a quiet spot to work and bumped into a poster advertising a talk by Nuel Belnap at 3:30. Went to the talk, of course. Neat stuff. It was about reconciling nondeterminism and the sort of locality required by special relativity without (necessarily, though there is other work that includes it) the full machinery of Minkowski spacetime and so forth. The theory is a collection of axioms on a partial order on events that is thought of as a causality relation. In a single "history", a single space-time, we have a < b if a is in the past light-cone of b. But most generally, a < b if b can occur as an event in the future light-cone of a, and a "history" is a maximal <-directed subset of the set of all possible events. So... yeah. Weird.
Finally got some of the complexity theory done. Problem 3 finished, still thinking about problem 2, but it's harder than I thought. Maybe I'll think of something tomorrow morning.