Jason (jcreed) wrote,
Jason
jcreed

Major twelf success just now --- the structure of this proof was like 5 stages to begin with, and ever since starting to formalize it each stage has a nasty habit of needing to be dividing up into zillions of little substages. Moreover, it is hard to tell in advance which substage will be the really hard one that I need to think the most about. So I just blunder forward a lot of the time, fixing problems whenever they come up. This means the structure of my approach to, say, stage X looks like this:

Think about substage X1. Code something up. It works! Hooray.
Think about substage X2. Code something up. It works! Hooray.
Think about substage X3. Code something up. It doesn't work.
Hmm.
Realize a conceptual mistake.
Change something about the way X3 is coded up.
Oh! That requires a change to substage X1 and everything after it.
Think about how to fix substage X1. Code something up. It works! Hooray.
Think about how to fix substage X2. Code something up. It works! Hooray.
Think about how to fix substage X3. Code something up. It works! Hooray.
Think about how to fix substage X4. Code something up. It doesn't work.
Hmm.
Change something about the way X4 is coded up. Oh! That requires a change to substage X1.
Think about substage X1. Code something up. It works! Hooray.
etc.

Nonetheless in the course of working on it, I have gotten a little better global view of how the proof needs to work. I succeeded in identifying a few hurdles that definitely are relatively nontrivial, important things to formalize right.

One of them, one that I solved a while ago, was the need for a certain lock-and-key trick. This is the thing I've been rather inappropriately calling "hackbindery", after the name, "hackbind", of a block declaration in Karl's code, whose very naming indicated his displeasure at certain aspects of its working that I think I've successfully cleaned up. The going has been incredibly more pleasant ever since I figured that out.

The other major turning point is kind of hard to describe without describing the guts of the proof, but hell, probably nobody is reading this entry but future-me anyhow. In order to translate lambdas I need to separate out which terms are "new" vs. which are "old", and this distinction arises in two ways; one in a type-free way, which dances a complicated dance involving which variables actually occur in certain terms. The other way arises out of the typing judgment, and there the "new" variables are precisely those that exist at the new modal world introduced by the lambda. I need to essentially show that these notions coincide. The trouble is, they don't. Typeless-new terms are always typed-new --- if they contain any new-world variables, then the term must come from the new world in order to be well-typed. But Typeless-old terms may be typed-new or typed-old. Fortunately I can jigger around the typing derivation so that there at least exists some derivation I can construct in which they're now typed-old.


Anyway I've said it before, but it sure competes well with the excitement of watching like action movies or sports or whatever when I'm all furiously typin' away, and I'm all getting towards the conclusion that I've been working for for a few days, and I'm like "Server OK? Server OK? Server OK? SERVER OK!" The huge, huge mess of coverage errors that I had to wade through to get to that point only made the partial victory sweeter. I'm particularly happy that I found a solution to a nasty termination problem, via tossing in another argument to one typing definition that tracks its "shape".

---

But now I think I've set a new personal record for most complicated set of coverage errors elicited by a single %total declaration: 180 missing cases, for a total of 2,638 lines of error messages.
Tags: twelf, work
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 2 comments