Jason (jcreed) wrote,

Guess what popular NBC sitcom named "30 Rock" I have been watching too much of lately? I will give you three guesses.

Still managing some productivity despite it. Rewriting the core type-theory-and-proof-of-correctness chapter of thesis to make it more readable and filling in some proof gaps. I looked again at Frank's generalized induction hypothesis for the identity theorem and noticed the fact that the mysterious "negative focus on the right" (or in his notation, the gap between Γ |- [N] > C and Γ |- C) is exactly what an atomic term is: an atomic term of type N is exactly the discrepancy between a spine from N to C and a full head-with-spine to C, where C is a base type. Anyway it cleaned up my stock identity proof for LF+extensions because instead of proving inductive lemmas one for each connective that show atomic-normal rules are admissible (which leads exactly to the "quadratic blowup" in terms of the number of connectives I'm always complaining about) I should just be proving an easy spine-concatenation lemma (which corresponds to the representation-language substitution that the twelf encoding does) and then just see that small spines have the right typing.
Tags: television, 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