[POPLmark] how to believe a twelf proof

[Randy Pollack]

Karl,

There must still be a part of the story that hasn't been explained.

Consider the declarations I sent earlier for subject reduction,
following your note "How to believe a Twelf proof".

"sr" also checks in the following extended context

  false : type.

  %block fblock : block {d:false}.
  %worlds (bind | fblock) (sr _ _ _).
  %total D (sr D _ _).

This seems to say that "sr" is total in any world (bind | fblock).
This is a world extending "bind" with possible extra entries
{d:false}.  This doesn't say how you could ever get an assumption
{d:false} in the context, but if you could, you would be able to prove
that every term has object type "o" (just for example).  That is,
{d:false} cannot occur (directly) in any canonical form proof of
judgements "red" or "of", but may occur indirectly, by theorems which
may not have been stated.  How does Twelf check that some assumption
in an extended context may not contribute indirectly, by yet unproved
theorems, to some canonical form of interest?

(Of course, subject reduction actually does hold in any context
containing false, as any judgement holds in such a context, but I
think the example shows what my question is.)

So Karl's explanation

 > Since the extra assumptions in H cannot appear in M3, it follows that:
 > e(X)(G) |- M3 : sub e(X)(S) e(X)(U)

doesn't seem to explain the situation to me.  Some part of the story
is still missing.

Randy
--
Karl Crary writes:
 > 
 > This is a good question, but I believe I answered it fully in an earlier 
 > message, which I am attaching.
 > 
 >     -- Karl
 > 
 > 
 > Randy Pollack wrote:
 > 
 > >Karl,
 > >
 > >Okay, "sr" checks in every world for which the representations of
 > >"tp", "tm", "of" and "red" are adequate, so we can read "sr" as a
 > >theorem about the intended object language typing and reduction
 > >relations.  Am I right that this is your point?
 > >
 > >Similarly, Frank's proof of type preservation for cbv evaluation,
 > >which hapens to check in a closed world, also checks in every world
 > >for which the representations of "tp", "tm", "of" and "eval" are
 > >adequate, so we can read "sr" as a theorem about the intended object
 > >language typing and evaluation relations.
 > >
 > >Now we are getting to my real question.  In your PoplMark solution,
 > >file 1a.elf, the lemma "trans" does NOT check in every world in which
 > >"tp", "assm" and "sub" are adequate representations of the intended
 > >object language.  I believe you agreed with me in previous email that
 > >the world in which "tp", "assm" and "sub" are adequate representations
 > >is generated by the block
 > >
 > >  %block pure : some {t:tp} block {x:tp} {d:assm x t}.
 > >
 > >But "trans" also requires some other assumptions about "var" and
 > >"assm_var" to check.  So, why should I consider "trans" as a theorem
 > >about the intended object language subtyping relation???
 > >
 > >Randy
 > >
 > >  
 > >
 > Message-ID: <42711EF4.3090705 at cs.cmu.edu>
 > Date: Thu, 28 Apr 2005 13:35:48 -0400
 > From: Karl Crary <crary at cs.cmu.edu>
 > User-Agent: Mozilla Thunderbird 1.0.2 (Windows/20050317)
 > X-Accept-Language: en-us, en
 > MIME-Version: 1.0
 > To: Randy Pollack <rap at inf.ed.ac.uk>
 > CC: POPLmark challenge <poplmark at lists.seas.upenn.edu>
 > Subject: Re: Twelf solution: adequacy theorem
 > References: <17007.62262.879485.499046 at slim.inf.ed.ac.uk>	<42701373.8030107 at cs.cmu.edu> <200504281648.j3SGmMPc020395 at sorrel.inf.ed.ac.uk>
 > In-Reply-To: <200504281648.j3SGmMPc020395 at sorrel.inf.ed.ac.uk>
 > Content-Type: text/plain; charset=ISO-8859-1; format=flowed
 > Content-Transfer-Encoding: 7bit
 > 
 > You are correct, the answer is no.  To be totally precise, let me give 
 > the complete story for "+".
 > 
 > Suppose G |- S <: T and G |- T <: U.
 > 
 > By adequacy, we have canonical forms M1 and M2 such that
 > e(X)(G) |- M1 : sub e(X)(S) e(X)(T)
 > and
 > e(X)(G) |- M2 : sub e(X)(T) e(X)(U)
 > 
 > Then, there exists some LF context H that contains e(X)(G) and is made 
 > up of blocks described by bind.  Moreover, any assumptions in H that are 
 > not in e(X)(G) cannot appear in any canonical form belonging to type 
 > family sub.  (H is obtained from e(X)(G) by adding var and assm_var 
 > assumptions.)
 > 
 > It follows that:
 > H |- M1 : sub e(X)(S) e(X)(T)
 > and
 > H |- M2 : sub e(X)(T) e(X)(U)
 > 
 > By the totality of trans, it follows that there exists canonical M3 such 
 > that
 > H |- M3 : sub e(X)(S) e(X)(U)
 > 
 > Since the extra assumptions in H cannot appear in M3, it follows that:
 > e(X)(G) |- M3 : sub e(X)(S) e(X)(U)
 > 
 > By adequacy, G |- S <: U.
 > 
 > 
 > Now, consider "++".  In this case, there does not in general exist a 
 > corresponding context H made up of bind blocks.  The extra bindings are 
 > a red herring; ignore them.  The problem is that
 > 
 >     x:tp, d:assm x (T[x]) ...
 > 
 > is not a valid bind block when T[x] mentions x, because in that the 
 > definition of bind
 > 
 >     %block bind : some {t:tp} block {x:tp}{d:assm x t} ...
 > 
 > the variable t is not in the scope of x.  If you wanted to support this, 
 > you would need a block like:
 > 
 >     %block f-bound-bind : some {t:tp -> tp} block {x:tp} {d:assm x (t 
 > x)} ...
 > 
 > Since you cannot come up with H, the argument cannot proceed.
 > 
 >     -- Karl > 
 > 
 > Randy Pollack wrote:
 > 
 > >Dear Karl,
 > >
 > >Thanks for your efforts to explain the situation to me.  My (first)
 > >question is still the relationship between the adequacy theorem for a
 > >particular LF representation of an object system, and the
 > >interpretation of total logic programs over that LF signature as
 > >proofs of inductive properties of the object system.
 > >
 > >
 > >Here is a detailed question.  Consider Fsub without the "forall" type
 > >constructor, as my question arises already without it.
 > >
 > >
 > >Let Sig_sub be the valid LF signature:
 > >
 > >  tp : type.  %name tp T.
 > >  top     : tp.
 > >  arrow   : tp -> tp -> tp.
 > >  assm : tp -> tp -> type.  %% subtyping assumptions
 > >  sub  : tp -> tp -> type.  %% subtyping judgement
 > >  sub_top         : sub _ top.
 > >  sub_refl        : sub X X
 > >		     <- assm X _.
 > >  sub_trans       : sub X T
 > >		     <- assm X U
 > >		     <- sub U T.
 > >  sub_arrow       : sub (arrow S1 S2) (arrow T1 T2)
 > >		     <- sub T1 S1
 > >		     <- sub S2 T2.
 > >
 > >
 > >Define a translation from the (informal) types of Fsub with free type
 > >variables in the list X = [x1, ..., xn], to LF terms:
 > >
 > >  e(X): x         |-> x  (if x in X)
 > >        top       |-> top
 > >        S->T      |-> arrow (e(X)(S)) (e(X)(T))
 > >
 > >e(X) is a bijection between types of Fsub with free type variables in
 > >the list X, and LF canonical forms of LF type "tp" in the LF context
 > >Sig_sub, x1:tp, ..., xn:tp.
 > >
 > >
 > >The translation is extended to contexts
 > >
 > >(+)  e(X)(x<:U, Gam) |-> x:tp, d:assm x (e(X)(U)), e(X,x)(Gam)
 > >                                             (x not in X)
 > >
 > >There is a bijection between well-formed Fsub contexts, Gam, and
 > >well-typed LF contexts  Sig_sub, e(nil)(Gam).
 > >
 > >
 > >The adequacy theorem claims there is a bijection between derivable
 > >Fsub judgements  Gam |- S <: T  and canonical LF terms M satisfying
 > >
 > >   Sig_sub, e(nil)(Gam) |- M : sub (e(Gam)(S)) (e(Gam)(T))
 > >
 > >(By "e(Gam)(S)" I mean something like e(map fst Gam)(S).)
 > >
 > >
 > >In the CMU solution to POPLmark, you show that 
 > >
 > >  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 _ _ _).
 > >
 > >which is interpreted as meaning
 > >
 > >   "S<:Q => Q<:T => S<:T holds in Fsub".
 > >
 > >This interpretation must depend on some relationship between Fsub and
 > >the LF context Sig_sub, namely the adequacy theorem.
 > >
 > >
 > >But there is an alternative to the translation of contexts (+) above:
 > >
 > >(++)  e(X)(x<:U, Gam) |-> x:tp, d:assm x (e(X,x)(U)), e(X,x)(Gam)
 > >                                             ^^        (x not in X)
 > >
 > >This is not the informal intention of system Fsub, but it does
 > >correspond adequately to some informal system with a more liberal
 > >notion of context.  Call this system Gsub.
 > >
 > >
 > >QUESTION: Do you claim that the fact "trans" is total in world "bind"
 > >implies transitivity of subtyping for the informal system Gsub?
 > >
 > >I guess the answer is "no".  So what is it about (+) that means
 > >totality of a program for trans implies Fsub is transitive, and about
 > >(++) such that totality of a program for trans does not imply Gsub is
 > >transitive?
 > >
 > >In case you answer "yes" to my question, notice that Fsub and Gsub
 > >have some dfferent properties that are observable as inductive
 > >theorems.
 > >
 > >Randy
 > >
 > >
 > >  
 > >
 >