[opentheory-users] new_specification

[Joe Leslie-Hurd]

Hi Rob,

I thought about your comments, and I take your point that even though
OpenTheory uses theory boundaries to enforce abstraction there are some
compelling reasons to support a definition principle such as your new
proposed mechanism that has better abstraction properties.

One of the design goals of OpenTheory is to have very precisely defined
standards, to maximize compatibility between tools that implement them, and
even though I can see the conceptual unity of your proposed "spec" command
it doesn't give precise enough instructions as to what the reader should do
for my taste.

Instead I have sketched out the spec for a draft "defineConstList" command

http://www.gilith.com/research/opentheory/article.html#defineConstListCommand

which is intended to match your proposed definition mechanism. Writers
using this command will almost certainly need to save the new constants to
the dictionary to build new terms, hence the need for another new command
to take apart lists:

http://www.gilith.com/research/opentheory/article.html#hdTlCommand

which is simply the inverse of cons.

I was reluctant before now to introduce any derived inference rules,
because another design goal of OpenTheory is to make it as simple as
possible to implement readers. However, I have convinced myself that this
is not an issue, because you can convert a version 6 article into a
logically equivalent version 5 article, and so a reader can always perform
this preprocessing step to avoid dealing with derived rules.

Following this new line of thinking, I have introduced some extra derived
rules

http://www.gilith.com/research/opentheory/article.html#symCommand
http://www.gilith.com/research/opentheory/article.html#transCommand
http://www.gilith.com/research/opentheory/article.html#proveHypCommand

that only depend on equality, and if writers choose to make use of them
will hopefully help to compress the resulting article files.

Please take a look at the new version 6 draft standard and let me know what
you think:

http://www.gilith.com/research/opentheory/article.html

Cheers,

Joe



On Sat, Mar 15, 2014 at 6:30 AM, Rob Arthan <rda at lemma-one.com> wrote:

> Joe,
>
> On 14 Mar 2014, at 21:35, Joe Leslie-Hurd <joe at gilith.com> wrote:
>
> I have thought about this some more, and I believe I have answered my own
> questions.
>
> 1. The proposed definition mechanism is not more expressive than
> new_definition, because it can be simulated by first defining c_1 = t_1,
> ..., c_n = t_n, instantiating the given theorem with the substitution
> [c_1/v_1, ..., c_n/v_n], and then using the definition theorems of the c_i
> to prove the hypotheses.
>
>
> It doesn't claim to be more expressive. What it is designed to offer is
> abstraction. The OpenTheory kernel has a different way of hiding
> representation details, but HOL4, HOL Light, ProofPower and the OpenTheory
> article format don't have that option.
>
> So I think the best thing is to keep the OpenTheory defineConst mechanism,
> and "compile" the proposed definition mechanism using the above scheme.
>
> But that means that the article format can't express the desired
> abstraction in a way that can be ported from one system to another. That
> seems like a major shortfall to me.
>
> My proposal for OpenTheory would be a new command, called "spec" say,
> which would actually provide the functionality of new_type, new_const,
> new_axiom, new_specification, gen_new_specification and new_type_definition
> in their HOL4, ProofPower and HOL Light guises. (Here gen_new_specification
> is the new principle from HOL Constant Definition Done Right.) "spec" would
> have four parameters:
>
> (1) a list of type name/arity pairs identifying new types to be introduced;
> (2) a list of constant name/type pairs identifying new constants to be
> introduced (the types in list (1) may appear in the types of these
> constants);
> (3) A list of sequents giving new axioms to be introduced (the types in
> list (1) and the constants in list (2) may appear in these sequence);
> (4) a list of objects, which constitute a "justification" for the new
> axiom.
>
> (4) would be empty for new_axiom, new_const or new_type. It would give the
> input theorem for new_specification, gen_new_specification and
> new_type_definition.
>
> A reader would analyse the parameters to figure out the best way to
> introduce the types and constants and so derive the required axioms.
> Recognising the various new_XYZ forms that I listed above and allowing for
> the differences between systems is easy and the reader can always fall back
> on a combination of new_type, new_const and new_axiom (or some kind of
> cheat).
>
> By making parameter (4) a list of objects, the "spec" command is general
> enough to accommodate any conceivable extension to the definitional
> mechanisms without changing the article format.
>
> The "spec" also makes the article format support higher levels of
> abstraction. For example, it would let the Gilith OpenTheory repo describe
> the types and constants in the base package (and others) in a way that is
> easy to import. The pair type for example, would be introduced by a spec
> command that introduces the type constructor "x", the constants ",", "fst"
> and "snd" and with the theorems that characterize the type in terms of
> these constants as the new axioms. The justification could be a string like
> "primitive" to hint to a reader that it should already have the types and
> constants. This declarative approach would make the base package a really
> useful resource (solving the problems discussed in this thread: [opentheory-users]
> Importing from the Gilith OpenTheory Repo<http://www.gilith.com/opentheory/mailing-list/2013-December/000329.html>
> ).
>
> 2. I think my simplification is bogus because defining the c_i in terms of
> c can fail because of the type variable condition.
>
> That is correct.
>
> Regards,
>
> Rob.
>
>
>
> _______________________________________________
> 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/20140316/878a813c/attachment.html>