[opentheory-users] the Unwanted namespace

Joe Hurd joe at gilith.com
Sat Jan 14 13:19:03 UTC 2012


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
>



More information about the opentheory-users mailing list