dmv and trurl's comic are running, and they already got instant positive reaction from random people around the office. So... yeah. I think they're neat, too. Something ought to fill the lamentable void of vaguely surreal, geeky humor that combinator's departure created, anyway.Lunch at Sam's. It's official: I eat there too damn often. My end of the ordering protocol has finally withered away to repetition of the word "yep", in response to "bacon burger, right?" and, subsequently, "lettuce, tomato, no dressing?".
Read some of "Maurice and his educated rodents". I love Pratchett for random light reading. He's kind of predictable, but by the same token I know what I'm getting in to, and fortunately I find the one book that he's written seventeen gajillion and a half times pretty amusing.
Got the type systems homework done. I'm kind of scared about eventually having to be on the teaching end of this stuff, where by "this stuff" I mean roughly the first half of 15-312, with preservation and progress and basic extensions to the simply-typed lambda calculus. I have already done it enough times that it seems kind of dull and obvious-in-hindsight. I mean, seriously. Are they still not teaching kids Curry-Howard in third grade? Have all of my petitions gone unheard?
But, seriously. Still poking at research problem at a bit, but haven't had much time for it today. Still at a bit of an impasse reading [Kosaraju 1982]. Get this:
Lemma 1: Let L be a semilinear set, and let A be a subset of {1,2,...,n}. If L does
not satisfy the property that for every m >= 1 there exists an x in L s.t. for every j in A,
pi_j (x) >= m, then there exists a constant c such that when L is expressed as a union of
linear sets U L_i, for every L_i there exists a j in A s.t. the jth component of every period
of L_i has value 0 (the jth component of the sum of the periods of L_i has zero value)
This is Lemma 1, people. I had to track down a book written by Ginsburg in the 1960's on context-free languages and a bunch of other random topics just to get a feel for semilinearity, and then cope with such expositional and/or mathematical felicities as the fact that he's existentially quantifying over c and then never mentions it again. Not as if needing to dig up a book for background is such an exceptionally unusual thing to do, but I'm starting to feel kind of pessimistic about lifting this proof up to the level of talking about linear logic and proofs as Frank suggested, as mired as it seems to be in grungy number theory. Oh well. I'll still be happy myself if I can reduce MELL to stack petri nets, which I still think is possible.