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

[Michael Philip Ashley-Rollman]

Randy,

It is necessary to check that the complete derivation of "sub S T" 
cannot depend on any of the extra variables in the context. The simplist 
way to do this is to check that "var" does not appear hereditarily in any 
of the constructors of "sub". In this case that means it cannot appear in 
"sub" or "assm", as "sub" can contain "assm". Once you do that, you know 
that none of the extra variables in the context can appear in the 
derivation and thus they may be removed. One way to check this is to look 
at the subordination relations (Print.subord will show them) and verify 
that "var" is not subordinate to "sub". (Twelf does not print the 
transitive closure of the subordination relation, so it is necessary to 
recursively verify this)

Even if "var" is subordinate to "sub", it may be the case that "var" 
cannot appear in "sub". This comes up when a proof is done using 
assumptions of "var x -> sub x T" or something similar. By introducing 
these assumptions, one makes "var" subordinate to "sub", even if it can 
only appear in the derivation of "sub" in the presence of these 
assumptions. One could then deal with this situation by writting a proof 
that removes the dependence on these variables. Something like this:

(var X -> sub S T) -> sub S T -> type.

to show that "sub" cannot depend on "var".

As for more interesting cases, it is possible to construct a situation 
where "sub" may contain "var", but cannot contain any of the ones in the 
context. If, for example, we introduced a new construct "bound" and every 
usage of "var x" required "bound x" as well, then none of the "var"s 
occuring in the context could be used in "sub" and they could again be 
removed. I don't know if there is ever any reason to do something like 
this, but it is at least possible.
 	-Michael

On Wed, 18 May 2005, Randy Pollack wrote:

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