Jason (jcreed) wrote,

I am a police officer! I am the law, eh?

"The Wizard of Speed and CrackTime" is amazing. Ask yourself: are movies the only way you can touch people? I want to have Mike Jittlov's ridiculous-indie-movie-babies. Too bad the DVD was all glitchy, but huge thanks to whichever of _tove's relativesex-boyfriend are responsible for sending it to her.

Also poking around in more detail at how ordered logic ought to get encoded into the labelled LF variant. I was worried at first that something was going wrong, because uniform proofs for ordered logic (and spine form of OLF) have "two ordered contexts" when you focus on the left, because the focal proposition has to live somewhere in the ordered context, and in my system there didn't seem to be any place for that pheomenon to show up. Certainly changing the label algebra isn't going to make an extra context zone magically show up! But after thinking about it for a while, it looks like everything's fine, and in fact it almost seems more elegant with labels. In the spine typing judgment, you have one label-expresion that describes the whole context (including the focal proposition) and another one that describes the resources in the "hole" — so the erstwhile "two zones" are just the stuff remaining on the left and right of the "hole" once you subtract it. This seems to be related to a couple of otherwise mysterious lemmas in the proof of adequacy for embedding LLF anyway, so that's pleasantly illuminating.
Tags: math, movies, work

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded