[opentheory-users] the Unwanted namespace

[Ramana Kumar]

Yes I think the theory package *-file lines allow any kind of file to be
attached to a package.

The only reason to have an extra hol4 article file is tags like Abbrev and
NUMERAL. Everything else, as I mentioned before, can be done separately
from the article.
So, to summarise what's required on the HOL4 side to package an existing
HOL4 theory:
1. Log the article without translating any constants to Unwanted.id (i.e.
don't mark anything as tags); maybe just put constants that won't be in a
standard namespace into the HOL4 namespace.
2. In the theory package file, name the article from step 1 as the
hol4-theory-file. Probably post-process it with the opentheory tool too.
3. Create a new copy of the article file from step 1, and rename the tags
(I'm thinking just a search+replace taking "HOL4.Abbrev" -> "Unwanted.id",
etc. might be enough, right?), then postprocess with opentheory to remove
them.
4. Name the article from step 3 as the main article in the package.
5. For any additional information (theorem names, exported rewrites, etc.,
which should probably also be recorded in step 1) add appropriate extra
hol4-something-files to the package.

Unfortunately, that still doesn't solve the problem when a tag shows up not
fully applied (like in a point-free term).

On Sat, Jan 14, 2012 at 8:32 PM, Michael Norrish <
michael.norrish at nicta.com.au> wrote:

> This would be my preference (thus my "associated files if necessary").  I
> don't know if everything HOL4-ish could necessarily be encoded in an "art"
> file though.  Presumably, files mentioned in the package could contain
> other stuff.
>
> Michael
>
> On 15/01/2012, at 0:19, Joe Hurd <joe at gilith.com> wrote:
>
> > 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
> >>
> >
> > _______________________________________________
> > 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120114/f8fb6a5e/attachment.htm>