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



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

This is the point where one would have to start thinking and looking carefully. So far the attitudes towards the system were far too crude, to even think of it.


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

Misunderstanding again. Wrong attitudes towards "good or bad", "wrong or right", "broken or fixed" means. The incident is rather trivial here, but the general principles are very important.


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.

Here you also need to look at the history. When the type conv was re-introduced after a long time, I merely tried to re-integrate many existing functions into the framework, without assuming too much semantics behind it.


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

It will be probably not too hard, but such things have to be done with the proper attitude and care. The "bug" fraction on this thread lacks that.


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

I never said said. You should get your expectations right and realistic. The code base is generally not so bad, but after > 25 years it defines it own rules. So as long as you are standing outside somewhere and pretending to know how to "fix" it, it wont work for you.


	Makarius






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