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

[Karl Crary]

Randy,

The precise statement you want to check is that var is not subordinate 
to sub.

The notion of subordination is formalized in Roberto Virga's thesis.  In 
principle, the subordination relation is pre-specified, and you're only 
allowed to form the function space A -> B when A is subordinate to B.  
In practice, to spare the programmer the trouble of specifying the 
relation, Twelf takes it to be the smallest relation such that all 
functions spaces that appear are well-formed.

You can obtain this relation in one of two ways.  First, you can simply 
ask Twelf to report it, using Print.subord.  Second, if you want to do 
it by hand, look through your development for function spaces and 
compute the transitive closure.

Anticipating your next question, Twelf's estimate of the subordination 
relation can change as it processes more input.  (That is, whenever 
Twelf sees a function space, it adds a new edge if it's not there.)  You 
can prevent it from doing so by freezing a type family (using %freeze), 
which makes it impossible to add new subordinate types.  Twelf also 
freezes families automatically whenever it uses non-subordination 
information to make sure its decisions are not later invalidated.  (So, 
in your case, you would want to freeze sub, to make sure that var 
doesn't later become subordinate to it, except you don't have tok, 
because it would happen automatically anyway.)

    -- Karl


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
> > >
> > >
>_______________________________________________
>Poplmark mailing list
>Poplmark at lists.seas.upenn.edu
>http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
>
>  
>