Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue



Am 23/10/2012 07:38, schrieb Brian Huffman:
> Peter neatly stated the behavior that we all expect of conversions:
> 
> On Mon, 22 Oct 2012, Peter Lammich wrote:
>> > my understanding of conversions is, that "conv ct" either throws an
>> > exception or returns a theorem of the form "ct == ...".
> The current situation is this: Conv.rewr_conv only satisfies this
> property if a side-condition is met, namely that the input cterm must
> be already in beta-normal form.
> 
> The proposal is to modify rewr_conv to remove the side-condition: It
> should satisfy the basic property also for non-beta-normal cterms. On
> beta-normal cterms, rewr_conv should behave exactly as it did before.
> (Thomas's fix_conv would be one possible implementation of this
> proposal.)
> 
> So far, I haven't seen any good arguments against this change.

This is the essence: rewr_conv only satisfies

"A conversion is any function that maps a term t to a theorem |-t==u."
LCP, 1983

up to beta-equivalence. Since conversions are low-level proof methods which are
sensitive to the precise term structure, this is a wart that causes
non-modularity. This non-modularity only shows up (to refine Brian's analysis)
if the lhs of the rewrite rule has a free variable F in an applied position: F
t. This does not happen very often, but if it does, rewr_conv should still
behave nicely. It should do a non-normalizing instantiation followed by a
beta-normalization.

Tobias





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