<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:57, 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"><br><div class="gmail_quote">On Thu, Oct 16, 2014 at 3:43 AM, Ramana Kumar <span dir="ltr"><<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><span class="">On Thu, Oct 16, 2014 at 8:36 AM, Mario Carneiro <span dir="ltr"><<a href="mailto:di.gama@gmail.com" target="_blank">di.gama@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><div>Assuming that <span> (abs (rep a)) = a is the shortest way to express the original claim, I am confident that this is the symbol-minimal quantified version of the same formula.<span><font color="#888888"><br></font></span></span></div></div></div></div></blockquote><div><br></div></span><div>What if we relax that assumption?<br></div></div></div></div></blockquote></div><br></div><div class="gmail_extra">A really clever way of writing it would be (abs o. rep) = id , where o. is composition, but I don't think there is a way to write that using primitives any simpler than <span>\a. (abs (rep a)) = \a. a. You already know that it needs a dummy variable (because things like (abs rep) are not well-typed, and you have no other objects using type A), needs to have abs and rep, and needs to be quantified over the dummy variable (once on each side of the equality so the types match), which gives \a. (abs (rep a)) = \a. ? where the a on the left may possibly be somewhere else. There really aren't too many options that are even shorter than </span><span>\a. (abs (rep a)) = \a. a, so I would say that it's probably as good as it gets. For the other one, there are no spare symbols in </span><span><span>P = \r. ((rep (abs r)) = r</span>, so again I think that's minimal. A rigorous proof would need an enumeration of all smaller formulas, but it's hard to see anything well-typed that is any smaller than this and still uses all the essential elements.</span></div></div></blockquote><br></div></div><div>Well done! I wasn’t really expecting a rigorous proof. The characterisations</div><div><br></div><div> \a. (abs (rep a)) = \a.a</div><div> P = \r. ((rep (abs r)) = r</div><div><br></div><div>that you have arrived at would provide a nice alternative to what HOL Light currently offers.</div><div>It would be really nice if there was a simple replacement within the typed lambda-calculus</div><div>for the HOL4 characterisation of a new type.</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div></body></html>