Jason (jcreed) wrote,
Jason
jcreed

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
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 

  • 1 comment