Jason (jcreed) wrote,

I've been reading Jeff Polakow's PhD thesis the last couple days. It's quite interesting. It basically has four kinds of stuff in it:

1. Things that I feel I could easily reconstruct given just the end result and enough time, because really, I understand what ordered logic ought to be, and much of it plays out just like you'd expect. Pleasantly routine — to put it an even nicer way, canonical-seeming — properties and proofs. These things make me feel all smart and stuff. Examples: basic logic and type theory, and the uniform proof system.
2. Things that I feel I could reconstruct, but god it would be so annoying, because we have better technology now. These things make me feel immensely grateful for the collateral inventions that came along with the development CLF, by which I mean I am immensely grateful for something I like to call "Kevin Watkins". Examples: tedious decidability proofs, logical relations arguments, type conversion rules, and the gaping chasm between the definitional and algorithmic systems.
3. Things that perplex me so much I don't understand what it is I don't understand. Coupla chapters like this. Things like how he handles the nondeterminism peculiar to the ordered system, because when you pick an unrestricted or mobile formula to copy and focus on, you have to decide where in the ordered context it shows up.
4. Delicious examples of ordered logic programs. I hope to cook up some way of handling their metatheory in my framework, but yikes it looks hard right now.
Tags: math, 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