really isn't as problematic as I thought (though I'm keeping
my alternate formulation of irrelevance with blank terms in the
back of my mind still -- I'm not convinced it's useless, even though
Frank and Kaustuv seem to :) since leaving evars is a natural way
of 'solving' a unification and leaving inhabitation constraints
unanswered. Just a bit of quantifier smoke and mirrors if you ask
me, but it seems like the right thing to do.
The model theory midterm went decently. The questions were 3-choose-1
and 4-choose-2. Thankfully, there were 2 questions among the second 4
I had studied for, so I got them done in a reasonable amount of time.
Unfortunately, I didn't have any good leads on any of the remaining three,
so I dove into the second and produced an extremely hand-wavy proof.
Later, however, Rami emailed all of us saying that one was ill-posed
and required some other assumptions. So now we have to solve a different
problem for Monday as a take-home. It doesn't look like such a terribly
hard question given a whole weekend to do it, so I'm not really upset
Went over to WhizBang! to talk to Andrew but he was missing, for
once; apparently his second child was born. Better excuse than
mine ever were, I'm sure :)
Wrote up some notes about the join calculus translation.
I realize that I really have no idea how to prove completeness.
Oh well. Maybe staring at the pi calculus literature could help.
Maybe working on my actual semester project instead would
be a better idea.