[opentheory-users] Finalizing version 6 of the article file format standard

[Joe Leslie-Hurd]

Hi Rob,

I've taken some steps in preparation for an announcement:

1. Version 6 of the article spec is now available at the following URLs:

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

2. The changes between version 5 and version 6 are highlighted at

http://www.gilith.com/research/opentheory/article-5-6.html

3. A version of the standard theory library using version 6 articles
is now on the public OpenTheory repo:

http://opentheory.gilith.com/?pkg=base-1.169

You should be able to upgrade by simply typing

opentheory update
opentheory upgrade

using the latest version of the opentheory tool.

If you would like to write some text describing the changes in the
article spec then I'll make an official announcement on this list.

Cheers,

Joe

On Wed, Nov 19, 2014 at 1:02 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:
> Hi Rob,
>
> I am indeed working on the Haskell export functionality and I thought
> that the theorem metadata might help with this, but for now I plan on
> using theory files to record the necessary information.
>
> The only plan I have for recording the changes is to keep a copy of
> the current article spec (with highlighting) to make it easy to see
> what has changed. I would then remove the highlighting in the official
> version 6 spec so we can start with a blank slate when discussing
> possible changes toward a version 7.
>
> I would be happy to take you up on your offer to collect the reasons
> for changing the format. How do you think it is best to record the
> reasons for the changes? As part of an announcement on this mailing
> list? As annotations in the version of the article spec with the
> changes highlighted?
>
> Cheers,
>
> Joe
>
> On Wed, Nov 19, 2014 at 12:12 PM, Rob Arthan <rda at lemma-one.com> wrote:
>> Joe,
>>
>> I think it is prudent to leave the metadata proposal in the test lab for
>> now.
>> Is there ongoing work on interchange with Haskell? If part of your plan
>> for the metadata was to do with mapping to the modularity features of other
>> languages, then maybe that would be something that could be usefully
>> addressed
>> with some support from the theory format as well as or instead of the
>> article format.
>>
>> I have no objection to version 6 going live. Do you think it would be worth
>> recording the reasons for the changes somewhere? I don’t mind volunteering
>> to collect the information.
>>
>> Thanks for all your hard work on this.
>>
>> Regards,
>>
>> Rob.
>>
>>
>> On 19 Nov 2014, at 18:45, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>
>> With the demise of the theorem metadata proposal there are no open
>> features for version 6 of the article spec, and so I move to close the
>> spec and make it official. At this point any future development will
>> be for version 7 of the article spec.
>>
>> If I don't hear any objections I'll do this in the next day or so and
>> release a version of the standard theory library in version 6 format.
>>
>> Cheers,
>>
>> Joe
>>
>> On Wed, Nov 5, 2014 at 11:23 PM, Mario Carneiro <di.gama at gmail.com> wrote:
>>
>> Oh wow, that's a pretty direct derivation of extensionality from my version
>> of defineTypeOp. I stand corrected; certainly it's not desirable to have a
>> "conservative extension" allow the derivation of an axiom before its
>> introduction. And I guess that the next best thing if you want to maintain
>> conservativity is exactly your version of the axiom.
>>
>> Mario
>>
>> On Thu, Nov 6, 2014 at 2:16 AM, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>
>>
>> Hi Mario,
>>
>> As you say, extensionality is an axiom of the system, but the use of
>> it is explicitly tracked. For example, you can see which theorems in
>> bool theory depend on it using the following command:
>>
>> opentheory info --theory --show-assumptions --show-derivations bool
>>
>> If defineTypeOp produced this:
>>
>> ⊦ p = (\r. rep (abs r) = r)  (1)
>>
>> then you could apply appThm, betaConv and absThm to get:
>>
>> ⊦ (\r. p r) = (\r. rep (abs r) = r)  (2)
>>
>> and then sym and trans using (1) and (2) to get
>>
>> ⊦ (\r. p r) = p  (3)
>>
>> which is an untracked application of extensionality for any non-empty
>> predicate p. It seemed more elegant to reformulate the theorem to
>> avoid this possibility.
>>
>> Cheers,
>>
>> Joe
>>
>> On Wed, Nov 5, 2014 at 10:45 PM, Mario Carneiro <di.gama at gmail.com> wrote:
>>
>> I was aware that equation (1) is stronger than (2) without
>> extensionality,
>> but I'm curious why this is a problem, since it is an axiom of the
>> system
>> and doesn't require proof. Any v5 proof that starts with (2) can easily
>> be
>> rebuilt to use (1), while conversely for a v6 proof there are very few
>> theorems that follow from (1) but not (2) in the absence of
>> extensionality
>> (mostly trivial restatements of (1) itself), and I expect that any proof
>> that starts from (1) will immediately wrap it with appThm, upon which
>> point
>> it will again be equivalent to (2).
>>
>> Mario
>>
>> On Thu, Nov 6, 2014 at 1:31 AM, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>
>>
>> Now that there is a release of the opentheory tool for processing
>> version 6 articles, and I am sitting on a release of the standard
>> theory library that uses version 6 articles, I'd like to finalize
>> version 6 of the article file format standard, which is currently in
>> draft mode:
>>
>> http://www.gilith.com/research/opentheory/article.html
>>
>> The commands that are new in version 6 are highlighted in yellow and
>> the command with changed semantics (defineTypeOp) is highlighted in
>> red. We have discussed the changes on this list, so there shouldn't be
>> any surprises in store.
>>
>> Actually, there is one minor change that hasn't been discussed before.
>> During implementation work on defineTypeOp I discovered that one of
>> Mario's proposed theorems
>>
>> ⊦ p = (\r. rep (abs r) = r)  (1)
>>
>> required the axiom of extensionality to be logically equivalent to the
>> same theorem produced by version 5 of defineTypeOp:
>>
>> ⊦ p r = (rep (abs r) = r)  (2)
>>
>> Although it would be theoretically possible to invoke the axiom of
>> extensionality to convert between the two versions of defineTypeOp, I
>> thought it was more elegant to reformulate theorem (1)
>> by eta-expanding p:
>>
>> ⊦ (\r. rep (abs r) = r) = \r. p r  (3)
>>
>> [I also flipped the LHS and RHS so that theorem (3) has a pleasing
>> similarity to the other theorem produced by defineTypeOp.] Now theorem
>> (3) is logically equivalent to theorem (2) without requiring the axiom
>> of extensionality, and retains the desirable property of having no
>> free term variables.
>>
>> Anyway, there are no other "brown bag updates" to the standard, and
>> I'd like to finalize it so we can start using it for real work.
>>
>> Does anybody have any objections or last-minute additions?
>>
>> Cheers,
>>
>> Joe
>>
>> _______________________________________________
>> 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
>>