<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Mario,<div><br><div><div>On 16 Oct 2014, at 08:36, Mario Carneiro <<a href="mailto:di.gama@gmail.com">di.gama@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr"><br><div class="gmail_extra"><div class="gmail_quote"><div><span>\a. (abs (rep a)) = \a. a</span><br><br></div><div>and similarly for the other:<br><br><span>P = \r. ((rep (abs r)) = r</span><br><br></div></div></div></div></blockquote><br></div><div>In fact, you win today’s star prize, because the above characterisations</div><div>give a workable way of formulating using only the typed lambda calculus</div><div>the type specification principle that is discussed in the HOL4 documentation,</div><div>but has never actually been implemented (despite having some really nice properties).</div><div><br></div><div>As described in the HOL4 logic manual, the type specification principle</div><div>would not be acceptable in the HOL Light or OpenTheory kernels because</div><div>it depends on various non-primitive constants. The problem is to</div><div>express using only the typed lambda-calculus something equiprovable with</div><div>the following sequent, (*) say;</div><div><br></div><div>Gamma |- (?f. TypeDefn P f) => Q</div><div><br></div><div>where P and Q are closed terms satisfying certain conditions.</div><div>From this (and another theorem that is easy to express without</div><div>the logical connectives), you get a new type operator (alpha1, … alphaN) op</div><div>whose defining property is q[alpha1, … alphaN) op/alpha].</div><div>This generalises new_type_definition, which is the special case when</div><div>Gamma is empty and Q is ?f.TypeDefn P f.</div><div><br></div><div>Now ?f. TypeDefn p f is equivalent to ?abs.?rep. R P abs rep,</div><div>where R P abs rep asserts that abs is left-inverse to rep and that</div><div>rep is left-inverse to abs precisely where P holds (i.e., the properties</div><div>that new_type_definition gives you of the abstraction and</div><div>representation functions that HOL Light insists on defining for you).</div><div>So (*) is equivalent to (**):</div><div><br></div><div>Gamma |- (?abs.?rep. R P abs rep) => Q</div><div><br></div><div>By first-order logic, (**) is equiprovable with:</div><div><br></div><div>Gamma, P = (\r.rep(abs r) = r), (\a.abs(rep a)) = (\a.a) |- Q</div><div><br></div></div><div>I had been fiddling around with various not very nice</div><div>approximations to the above. With your improvements you get</div><div>something that is relatively easy to understand and is</div><div>simple enough to propose for serious consideration</div><div>as a more general replacement for new_type_definition.</div><div>(Note that it also satisfies you desiderata for naming things:</div><div>the names of rep and abs above are whatever the user chooses.)</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div></body></html>