Email Gateway (Aug 22 2022 at 11:17): Email Gateway (Aug 22 2022 at 11:17):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
[This thread has become too volumnious to be followed in detail by a
casual bystander, so I try here with »one issue – one mail«.]
I did a glimpse at Alexander Krauss and Andreas Schropp, A mechanized
translation from higher-order logic to set theory. According to my
knowledge this had been the definite reference for taming overloading
and typedef until recently.
The critical passages are:
»Abstracting out unresolvable overloading would give rise to
dependent types.
This is no problem in the set-theoretic interpretation, but as
the overloading
elimination is currently implemented as a preprocessing step on the HOL
side,
it does not handle such overloading. This can be fixed by collapsing the
differ-
ent parts of the translation. However, to remove unresolvable
overloading from
type definitions while staying in HOL, one has to eliminate the type
definition
altogether, replacing it by its representing type together with a predicate.
It appears that this subtle issue was overlooked in all proof sketches
of con-
servativity of overloading so far. Practically, this form of overloading
seems to be quite rare. It does not occur in the main HOL
image, but a few
instances exist in the HOLCF development.«
»The fact that we uncovered a notable omission in all previous proofs of
conservativity of overloading shows that our approach of »implemented
semantics« is also useful for better understanding the logical system.«
Has anyone tried to apply proof extraction to a »inconsistent typedef«
example? According to my blurry understanding of the whole picture this
should fail then!? Maybe this would deserve a reference.
Cheers,
Florian
signature.asc
Last updated: Apr 27 2024 at 01:05 UTC