[opentheory-users] the Unwanted namespace

[Joe Hurd]

Hi Ramana,

My preference would be that the theorem prover interface handles as
much as possible of the standardization during theory export and then
localization during theory import (the inverse operation). But I can
see that there might be some HOL4 specific theory information that
can't be reconstructed on theory import.

I wonder if you could achieve your goal by exporting an extra file
hol4.art declared in the package theory file

hol4-theory-file: hol4.art

that contained a version of the proof article file for the theory with
the HOL4 specific theory information you want to preserve?

Cheers,

Joe

> If we store terms in articles as-is and then clean tags up later (or not),
> then I imagine Opentheory repos would offer different versions of packages:
> either the raw one that might include prover-specific constants for some
> prover, or the cleaned up one with all tags removed. If you're lucky enough
> to be using the prover the package was made on, you get the specific
> version, otherwise you get the generic one.
> If tags are inferable, though, then there could be more options, tailoring a
> package to the prover you want to use it on.
> Does this sound right?
>
>
> On Mon, Dec 12, 2011 at 2:13 AM, Michael Norrish
> <Michael.Norrish at nicta.com.au> wrote:
>>
>> I think it’s clear that there’s no end of cruft that systems might like to
>> put into theory files.  Even the “names” field you mention below may vary
>> from system to system.  Given that, we need some generic way of stuffing
>> arbitrary, well-delimited strings into theory files.  I’d probably prefer
>> these strings to be inline, but it could also be done with associated files
>> if necessary.
>>
>> I like the default being the storage of everything.
>>
>>
>> Another example of a tag-like thing is the way we use K T x to store
>> arbitrary terms x in a theory so that the term can be referred to by the
>> LaTeX machinery we have.
>>
>> Michael
>>
>> On 08/12/11 21:32, Ramana Kumar wrote:
>> > Can we make a comprehensive list of the kind of stuff we might want to
>> > store in a theory package?
>> > I suspect there will be different recovery methods suitable for
>> > different kinds of data, and looking at the requirements will help see
>> > if and how opentheory might have to be modified or extended.
>> >
>> > - Tag-free theorems, definitions, low-level proofs.
>> > : already handled by article format
>> >
>> > - theory name and description and dependencies
>> > : already handled by theory package format
>> >
>> > - NUMERAL tags
>> > : reconstructible on reading?
>> >
>> > - Abbrev tags
>> >
>> > - Other tags? (Such as?)
>> > : An alternative approach might be to store terms in an article as-is
>> > (with tags) and then have different processing options for cleaning up
>> > an article like do-nothing, remove all tags, remove all of the
>> > following tags, or even possibly introduce tags for a specific prover
>> > (if they are inferable).
>> >
>> > - theorem names
>> > : could be stored in a separate file mapping names to statements?
>> >
>> > - automatic rewrites
>> > : could be stored in a separate file containing a list of theorems?
>> >
>> > - parsing and printing rules, and overloads
>> > : also could be in a separate file?
>> >
>> > - derived rules and other functionality associated with a theory
>> >   - tactics, provers/decision procedures
>> >   - syntax manipulation functions
>> >   - what else?
>> > : again, could be in a separate file of code, possibly using
>> > opentheory article format to interface with the required
>> > constants/theorems in the theory?
>> >
>> > - what else?
>> >
>> > At the moment it looks like almost everything could be handled by
>> > extra files that would be mentioned in a theory package but wouldn't
>> > interfere with article files in their current form. Only tag constants
>> > are a problem because they change the terms the article is dealing
>> > with.
>> >
>> > Are there examples of tags that are definitely not reconstructible if
>> > they are thrown away during cleanup?
>> >
>> >
>> > On Thu, Dec 8, 2011 at 9:50 AM, Michael Norrish
>> > <michael.norrish at nicta.com.au> wrote:
>> >> On 07/12/2011, at 20:01, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> >>
>> >>
>> >> It would be worth thinking about how to do all that with opentheory.
>> >> I wouldn't want to compromise the goal of storing prover-independent
>> >> theories without a good reason, though...
>> >>
>> >>
>> >> My concern is that the resulting system might forget things that can't
>> >> be
>> >> recovered.  Then it will never be usable as a theory storage mechanism.
>> >>   Is
>> >> it possible to create a faithful representation of what's there that
>> >> does
>> >> support getting back exactly what was put in, and to *then* work on
>> >> forgetting stuff that doesn't belong in theories meant for sharing with
>> >> other systems?
>> >>
>> >> Michael
>> >>
>> >> _______________________________________________
>> >> 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
>