lambdacalculus recommended that I warn yinz guys that MATHBORINGS FOLLOWMight as well lj-cut, really.
I've had another slightly frustrating round of being nearly certain that a proof is there and right, but being uncertain as to how to overcome some silly technical difficulty.
My advisor meeting got put off by one day, so I have tomorrow to try to have something more useful to say on this particular topic. I had a very interesting little chat with
fancybred and neelk today, during which there came up a topic that I've been meaning to ask Frank about for a little while now anyway, because I think it has to do with his work with Brigitte Pientka and Alex Nanevski on contextual modal type theory.The itch in my side that prompted it was wanting to more carefully justify a shorthand I've been using a lot when proving substitution theorems. Normally a substitution theorem looks something like
if Γ ⊦ M : A and
Γ, x : A ⊦ N : B
then
Γ ⊦ [M/x]N : B
Not too messy, eh? But if your language has dependent types, then you have to substitute into the type, and also into the types of any variables in the context that mention x, resulting in a theorem like
if Γ ⊦ M : A and
Γ, x : A, Γ' ⊦ N : B
then
Γ, [M/x]Γ' ⊦ [M/x]N : [M/x]B
and also there are usually other judgments in the system, which need to admit their own substitution principle, and things get untidy rather quickly. What gets written sometimes is just
if Γ ⊦ M : A and
Γ, x : A, Γ' ⊦ J
then
Γ, [M/x]Γ ⊦ [M/x]J
where J is any judgment in the system. My habits lately have included (and I'm not at all certain I'm being original in doing this, but I might be for all I know) further absorbing into the "oh, you know what I mean" J the context to the right of the substituted variable, and simply writing
if Γ ⊦ M : A and
Γ, x : A ⊦ J
then
Γ ⊦ [M/x]J
with the understanding that J may be a bit of data like "Γ' ⊦ N : B" in which case the judgment Γ ⊦ [M/x]J is understood as meaning Γ, [M/x]Γ ⊦ [M/x]N : [M/x]B
Now I think that this perspective could be made a little more first-class by including these things into the syntax of the language properly by saying
J ::= Γ ⊦ M : A | Γ ⊦ A : type | ...
and then defining a judgment ok on these Js like
Γ,Γ' ⊦ M : A ------------------------- Γ ⊦ (Γ' ⊦ M : A) ok Γ,Γ' ⊦ A : type ------------------------- Γ ⊦ (Γ' ⊦ A : type) ok
moreover my guts tell me this is almost exactly the Nanevski-Pfenning-Pientka judgment "A valid[Γ]", except it's mere contextual truth instead of contextual validity.
The other payoff that seems possible is that this smells like it might yield a cleaner way to prove properties of hereditary substitution in twelf; the only technique I know of that works is all but a trade secret of Karl Crary and Daniel Lee, not because they are trying to keep it secret, but because it is time-consuming to explain.
---
Aw, poop inna biscuit. The hoped-for twelf trick doesn't seem to work that well. Right now I am getting internal Match raised internally in Twelf which is all kinds of no good.
