October 22nd, 2003

beartato phd

(no subject)

So I was going back over the completeness proofs hunting for bugs, and found myself proving a couple little facts about substitution typing and things. It was kind of irritating at first, but the way it worked out is actually quite cute. The fact that I'm tracking the types of the things being substituted in a substantial way, in the very syntax of substitution means I can't just look up the answer in some book or paper (although if anyone listening knows of any work where [M/x] can have different values depending on the type ascribed to M, do let me know) So... it's a very small result -- it's just showing that one two-rule inference system is equivalent to another, that I can describe typing either by conses or snocs -- but it feels ever so mine, and it's a nice little clean result, and as far as me and mathematical work get along, that's the best feeling I know.
beartato phd

(no subject)

Good solid progress on research lately. Sitting down and working out a sufficiently general example revealed a lot about what variables are bound where, which helped me realize which things to hit with what substitutions, and from there hinted at what I now think is the right thing to induct on to glue together the two big pieces of machinery I've been trying to coax together.

It's gonna be one mofo of a mutual induction when I'm finished, I think, but I'm really quite optimistic about this tactic working. One of the three context zones in the main judgment has me a little mystified, however. I don't understand what it means, really. I just introduced it at one point to hold some variables that would have been free otherwise. I am compelled to hazily trust my intuition as to how to involve it in the proofs, but it seems to make everything go: it is the magic glue between the "outside world" and the variables of the unification problem.
beartato phd

(no subject)

Heh, nothing like giddy optimism to smoke out a counterexample. I'm going to have to be more clever. At least I found it pretty quickly this time...
beartato phd

(no subject)

Tired from lugging computer from office back home from home. Er, from wean. Somewhere between half a mile and a mile I think. Ate wendy's and faced off at Set with denorae. Losses 12-13, 12-13, 7-18. So close.

Meanwhile, I'm still waiting for my brain to spit out another idea. I'm totally convinced that the big picture is correct, but I've been totally convinced of so many falsehoods within this project alone that such statements are all but meaningless. Oh, math.