[opentheory-users] extending the standard library

[Joe Leslie-Hurd]

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
>>
>>
>> On Sat, May 7, 2016 at 7:37 PM, Ramana Kumar <ramana at member.fsf.org>
>> wrote:
>> > Hi,
>> >
>> > I wanted to check if there was further interest in continuing this
>> > discussion from last month.
>> >
>> > The reason is that I am putting together a lot of OpenTheory packages
>> > based
>> > on theories made with the HOL theorem prover, and I would like it if
>> > this
>> > work could fit together nicely with other OpenTheory packages rather
>> > than
>> > living in its own universe (and perpetuating the problem of
>> > fragmentation).
>> >
>> > I think the theories I'm looking into (n-bit words, floating point
>> > numbers,
>> > real numbers, integers, rings, streams, quotients, ...) should all
>> > ultimately end up within the Standard Library. But to get there would I
>> > imagine require substantial coordination with the designers of the
>> > OpenTheory standard library, and other interested community members. I
>> > am
>> > also looking for technical advice on how to interface with the existing
>> > theories in the Gilith repo that seem to cover some of those topics.
>> >
>> > Cheers,
>> > Ramana
>> >
>> > On 13 April 2016 at 17:15, Ramana Kumar <ramana at member.fsf.org> wrote:
>> >>
>> >> Data.List.unzip works as a replacement for list.UNZIP. However, I will
>> >> hold back for a bit on making a new version of hol-base in case there
>> >> are
>> >> further improvements arising from this thread.
>> >>
>> >> On 13 April 2016 at 15:38, Konrad Slind <konrad.slind at gmail.com> wrote:
>> >>>
>> >>> Re: MAP2 in HOL4. This is an example of an underspecified function. I
>> >>> recall having
>> >>> to redefine map2 to completely specify it in order to get it through
>> >>> the
>> >>> HOL-->CakeML translator.
>> >>>
>> >>> So, presumably, different systems can and will define common partial
>> >>> functions differently, as
>> >>> either underspecified or completely specified. Is there an OpenTheory
>> >>> policy on this, for
>> >>> its standard library?
>> >>>
>> >>> Konrad.
>> >>>
>> >>>
>> >>> On Tue, Apr 12, 2016 at 11:56 PM, Ramana Kumar <ramana at member.fsf.org>
>> >>> wrote:
>> >>>>
>> >>>> It looks like list.ZIP can't be mapped to Data.List.zip because the
>> >>>> latter is curried. But I'm still looking into unzip.
>> >>>>
>> >>>> On 13 April 2016 at 13:56, Ramana Kumar <ramana at member.fsf.org>
>> >>>> wrote:
>> >>>>>
>> >>>>> The HOL4 base library has its own version of constants like
>> >>>>> Data.List.take and Number.Natural.- because it needs to prove
>> >>>>> theorems like:
>> >>>>>
>> >>>>> ⊦ length (list.TAKE n xs) = if n ≤ length xs then n else length xs
>> >>>>>
>> >>>>> ⊦ (∀m. arithmetic.- 0 m = 0) ∧
>> >>>>>   ∀m n.
>> >>>>>     arithmetic.- (suc m) n = if m < n then 0 else suc (arithmetic.-
>> >>>>> m
>> >>>>> n)
>> >>>>>
>> >>>>> I don't think these theorems are provable using the OpenTheory
>> >>>>> standard
>> >>>>> library versions of those constants.
>> >>>>>
>> >>>>> However, I don't know whether Data.List.unzip suffers from this
>> >>>>> problem. If not, then the HOL4 base package should be updated to use
>> >>>>> the
>> >>>>> standard library constant. It would be helpful if you could make a
>> >>>>> list of
>> >>>>> any other similar updates that should be made.
>> >>>>>
>> >>>>> I don't think the current OpenTheory standard library base contains
>> >>>>> theories that every HOL theorem prover supports. There are constants
>> >>>>> like
>> >>>>> Data.List.nub, for example, which are not supported by HOL4. I'm not
>> >>>>> entirely sure whether being the intersection of what every HOL
>> >>>>> theorem
>> >>>>> prover supports is a good goal, but if that is the rule it should at
>> >>>>> least
>> >>>>> be followed :)
>> >>>>>
>> >>>>> However, my question was not solely about the base package, but
>> >>>>> about
>> >>>>> the naming scheme for the standard library. If there are useful
>> >>>>> constants
>> >>>>> from other theorem provers (like, say, HOL4's list.GENLIST or
>> >>>>> list.MAP2), I
>> >>>>> think their name and characterising theorems should be fit into the
>> >>>>> OpenTheory namespace (Data.List, for example) in a standardised way,
>> >>>>> even if
>> >>>>> they don't make it into the base package itself. What do you think
>> >>>>> of that?
>> >>>>>
>> >>>>> I envision OpenTheory being used for the twin goals of portability
>> >>>>> (where being an intersection is good) and designing a rich, cleanly
>> >>>>> organised, useful standard library of HOL theorems (where being a
>> >>>>> union is
>> >>>>> good). These activities can happen simultaneously in different
>> >>>>> OpenTheory
>> >>>>> standard packages.
>> >>>>>
>> >>>>> On 13 April 2016 at 04:11, Joe Leslie-Hurd <joe at gilith.com> wrote:
>> >>>>>>
>> >>>>>> Hi Ramana,
>> >>>>>>
>> >>>>>> The intent is for the standard theory library to always be
>> >>>>>> evolving,
>> >>>>>> but slowly, because it's supposed to contain the base theories that
>> >>>>>> *every* HOL theorem prover supports.
>> >>>>>>
>> >>>>>> Looking through the theory I see a lot of defined constants that
>> >>>>>> also
>> >>>>>> occur in the OpenTheory standard library (e.g., list.UNZIP), and I
>> >>>>>> was
>> >>>>>> wondering why the HOL4 base theory has its own version?
>> >>>>>>
>> >>>>>> Cheers,
>> >>>>>>
>> >>>>>> Joe
>> >>>>>>
>> >>>>>> On Sun, Apr 10, 2016 at 1:54 PM, Ramana Kumar
>> >>>>>> <ramana at member.fsf.org>
>> >>>>>> wrote:
>> >>>>>> > Hi Joe,
>> >>>>>> >
>> >>>>>> > You will have seen that the HOL developers have uploaded a
>> >>>>>> > package
>> >>>>>> > called
>> >>>>>> > hol-base to the Gilith repo. The purpose of this package is
>> >>>>>> > twofold:
>> >>>>>> >
>> >>>>>> > It proves many useful theorems as found in the basic libraries of
>> >>>>>> > the HOL
>> >>>>>> > theorem prover.
>> >>>>>> > It serves to satisfy the assumptions of further theories
>> >>>>>> > developed
>> >>>>>> > in the
>> >>>>>> > HOL theorem prover, by proving those assumptions using only the
>> >>>>>> > theorems of
>> >>>>>> > the OpenTheory standard library base package.
>> >>>>>> >
>> >>>>>> > For purpose 1 in particular, it seems to me that many of the
>> >>>>>> > constants
>> >>>>>> > defined by hol-base would benefit from residing in an appropriate
>> >>>>>> > place in
>> >>>>>> > OpenTheory's namespace hierarchy, and indeed some of the proofs
>> >>>>>> > from
>> >>>>>> > hol-base might beneficially be moved into the base package
>> >>>>>> > itself.
>> >>>>>> > (Currently, all constants defined by hol-base are in their own
>> >>>>>> > namespace.)
>> >>>>>> >
>> >>>>>> > Is the design of the standard library still evolving, and is it
>> >>>>>> > open
>> >>>>>> > to
>> >>>>>> > extension? Would you be willing to copy over any useful-looking
>> >>>>>> > constants?
>> >>>>>> > And/or settle on some namespace decisions?
>> >>>>>> >
>> >>>>>> > Cheers,
>> >>>>>> > Ramana
>> >>>>>> >
>> >>>>>> > _______________________________________________
>> >>>>>> > opentheory-users mailing list
>> >>>>>> > opentheory-users at gilith.com
>> >>>>>> > http://www.gilith.com/opentheory/mailing-list
>> >>>>>> >
>> >>>>>>
>> >>>>>> _______________________________________________
>> >>>>>> opentheory-users mailing list
>> >>>>>> opentheory-users at gilith.com
>> >>>>>> http://www.gilith.com/opentheory/mailing-list
>> >>>>>
>> >>>>>
>> >>>>
>> >>>>
>> >>>> _______________________________________________
>> >>>> opentheory-users mailing list
>> >>>> opentheory-users at gilith.com
>> >>>> http://www.gilith.com/opentheory/mailing-list
>> >>>>
>> >>>
>> >>>
>> >>> _______________________________________________
>> >>> opentheory-users mailing list
>> >>> opentheory-users at gilith.com
>> >>> http://www.gilith.com/opentheory/mailing-list
>> >>>
>> >>
>> >
>> >
>> > _______________________________________________
>> > opentheory-users mailing list
>> > opentheory-users at gilith.com
>> > http://www.gilith.com/opentheory/mailing-list
>> >
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>