[opentheory-users] Troubleshooting an article reader

[Mario Carneiro]

...which can also be written

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

(although using curried = that way is a bit strange)

On Thu, Oct 16, 2014 at 4:04 AM, Mario Carneiro <di.gama at gmail.com> wrote:

> If you allow combining the two equations into one, there is also the option
>
> P = \r. (\a. ((rep a) = r) = \a. ((abs r) = a))
>
> On Thu, Oct 16, 2014 at 3:57 AM, 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.
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141016/caad20bc/attachment.html>