Jason (jcreed) wrote,

I'm pretty convinced now that the reason hereditary substitution is hard to prove in twelf is not just because the context changes from the assumptions of the theorem to the conclusion; it's not that the function you apply to the context is genuinely partial recursive and not merely substitutive in the representation language; it's that the function you apply to the context is parameterized by one of the inputs of the theorem, namely the term that's being substituted for the variable. You can't make a worlds declaration that says "okay, in each block I have (among other things) a proof that the type of this hypothesis gets translated this other type when you substitute N (by which I mean the term being substituted in this application of the theorem!)" I can sort of do this for an individual block, but I can't think of a good way of constraining all the blocks in a regular world to have the same N.
Tags: twelf

  • (no subject)

    Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

  • (no subject)

    Did some personal archaeology. Helped a little with laundry. Threw some chicken, onions, tomato, stock, peppers in the slow cooker and hopefully…

  • (no subject)

    Dinner with akiva and dannel at nuevo portal in carroll gardens. Ate a pile of chicken stew and rice and beans and maduros, good times. I do miss…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment