[isabelle-dev] Typing problem in autogenerated axiom
Andreas Schropp
schropp at in.tum.de
Mon Nov 30 18:38:01 CET 2009
Dominique Unruh wrote:
> Dear all,
>
It looks like you only replied to me. ^^
> thanks for the answers.
>
> Let me summarize how I understood things, just to make clear I did not
> misunderstand anything:
>
> * Any constant is treated by the kernel as having no sort annotations.
> Although this leads to constants defined on more types than intended
> by the user, this does not lead to inconsistencies because we could
> always imagine that the constant has some arbitrary value on the extra
> types. (And arbitrary values exist anyway because even Pure already
> ensures non-emptiness of all types.)
>
> * Some axioms that are autogenerated by definitions have no sort
> annotations. E.g., less_eq has an axiom giving its definition for all
> types of the form 'a::{}=>'a::{}=>bool instead of only
> 'a::ord=>'a::ord=>Prop.
You mean 'a::ord=>'a::ord=>bool, right?
> Although such an axiom asserts things about
> less_eq for types outside the typeclass ord (for which the definition
> then usually also does not make much sense), this again does not do
> any harm to consistency because we this simply means that we fix a
> certain meaningless value for less_eq on types for which we would not
> have fixed any value at all otherwise.
>
Yeah, thats the way I understand it. As I mentioned, I even invent such
meaningless values in ZF, just to make my code more regular.
> This answers the question why there is no harm in removing sorts (at
> least from constants and definitions, not of course from class
> axioms). I am still wondering what the reasons for doing so are. At a
> first glance, at least, it would seem more natural to me if the
> constants and definitional axioms would have sort annotation. Also,
> the argument given by Florian ("definitions not only *can* ignore sort
> constraints, but *must* ignore sort constraints, otherwise this
> unfolding would not be possible in all situations.") does not convince
> me, because since in a normal proof, we would never even have an
> occurrence of a constant with the "wrong" sorts, so there is no need
> for a definition that allows unfolding in such situations. Also, as
> mentioned by Andreas, stripping sort constraints may make it much
> harder to interpret Isabelle/HOL in other logics (be it ZF as in
> Andreas case, or my experiments of translating Isabelle/HOL to Coq).
>
Let me put this into perspective, in the light of a forthcoming kernel
extension/modification:
in this kernel patch, all sort constaints and type class reasoning
steps are eliminated in proofterms on theorem boundaries, and
strip_sorted variants of the axioms are asserted on the proofterm side.
So what remains is a proof which sort and typeclass reasoning
internalized into the logic.
From my POV this is needed to translate HOL into logics not involving
Isabelle-style type classes.
BTW: I would like to hear about your experiences translating HOL->Coq.
How are you handling type class reasoning and overloading (I prefix an
unoverloading step) in your HOL->Coq translation? How do you handle the
interactions between Pure and HOL, or is this even a problem when
translating into another type theory?
I would actually like it if even axiomatized constants would get
topsorted declared types in consts.ML
The strangeness in the HOL->ZF translation regarding "fake constants" is
just a minor annoyance, where a Pure.undefined would help.
> Does anyone know what the reason for these design decisions are?
>
> Best,
> Dominique.
>
More information about the isabelle-dev
mailing list