Re: [isabelle] Strange eta-expansion on induction



On Fri, Mar 2, 2012 at 9:28 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> Eta-expansion is an intrinsic part of the higher-order unification algorithm. Following each unification by an eta-contraction step would be inefficient, and equally arbitrary. The “problem" that must be “fixed" is any code that cannot exist with this basic fact of nature.

By this reasoning, the Isabelle simplifier is a "problem" that must be "fixed".

The simplifier does not respect eta-equivalence of terms. I don't
think I would want one that did.

- Brian


> On 1 Mar 2012, at 20:15, Brian Huffman wrote:
>
>> I have complained at length about this issue before. See this thread
>> from August of last year:
>>
>> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-August/msg00080.html
>> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-August/msg00089.html
>>
>> To summarize: In my opinion, having a proof kernel that does
>> eta-expansion willy-nilly is an embarrassment; I also have similar
>> feelings about the "eta-contract" option in the pretty-printer, which
>> our eta-expanding kernel makes necessary.
>>
>> Unfortunately, fixing the problem properly would require modifying the
>> unification code in the kernel, which hardly anybody understands. It
>> would be hard to get anyone to trust a modified version of it.
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.