*To*: Brian Huffman <huffman at in.tum.de>*Subject*: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue*From*: Makarius <makarius at sketis.net>*Date*: Tue, 23 Oct 2012 13:08:18 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAAMXsiYtk-FyKBTA05e=TnvAAgR1Hx=GLuC-Vt=GufP-6e=UMQ@mail.gmail.com>*References*: <1350924337.3906.54.camel@lapbroy33> <7588B83F-3006-45D4-ACBC-2EB0693E79BD@cam.ac.uk> <5085F0E7.9070207@nicta.com.au> <CAAMXsiYtk-FyKBTA05e=TnvAAgR1Hx=GLuC-Vt=GufP-6e=UMQ@mail.gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 23 Oct 2012, Brian Huffman wrote:

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.)

Makarius argues that it is reasonable to have low expectations of theconversion library. Yes, but this is no argument against making thelibrary exceed his low expectations of it.

Reading the ML source, we also find various low-level conversions in thm.ML: val beta_conversion: bool -> conv val eta_conversion: conv val eta_long_conversion: conv Their existence clearly indicates that conversions are not intended to work modulo beta- or eta-equivalence.

Furthermore, remember that we are only proposing to change the behaviorof rewr_conv on *non-beta-normal* input. I seriously doubt that anyexisting code actually depends on the current behavior of rewr_conv onnon-beta-normal cterms. In any case, it is easy enough to run the usualtest suite before committing a change.

This is good advice for *users* of Isabelle/ML libraries: Don't expecttoo much.

Makarius

**References**:**[isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue***From:*Peter Lammich

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

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

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

- Previous by Date: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
- Next by Date: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
- Previous by Thread: Re: [isabelle] mergesort
- Next by Thread: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
- Cl-isabelle-users October 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list