[POPLmark] Adequacy for LF

[Robert Harper]

Whatever the form of the argument, it is all part of the adequacy 
theorem, and is of no concern for the formalization.  I might add that 
ANY encoding in ANY logical framework requires an adequacy theorem to 
justify its validity/relevance to the problem at hand.  I regard the 
adequacy of our formalization to be self-evident to anyone with 
"ordinary skill" in the field (as they say in patent law here).

It would be a trivial matter to reformulate the operational semantics 
using "evaluation contexts", but doing so would only crapify the 
presentation for no good reason whatsoever.  I have been through two 
complete formalizations of Standard ML, one of which is in the very 
last stages of being completely formalized in Twelf.  I believe that I 
know the best way to do this for all purposes, and that's to use SOS.  
Any other approach is only more complicated, and affords nothing, 
particularly when you want to do machine-checked proof.  Yes, we could 
do it, and, no, it would not be substantially more complicated, but it 
would annoy us and take up valuable time that is much better spent 
working on real issues in logical frameworks (such as how to 
incorporate more interesting structural congruences, a point where a 
*legitimate* criticism of our solution can be levelled.)

This again brings us back to the fundamental point that it is entirely 
spurious and counterproductive to insist on some a priori formulation 
of a language if your goal is to mechanize its metatheory.  You have to 
listen to the logical framework, as it were, and take its advice in 
guiding you towards a better way to formulate your system.  We learned 
this lesson many years ago when we first invented LF --- the exercise 
of formalizing a logic in LF does wonders for the logic.

Bob

On May 2, 2005, at 8:54 PM, Benjamin Pierce wrote:

>> If we agree on this definition, then it is very easy to see that the
>> encoding is adequate.  (Easier than usual, actually.)  Observe that, 
>> in the
>> object language, there is exactly one derivation for derivable 
>> evaluation
>> judgements.  Similarly, for any E1 and E2, there is at most one 
>> canonical
>> form belonging to "step E1 E2".  Thus, the object language and its 
>> encoding
>> are in isomorphism provided they agree on the judgement's graph.  We 
>> believe
>> the latter is obvious (although to be rigorous would require an 
>> inductive
>> proof).
>
> I think this is where we're really disagreeing.  To me, this "obvious" 
> fact
> is not obvious.
>
> I believe it's TRUE, of course, but that belief is based on an argument
> (i.e., that the evaluation-context-style and the direct-style 
> operational
> semantics of Fsub are the same relation) that IMHO is of the same 
> order of
> trickiness as the other properties that are being formalized in the
> challenge.  (For example, the proofs of this equivalence that I've seen
> always invoke a "unique decomposition" lemma, saying that any
> non-normal-form t can be factored as t=E[t'] for exactly one E and 
> t'."  The
> proof of this property is not very hard, but it's not trivial either.)
>
> Regards,
>
>     - Benjamin
>
>
>
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark