Re: [isabelle] [Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?
- To: OndÅej KunÄar <kuncar at in.tum.de>
- Subject: Re: [isabelle] [Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?
- From: Scott Owens <S.A.Owens at kent.ac.uk>
- Date: Sun, 23 Oct 2016 00:08:44 +0000
- Accept-language: en-US, en-GB
- Cc: "Prof. Andrew M. Pitts" <Andrew.Pitts at cl.cam.ac.uk>, Andrei Popescu <a.popescu at mdx.ac.uk>, "Prof. Thomas F. Melham" <thomas.melham at balliol.ox.ac.uk>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>, Roger Bishop Jones <rbj at rbjones.com>, "Prof. Peter B. Andrews" <andrews at cmu.edu>, Ken Kubota <mail at kenkubota.de>, Rob Arthan <rda at lemma-one.com>, HOL-info list <hol-info at lists.sourceforge.net>
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org> <email@example.com> <5E3CAC59-87D9-4C98-A58E-1B435A2F1E41@kenkubota.de> <B9CAE32E-026D-4ECB-B0BD-9D69ED2BAC69@lemma-one.com> <firstname.lastname@example.org>
- Thread-index: AQHSLFnQCRefVT6zQEumtY9jR+5wCaC0xYoAgABUOwA=
- Thread-topic: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?
I donât want to put words in Robâs mouth, as heâs far more knowledgable in this area than I am.
As far as I know, there is no mechanised conservativity proof for HOLâs recent generalised constant specification mechanism. (Here Iâm in agreement that âconservativityâ without any other modification should refer to the proof theoretic notion, and thatâs what I mean here.) Rob certainly has a pencil-and-paper proof. Ramana, Rob, Magnus, and I (although mostly Ramana) proved the soundness of a HOL Light-style logical system, including the generalised constant specification mechanism that Rob refers to (and also designed) and type definition mechanism, with respect to a standard model of higher-order logic. I worked on a mechanised conservativity proof for the definition mechanism for a bit two years ago but got distracted and havenât returned to it. I think it would be a suitable student project, but Iâm not convinced that itâs really that interesting â I wouldnât be bothered by a sound and consistent definition principle that allowed one to prove more things.
> On 2016/10/22, at 20:07, OndÅej KunÄar <kuncar at in.tum.de> wrote:
> 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.
> On 10/22/2016 12:59 PM, Rob Arthan wrote:
>> 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. 
>> 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.
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, SlashDot.org! http://sdm.link/slashdot
> hol-info mailing list
> hol-info at lists.sourceforge.net
This archive was generated by a fusion of
Pipermail (Mailman edition) and