[POPLmark] Re: [Provers] Re: adequacy

[Rob Simmons]

The two (understanding what a Twelf proof is and understanding coverage 
checking) are not necessarily unrelated. When I gave a talk to some 
other people here at Prinction where I attempted to give a short 
introduction to Twelf (the talk is linked from the Resources page of the 
Wiki), part of the explanation for what a total function was an 
explanation of *why* Twelf could decide that something was a total 
function.

For example, the problem you mention, which I dealt with myself (and 
which is discussed in the Wiki link I sent in response to Randy - a 
discussion which I going to update in light of these emails) is the 
/result /of the way Twelf knows that something is a total function - 
specifically, by checking that the outputs are totally unconstrained. 
Yes, there are ways (splitting or factoring on outputs) that would allow 
Twelf to accepct more functions as total, and if you haven't been 
presented with the problem (which the Twelf User's Guide currently does 
not discuss) it is quite mysterious. I wouldn't call it a bug, you could 
call it an unimplemented feature certainly, in all honesty I think it's 
primarily a result of limitations of the logic programming metaphor.

I've posted a summary of Randy's general question on the Wiki, I hope 
it's helpful - comments and revisions welcome.

Rob

Geoffrey A. Washburn wrote:

>On Thu, 5 May 2005, Kevin Watkins wrote:
>
>  
>
>>If I were just starting to learn Twelf, I would focus on understanding
>>what a Twelf proof (total function) is, first, before trying to
>>understand Twelf's totality checker, or the messages it generates.
>>    
>>
>
>	In my experience it is simply not possible to understand what
>  Twelf considers a proof without trying to understand the coverage
>  checker.  For example, if I write down the obvious total function
>  corresponding to a proof of about the type soundness of small step
>  semantics, it will fail because Twelf does not perform splitting when
>  considering output coverage.  Maybe this should be considered a bug in
>  Twelf; Karl has argued otherwise in the past.  The point is that just
>  writing down a total function in Twelf may not lead to a verifiable
>  proof unless you understand the coverage checker.
>
>  
>