Email Gateway (Aug 22 2022 at 14:19): Email Gateway (Aug 22 2022 at 14:19):From: Rob Arthan <rda@lemma-one.com>
Ken,
Unfortunately, the paper by Ondrej Kuncar and Andrei Popescu that you cite gives
a description of the definitional mechanisms in HOL that is about 25 years out of date.
The new_specification mechanism allows implicit definitions and cannot be viewed
as a syntactic abbreviation mechanism. There is a proof of the conservativeness of a
(generalisation of) this mechanism in Andy Pitts’ Introduction to the HOL Logic (ref. [31]
in the paper). new_specification is implemented in all the "HOL-based provers” listed
in the paper.
Due to tinkering on my part around 2013, new_specification has been extended to relax
certain constraints on polymorphism that it imposed. The resulting gen_new_specification
has been proved conservative informally by me and formally in HOL4 by Ramana Kumar,
Magnus Myreen and Scott Owens (see their and my papers in ITP 2014 and/or JAR 56(3)).
gen_new_specification is implemented (to my knowledge) in HOL4, ProofPower and OpenTheory.
Regards,
Rob.
Email Gateway (Aug 22 2022 at 14:20):From: Ondřej Kunčar <kuncar@in.tum.de>
Hi Rob,
you are right that we mention only the plain definitions in HOL and not
the implicit ones, when we compare the definitional mechanism of HOL and
Isabelle/HOL. (If this what you meant; I assume you didn't mean to say
that the overloading in Isabelle is 25 years out of date).
I clearly remember that one of the early versions of our paper contained
the comment that the current HOL provers use the more powerful mechanism
that you mentioned but I guess that it was lost during later editing. We
will include it again into the journal version of the paper.
I wanted to comment on your statement that A. Pitts proved that
definitions in HOL are conservative. Such statements are always a little
bit puzzling to me because when you say conservative (without any
modifier), I always think that you mean the notion that "nothing new can
be proved if you extend your theory (by a definition)". I think a lot of
people (including me) think that this is THE conservativity. There is
also a notion of the model-theoretic conservativity that requires that
every model of the old theory can be expanded to a model of the new
theory. This is a stronger notion and implies the proof conservativity.
As far as I know, A. Pitts considers only a subset of all possible
models (so called standard models) in his proof and he only proves that
these models can be extended from the old to the new theory. But as far
as I know this does not imply the proof conservativity.
Best,
Ondrej
Last updated: Nov 21 2024 at 12:39 UTC