[opentheory-users] Troubleshooting an article reader

[Rob Arthan]

Mario,

On 16 Oct 2014, at 08:57, Mario Carneiro <di.gama at gmail.com> wrote:

> 
> 
> On Thu, Oct 16, 2014 at 3:43 AM, Ramana Kumar <ramana at member.fsf.org> wrote:
> On Thu, Oct 16, 2014 at 8:36 AM, Mario Carneiro <di.gama at gmail.com> wrote:
> Assuming that (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.
> 
> What if we relax that assumption?
> 
> 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 \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 \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 P = \r. ((rep (abs r)) = r, 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.

Well done! I wasn’t really expecting a rigorous proof.  The characterisations

    \a. (abs (rep a)) = \a.a
   P = \r. ((rep (abs r)) = r

that you have arrived at would provide a nice alternative to what HOL Light currently offers.
It would be really nice if there was a simple replacement within the typed lambda-calculus
for the HOL4 characterisation of a new type.

Regards,

Rob.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141016/e144799a/attachment.html>