[opentheory-users] the Unwanted namespace

[Ramana Kumar]

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120113/97cb0176/attachment.html>