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

We should not interpret Peter's original post as the question, "how
can I make my concrete application work"; rather, we should treat it
as a proposal to refine the behavior of the Isabelle conversion

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

So far, I haven't seen any good arguments against this change.

On Mon, Oct 22, 2012 at 9:27 PM, Makarius <makarius at> wrote:
> What happens here is that cv2 gets a cterm with beta redex, but it is rather
> well-known in Isabelle practice, that this can cause all kinds of troubles.
> So one could argue that the behaviour is correctly undefined.

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.

> Despite tons of manuals, which are often hard to keep in overview anyway,
> the real documentaion is the ML source:

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.

> If this is good or bad, or a "bug" is a completely different question.
> Further judgement would require careful studies how a change would impact
> existing application, and potential interaction with the Simplifier and the
> rule composition mechanisms (RS etc.)
> Seriously: I am now working a lot with Scala on the JVM platform.  What
> these industrial-strength guys usually do is to declare odd behaviour
> official rather quickly, because too many applications depend on it.

A quick search reveals that very little code within Isabelle depends
on rewr_conv; in particular, the simplifier and rule composition
mechanisms like RS predate the conversion library.

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.

> * The system knows alpha, beta, eta conversion.
> * Some layers use alpha (kernel).
> * Some layers use alpha + beta + eta (simplifier, resolution) but
>   normalize in different directions.

As I pointed out above, the existence of Thm.{beta,eta}_conversion
makes it clear that conversions do not use beta + eta.

> * Insisting too much in one way or the other causes trouble.
> * It is possible not to insist too much.
> * What is your concrete application anyway?

This is good advice for *users* of Isabelle/ML libraries: Don't expect
too much. For *developers* of Isabelle/ML libraries, this is no
argument against making improvements.

On 23/10/12 07:40, Lawrence Paulson wrote:
> This module was written long ago for a specific, internal purpose and was
> never intended for general use, so it's hard to say what is a bug and what
> isn't. The beauty of conversions is that they are highly modular, so you can
> write your own primitives that do exactly what you want.

If the module was never intended for general use, then we shouldn't be
so worried about breaking user code by modifying the module. I would
read this as an argument in favor of updating the conversion library
(or at least an argument against *not* updating it).

- Brian

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