<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Joe,<div><br></div><div>I am certainly happy with the new way of formulating defineTypeOp.</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div><div><br></div><div><div><div>On 16 Oct 2014, at 19:06, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">Hi Rob,<br><br>That is a very nice idea for a new_type_specification that is<br>compatible with the HOL Light and OpenTheory kernels: I like that it<br>doesn't define new constants with the new type operator, which always<br>seemed a bit inelegant to me.<br><br>In the immediate term, I wonder if we can now agree that the benefits<br>of Mario's new formulation of defineTypeOp are significant enough to<br>change the OpenTheory article spec as follows?<br><br><a href="http://www.gilith.com/research/opentheory/article.html#defineTypeOpCommand">http://www.gilith.com/research/opentheory/article.html#defineTypeOpCommand</a><br><br>I very much like the removal of hard-coded free variables (as opposed<br>to providing additional arguments to specify their name), and the<br>formulation simplifies the explanation of a future<br>new_type_specification article command. As before, the cost is that<br>readers have to implement both the old and new behaviors.<br><br>Cheers,<br><br>Joe<br><br>On Thu, Oct 16, 2014 at 9:22 AM, Rob Arthan <rda@lemma-one.com> wrote:<br><blockquote type="cite">Mario,<br><br>On 16 Oct 2014, at 08:36, Mario Carneiro <di.gama@gmail.com> wrote:<br><br><br>\a. (abs (rep a)) = \a. a<br><br>and similarly for the other:<br><br>P = \r. ((rep (abs r)) = r<br><br><br>In fact, you win today's star prize, because the above characterisations<br>give a workable way of formulating using only the typed lambda calculus<br>the type specification principle that is discussed in the HOL4<br>documentation,<br>but has never actually been implemented (despite having some really nice<br>properties).<br><br>As described in the HOL4 logic manual, the type specification principle<br>would not be acceptable in the HOL Light or OpenTheory kernels because<br>it depends on various non-primitive constants. The problem is to<br>express using only the typed lambda-calculus something equiprovable with<br>the following sequent, (*) say;<br><br>Gamma |- (?f. TypeDefn P f) => Q<br><br>where P and Q are closed terms satisfying certain conditions.<br>From this (and another theorem that is easy to express without<br>the logical connectives), you get a new type operator (alpha1, ... alphaN) op<br>whose defining property is q[alpha1, ... alphaN) op/alpha].<br>This generalises new_type_definition, which is the special case when<br>Gamma is empty and Q is ?f.TypeDefn P f.<br><br>Now ?f. TypeDefn p f is equivalent to ?abs.?rep. R P abs rep,<br>where R P abs rep asserts that abs is left-inverse to rep and that<br>rep is left-inverse to abs precisely where P holds (i.e., the properties<br>that new_type_definition gives you of the abstraction and<br>representation functions that HOL Light insists on defining for you).<br>So (*) is equivalent to (**):<br><br>Gamma |- (?abs.?rep. R P abs rep) => Q<br><br>By first-order logic, (**) is equiprovable with:<br><br>Gamma, P = (\r.rep(abs r) = r), (\a.abs(rep a)) = (\a.a) |- Q<br><br>I had been fiddling around with various not very nice<br>approximations to the above. With your improvements you get<br>something that is relatively easy to understand and is<br>simple enough to propose for serious consideration<br>as a more general replacement for new_type_definition.<br>(Note that it also satisfies you desiderata for naming things:<br>the names of rep and abs above are whatever the user chooses.)<br><br>Regards,<br><br>Rob.<br><br>_______________________________________________<br>opentheory-users mailing list<br>opentheory-users@gilith.com<br>http://www.gilith.com/opentheory/mailing-list<br><br></blockquote><br>_______________________________________________<br>opentheory-users mailing list<br>opentheory-users@gilith.com<br>http://www.gilith.com/opentheory/mailing-list<br></blockquote></div><br></div></body></html>