<div dir="ltr">...which can also be written<br><br><div>P = \r. (\a. ((rep a) = r) = (= (abs r)))<br><br> (although using curried = that way is a bit strange)<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Oct 16, 2014 at 4:04 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:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">If you allow combining the two equations into one, there is also the option<br><div><br>P = \r. (\a. ((rep a) = r) = \a. ((abs r) = a))<br></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Oct 16, 2014 at 3:57 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:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><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>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></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.<br></span></div></div>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>