[POPLmark] Experience report with Twelf

[Stephanie Weirich]

Thanks Michael, that clears up that issue. I don't need  
sub_strengthen or lookupClass_strengthen anymore.

Thanks,
Stephanie


On Aug 19, 2005, at 12:51 AM, Michael Philip Ashley-Rollman wrote:

>>>> lookupClass_strengthen :
>>>>   ({x:exp} lookupClass CT C (class C D FS (MT x)))
>>>>     -> lookupClass CT C (class C D FS (MT unit)) -> type.
>>>>
>>>> However, I think this is a case where strengthening is unavoidable.
>>>> The type exp is subordinate to the type methodTable, but since the
>>>> methodTable MT comes from the classTable CT (which does not  
>>>> depend on
>>>> x) in this case, it can't depend on x.
>>>>
>>>>
>>>>
>>>
>>> This could be a property of the system you're formalizing, not just
>>> the LF encoding.  That is, on paper, how do you *know* that the  
>>> class
>>> you get back doesn't mention some variable in the context?   
>>> Sometimes
>>> I've glossed over things like this on paper only to have Twelf point
>>> them out to me.
>>>
>>>
>>>
>> This issue didn't come up in either the Coq version of the proof  
>> (that I
>> did) or the Isabelle/HOL version
>> (that two grad students here at Penn did).
>>
>
> This issue does not really come up in the twelf proof either.  
> Rather than proving the lookupClass_strengthen or sub_strengthen  
> lemmas, you can simply substitute unit in for exp for  
> lookupClass_strengthen and any expression at all into  
> sub_strengthen. A term with type (exp -> subtyping CT C D) is  
> saying that for any expression, I can provide you with a proof of  
> (subtyping CT C D). Thus, by providing any term with type exp, we  
> may immediately get a derivation of (subtyping CT C D). Sometimes  
> substituting in terms that don't matter can confuses twelf a little  
> bit and it will give you an error like this:
>
> Typing ambiguous -- unresolved constraints
> C1 unit = C1 x;
> CT1 unit = CT1 x;
> CT1 unit = CT1 x;
> CT1 unit = CT1 x.
>
> In this case, providing the type of the term after substition  
> usually resolves the issue. Thus we may change the last rule of  
> narrowing_explist to this:
>
> -:  narrowing_explist WCT TL1 SB TL2 ->
>     sub_trans SB2 (SB1 unit : subtyping CT C D) SB4 ->
> %%    sub_strengthen SB1 SB3 ->
>      narrowing_exp WCT T1 SB T2 SB2 ->
>      narrowing_explist WCT
>      ([x][q] tl_cons (SB1 x) (TL1 x q) (T1 x q)) SB
>      ([x][q] tl_cons SB4 (TL2 x q) (T2 x q)).
>
> Othertimes Twelf is able to understand the substitution as in the  
> narrowing_bexp cases.
>     -Michael
>