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
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and