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



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 == ...". Here is a minimal example where rewr_conv actually returns a theorem that does not satisfy this condition, and thus, a subsequent then_conv fails unexpectedly.


definition "I x \<equiv> x"
definition "A f x \<equiv> f x"


ML_val {*
 let
   open Conv

   val cv1 = fun_conv (rewr_conv @{thm I_def})
   val cv2 = rewr_conv (@{thm A_def[symmetric]})
 in
   (cv1 then_conv cv2) @{cterm "I (\<lambda>s::bool. s) True"}
 end

 (*
*** exception THM 0 raised (line 835 of "thm.ML"):
*** transitive: middle term
*** I (\<lambda>s\<Colon>bool. s) True \<equiv> True
*** True \<equiv> A (\<lambda>s\<Colon>bool. s) True
 *)

*}


The reason is, that the term after applying cv1 is not beta-reduced, and
cv2 returns a theorem with a beta-reduced left-hand side. The exception
is thrown when then_conv tries to put the two theorems together.

(ML *raises* exceptions, other languages like Java *throw* them.)

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.


I consider this a bug, because it is nowhere documented that the user of conversions has to take care of beta-normalization manually.

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


(* single rewrite step, cf. REWR_CONV in HOL *)

fun rewr_conv rule ct =
  let
    val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
    val lhs = Thm.lhs_of rule1;
    val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
  in
    Drule.instantiate_normalize (Thm.match (lhs, ct)) rule2
      handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
  end;

This says excplitly that your resulting rule instance will be produced by Drule.instantiate_normalize, and thus in beta-normal form. So you loose if you try to make a plain then_conv step based on something that is not in beta-normal form.

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.) I can't say much on the spot, apart from quoting the well-known "Mahabharata" software development principle: "Dharma eva hato hanti / Dharmo rakshati rakshitah". In other words, it might be easier to change your expectation about what the system should do for you.

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.


 What is the status of beta-equality within Isabelle?
   Alternative 1) beta-equivalent terms are considered equal: then_conv
should just work modulo beta-equivalence
   Alternative 2) They are not considered equal on this low-level:
rewr_conv should be forced to return an equal term.

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

* 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?


	Makarius





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