[opentheory-users] extending the standard library

[Ramana Kumar]

Hi Joe,

Sorry, but I feel like we are talking past each other at the moment. I
asked a
few questions in my last email which I don't think you addressed. Let me
address the concerns in your email first, then I will try to ask my
questions
again.

I agree with you about the value of underspecified constants in the standard
library. The source of value is that they put fewer constraints on readers,
thereby making theories based on the standard library more widely readable.

On creating theories in the HOL4 namespace, and depending on the hol-base
package: I see these as interim measures, with my desired goal being that
the
theorems and additional constants eventually all make it into the standard
namespace and depend on a nicely organised, unified, tree of packages. I
think
we probably agree on that goal, but I'm not sure. What do you say?

More generally, my goal is to put together OpenTheory packages that are so
compelling in their organisation and coverage, having taken theorems from
all
the existing HOL provers, that everyone wants to use them. I want to move
towards unification and away from fragmentation. I would be sad if
OpenTheory
simply becomes a mirror of the existing fragmentation and incompatibility
between the various theorem prover libraries today. Do you agree with this
more
general goal?

I would like to discuss how to achieve the HOL4-specific goal now, because I
think we have enough information to make progress on such a discussion
(enough
HOL4 packages are already created). (This is in response to "When the HOL4
theory packages are in place...".)

Now back to the questions from my previous email:

 - Do you agree with the three pieces of my solution to issue (2)? How do
you
   think responsibility for those tasks should be divided between readers
and
   creators?

 - I guess your response "I'm loath to totalize any of the constants..." was
   mainly to my suggested solution 0 to issue (3). That is a reasonable
   objection to solution 0.
   But:
   What do you think of solution 1, namely, providing multiple versions of
   constants that can be overspecified (in addition to the underspecified
   version), together with theorems relating them?

Thanks for bearing with me.

Cheers,
Ramana


On 12 May 2016 at 09:19, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Ramana,
>
> The problem I found with totalized constants is that the extra
> properties (e.g., inv 0 = 0) quickly infect a whole theory, which
> makes it useless for reading into an environment where the constant is
> defined differently.
>
> I'm loath to totalize any of the constants in the OpenTheory standard
> library just because there's an open world assumption that new
> environments might come along---beyond the HOL4, HOL Light and
> ProofPower theorem provers---with different policies on whether and
> how to totalize constants, but would still be able to read in current
> OpenTheory theories with underspecified constants.
>
> From your perspective as a theory creator I say just create theories
> in OpenTheory format that depend on your hol-base theory with its HOL4
> flavour of constants. Incidentally, you also asked about naming
> schemes in the hol-base theory, and I think it is set up perfectly
> with everything under a HOL4 namespace. Within that you can do
> whatever makes sense within a HOL4 context, which is the theory name
> followed by the symbol name. I do the same thing with HOL Light
> symbols, where there is no notion of theory name so it is even
> flatter.
>
> When the HOL4 theory packages are in place we can assess how feasible
> and desirable it is to remove their dependency on the hol-base
> package, so they can be read into any environment.
>
> Does that sound reasonable?
>
> Cheers,
>
> Joe
>
>
> On Tue, May 10, 2016 at 11:40 PM, Ramana Kumar <ramana at member.fsf.org>
> wrote:
> > Hi Joe,
> >
> > Thanks for your reply, which expresses the problem clearly.
> > There are the three issues with the standard theory library you listed,
> and
> > there are two perspectives to consider: reading an OpenTheory proof into
> a
> > theorem prover ("reading"), and creating an OpenTheory proof from a
> native
> > theory ("creating").
> >
> > Before considering issue (3), I want clarify what to do about the other
> two
> > issues from the creating perspective. For (1), there is no problem since
> the
> > extra constant can be ignored. For (2), I think some variation on your
> > solution
> > for the reading perspective could work. There are three pieces to the
> > solution:
> >
> >   A: Define the native version of the constant
> >   B: Prove an equation relating the native version to the OpenTheory
> version
> >   C: Use the theorem from B to rewrite theorems mentioning the native
> > constant
> >      into theorems mentioning only the OpenTheory version of the
> constant.
> >
> > How should responsibility for these tasks be divided between readers and
> > creators?  Initially, in the creator role, I am tempted to do only A, and
> > leave
> > B and C to the readers. I would expect you to eventually want all three
> to
> > be
> > done by the creator. I think there is some variation in how desirable C
> > might
> > be for different readers.
> >
> > Now for issue (3) from the creating perspective. I agree that it is a
> real
> > problem. I have a couple of ideas for possible solutions.
> >
> >   0. If the constant only has one natural candidate for how it might be
> >      overspecified, and all theorem provers overspecify it that way,
> simply
> > do
> >      so in the OpenTheory standard library too.
> >   1. Provide multiple versions of the constant in the standard library
> for
> > each
> >      of the natural ways of overspecifying it, and prove theorems
> relating
> > them
> >      (under appropriate conditions). Theorems that can be stated using
> the
> >      underspecified version should be (and readers should prefer these),
> but
> >      theorems that require overspecification can also be included (and
> > readers
> >      can handle these as they do issue (2)).
> >
> > Indeed, I think issue (3) is a variant of issue (2) where we cannot
> prove an
> > unconditional equation between different versions of the constants, but
> > where
> > we can still prove a conditional one.
> >
> > Do you have any other ideas for how to deal with these issues?
> >
> > Cheers,
> > Ramana
> >
> > On 10 May 2016 at 16:04, Joe Leslie-Hurd <joe at gilith.com> wrote:
> >>
> >> Hi Ramana,
> >>
> >> Despite the radio silence, I have been thinking about your question
> >> off and on since you asked it.
> >>
> >> The essential problem is that the different HOL theorem provers have
> >> slightly different definitions of fundamental constants, and so all
> >> the theories that are built on top of them are incompatible with other
> >> theorem provers.
> >>
> >> The standard theory library uploaded to the Gilith OpenTheory repo is
> >> my attempt at defining a common base that is implemented by all
> >> theorem provers, but it is imperfect in several ways:
> >>
> >> 1. It defines constants (such as Data.List.nub) that are not
> >> implemented in all the HOL theorem provers.
> >> 2. It defines constants (such as Data.List.zip) that exist in some HOL
> >> theorem provers with a different type.
> >> 3. It defines constants (such as Number.Real.inv) that are
> >> underspecified compared to their definitions in some HOL theorem
> >> provers.
> >>
> >> When we are reading an OpenTheory proof into a HOL theorem prover,
> >> then I don't believe any of these imperfections present any real
> >> obstacle:
> >>
> >> 1. If the proof relies on Data.List.nub, then this can simply be
> >> defined in the theorem prover. As you rightly say, such constants
> >> shouldn't really be part of the standard theory library, but I believe
> >> there are few enough of them that we can just add to the theorem
> >> provers.
> >> 2. In principle the OpenTheory interface in the HOL theorem prover
> >> would be able to translate constants from one type to an isomorphic
> >> one. One way to do this would be to define the OpenTheory versions of
> >> the constants in terms of the native ones and then "clean up" the
> >> resulting theorems by replacing the OpenTheory versions of the
> >> constants by expanding their definitions.
> >> 3. The OpenTheory proof will rely on fewer properties of such
> >> constants than are available in the native version, so the proof will
> >> go through.
> >>
> >> However, when creating OpenTheory proofs from native theories, then
> >> (3) appears to be a real problem. In my work I've tried to create a
> >> body of theories that rely only on the underspecified properties of
> >> such constants, but when I tried to translate some existing HOL Light
> >> proofs I found it hard going (I think I was trying to eliminate the
> >> saturated subtraction property: !n. 0 - n = 0).
> >>
> >> Do you have any ideas for how to overcome obstacle (3) so that we can
> >> start to build up a body of theories that can be read into any HOL
> >> theorem prover?
> >>
> >> Cheers,
> >>
> >> Joe
> >>
> >>
> > _______________________________________________
> > opentheory-users mailing list
> > opentheory-users at gilith.com
> > http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20160512/532f7882/attachment-0001.html>