[POPLmark] How to believe the Twelf proof of 1a

[Randy Pollack]

Michael,

I was looking for a precise statement that I can syntactically check.
Do you mean I must check that "var" (also "assm_var") doesn't appear
literally in any constructor of "sub"?  Or that "var" doesn't appear
hereditarily in any constructor of "sub"?  Might the syntactic check
which Twelf uses be symantically incomplete?  

You say "in this case ..."; are there more interesting cases?  What
other issues can arise?  Where is this explained in detail in the
Twelf literature?

Randy
--
Michael Philip Ashley-Rollman writes:
 > Randy,
 > 
 > In order to believe the theorem, you want to believe that the world 
 > containing bind is just as good as the world for which the adequacy 
 > theorem holds. In this case, you need only believe that none of the extra 
 > assumptions in the world cannot appear in the output of the theorem. In 
 > this case, since sub S T cannot contain var x within it somewhere and it 
 > cannot contain assm_var d dv in it anywhere, you may conclude that the 
 > derivation of sub S T produced by the trans theorem can only contain x and 
 > d. Thus, if we were to remove all of the extra assumptions from the world, 
 > we would still have a valid derivation of sub S T in the world
 > some {t:tp} block {x:tp} {d:assm x t}.
 >  	-Michael
 > 
 > On Wed, 18 May 2005, Randy Pollack wrote:
 > 
 > > Karl,
 > >
 > > I'm still unclear on the meaning of "var".  Suppose I want to believe
 > > that the main formal result in file 1a.elf proves the intended
 > > property of the intended object system.
 > >
 > >  %block bind  : some {t:tp}
 > > 		 block {x:tp} {dv:var x} {d:assm x t} {thm:assm_var d dv}.
 > >  trans : sub S Q -> sub Q T -> sub S T -> type.
 > >  %mode trans +X1 +X2 -X3.
 > >  - : trans D1 D2 D3 <- trans* _ _ nat_eq_ D1 D2 D3.
 > >  %worlds (bind) (trans _ _ _).
 > >  %total {} (trans _ _ _).
 > >
 > > (You've pointed out that the world (bind) is part of the statement of
 > > this result.)
 > >
 > > I must believe some adequacy theorem about "sub" and "assm", which in
 > > this case resides in the world
 > >
 > >  some {t:tp} block {x:tp} {d:assm x t}
 > >
 > > (As we have discussed, by choosing the world of the adequacy theorem,
 > > I specify which of the possible object systems I'm interested in.
 > > E.g. one could consider the world
 > >
 > >  some {t:tp -> tp} block {x:tp} {d:assm x (t x)}  %% funny binding
 > >
 > > but that is not the intended object system.)
 > >
 > > QUESTION: what do I need to believe about "var" in order to believe
 > > the theorem?  "var" doesn't show up in the declaration of "sub" or in
 > > the adequacy theorem, but it does appear in the statement of "trans".
 > >
 > > Randy
 > > _______________________________________________
 > > Poplmark mailing list
 > > Poplmark at lists.seas.upenn.edu
 > > http://lists.seas.upenn.edu/mailman/listinfo/poplmark
 > >
 > >