[POPLmark] Experience report with Twelf
Stephanie Weirich
sweirich at cis.upenn.edu
Thu Aug 18 20:07:06 EDT 2005
Dan Licata wrote:
>>A side note: I don't think that this is exactly the law of the
>>excluded middle. I think it says something like "at least one of the
>>'subtyping' and 'notsubtyping' judgments are derivable."
>>
>>
>
>The law of the excluded middle is usually phrased as (A or not(A)),
>which corresponds in this instance to the phrase in quotes above.
>
>
>
<rest snipped>
I think we dis agree on what the definition of not-subtype should be,
and that makes all of the difference.
You propose the following definition:
> not-subtyping-contra : not-subtyping A B
> <- (subtyping A B -> false).
where I define non-subtyping without relation to the subtyping
judgement. (Technically, a judgments that
holds when two types aren't subtypes of one another.) That's why the
subtyping-exclusive lemma
>>subtyping-exclusive: subtyping A B -> not-subtyping A B -> false ->
>>type.
>>
>>
is necessary to make it clear that both of these judgments can't hold.
(It is true by definition for your version.).
However, I prefer my definition of not-subtyping because with your
definition, the excluded middle lemma
is not provable in Twelf---there is no LF canonical form of type
(subtyping A B -> false). Even though I
originally wanted to assert the decidablity of subtyping, since
subtyping *is* in fact decidable, it makes sense for me to
assert it in a way that could eventually be proven in Twelf.
>>
>>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).
--Stephanie
More information about the Poplmark
mailing list