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