Re: [isabelle] Let and commutative rewrite rules



Dear Tobias,

I do not like the situation "We do not fully understand what is going on, so better not change anything", because this effectively freezes the code as it currently is with no way to ever improve it. I am pretty sure that my change would have hardly any effect on the existing proofs (although I would have to test this hypothesis). Still, I agree with your decision for another reason. The let_simp simproc is already fairly inefficient when there are nested let expressions such as

let x = foo a b c in
let y = bar a b c in
let z = fbr a b c in
f x x y y z z

because when the simproc triggers on the let for x (i.e., it has already looked at the lets for y and z), it inlines the x in the body and invokes the simplifier on the body

let y = bar a b c in
let z = fbr a b c in
f (foo a b c) (foo a b c) y y z z

Thus, the simplifier goes over the whole body again, which triggers the let_simp for the y once more (it has already triggered for this let binding before it triggered for the outer let). In summary, let_simp's runtime is exponential in the depth of let nestings.

Now, if we were to add another normalisation check for the abstracted body, this would increase the base of the exponential by one. The non-termination problem occurs rarely (the main reason is probably that commutativity rules are not in the simpset by default), so it probably does not justify slowing the simplifier down (although it took me a while to understand where the non-termination came from).

I consider the exponential running time more of a problem. (Note that this term remains linear in size if everything is inlined, so there is no exponential blow-up in term size due to the inlining.) I digged a bit through the history of the simproc, but I was not able to find any more information on what Norbert's case really is. Is there anyone who remembers?

Andreas

PS: For completeness, here's the changed simproc with the additional normalisation test for Isabelle2015-RC3.

lemma Let_folded2: "â f x â g x; g â g' â â Let x f â Let x g'"
by (simp add: Let_def)

simproc_setup let_simp ("Let x f") = {*
let
  val (f_Let_unfold, x_Let_unfold) =
    let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold}
    in apply2 (Thm.cterm_of @{context}) (f, x) end
  val (f_Let_folded2, x_Let_folded2) =
    let val [(_ $ (f $ x) $ _), _] = Thm.prems_of @{thm Let_folded2}
    in apply2 (Thm.cterm_of @{context}) (f, x) end;
  val (g_Let_folded2, g'_Let_folded2) =
    let val [_, (_ $ g $ g')] = Thm.prems_of @{thm Let_folded2}
    in apply2 (Thm.cterm_of @{context}) (g, g') end;
  fun count_loose (Bound i) k = if i >= k then 1 else 0
    | count_loose (s $ t) k = count_loose s k + count_loose t k
    | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
    | count_loose _ _ = 0;
  fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) =
    (case t of
      Abs (_, _, t') => count_loose t' 0 <= 1
    | _ => true);
in
  fn _ => fn ctxt => fn ct =>
    if is_trivial_let (Thm.term_of ct)
    then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
    else
      let (*Norbert Schirmer's case*)
        val t = Thm.term_of ct;
        val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
      in
        Option.map (hd o Variable.export ctxt' ctxt o single)
(case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *)
            if is_Free x orelse is_Bound x orelse is_Const x
            then SOME @{thm Let_def}
            else
              let
                val n = case f of (Abs (x, _, _)) => x | _ => "x";
                val cx = Thm.cterm_of ctxt x;
                val xT = Thm.typ_of_cterm cx;
                val cf = Thm.cterm_of ctxt f;
                val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
                val (_ $ _ $ g) = Thm.prop_of fx_g;
                val g' = abstract_over (x, g);
                val abs_g'= Abs (n, xT, g');
              in
                if g aconv g' then
                  let
                    val rl =
cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold};
                  in SOME (rl OF [fx_g]) end
else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g') then
                  NONE (*avoid identity conversion*)
                else
                  (* normalise the abstracted body, as the abstraction might have
                     un-normalised the body, e.g., ordered rewriting,
                     simprocs with syntactic checks, ... *)
                  let
                    val g'_normal = Simplifier.rewrite ctxt (Thm.cterm_of ctxt abs_g');
                    val (_ $ _ $ g'_normalised) = Thm.prop_of g'_normal;
                  in
if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract g'_normalised) then
                      NONE
                    else
                      let
                        val g'x = abs_g' $ x;
val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
                        val rl =
                          @{thm Let_folded2} |> cterm_instantiate
                            [(f_Let_folded2, Thm.cterm_of ctxt f),
                             (x_Let_folded2, cx),
                             (g_Let_folded2, Thm.cterm_of ctxt abs_g'),
                             (g'_Let_folded2, Thm.cterm_of ctxt g'_normalised)];
                      in SOME (rl OF [Thm.transitive fx_g g_g'x, g'_normal])
                      end
                  end
              end
          | _ => NONE)
      end
end
*}


On 06/05/15 11:38, Tobias Nipkow wrote:
Dear Andreas,

Thank you for your thoughts, but I would rather not change the current setup. I don't
really understand Norbert's code and I don't want to add further bits to it. Moreover, the
problem seems to crop up very rarely. If we were to modify the code, I would expect one of
two results: it hardly has any effect or it breaks a lot of proofs. In both cases I would
want to leave well alone.

Tobias

PS I have recently made some similar change also in HOL and am thinking about undoing it
for some of the reasons above.

On 05/05/2015 10:23, Andreas Lochbihler wrote:
Dear Tobias,

I had another look at the implementation of let_simp. I guess that one might be
able to change the let simproc fairly easily. The idea is as follows. For
non-trivial lets (at least two occurrences of the bound variable and the bound
term is not atomic), the let simproc inlines the bound term in the body,
normalises the result with the simplifier and the current simpset, and then
replaces all the remaining occurrences of the bound term in the normalised term
with the bound variable.

There is already a check whether the new body is alpha-beta-eta-equivalent to
the old body. In that case, the simproc aborts with NONE. Now, the interaction
can occur only if the abstracted body is no longer in normal form (although it
is with the bound term inlined)*. Thus, it would make sense to normalise the
abstracted body again and check for equivalence with the original body.

When I add this additional check, the looping in my example disappears. What do
you think?

Best,
Andreas

* This may happen due to term order as in my case, but I imagine that simprocs
like NO_MATCH equally cause trouble here.


On 04/05/15 16:36, Tobias Nipkow wrote:
Dear Andreas,

I was not aware of this interaction but it does not surprise me - the let
simproc is magic
- but you can switch it off. I have no idea if it can be modified to avoid this
interaction in the first place. That sounds like a time sink.

Tobias

On 04/05/2015 15:59, Andreas Lochbihler wrote:
Dear experts on rewriting,

I have a problem with let bindings and commutative rewrite rules. Here is an
example and my understanding of what is happening.

lemma "(let pb = foobar b in f pb (Îpad. g (pb * pad :: int))) = bar"
apply(simp add: mult.commute)

1. mult.commute rewrites pb * pad into pad * pb, because pad seems to be smaller
than pb in the term order that the simplifier uses.
2. The let simproc determines that pb occurs more than once in the body, so it
does not inline the let binding. Instead, it simplifies the body with knowledge
pb = foobar b. Thus, the simplifier now sees pad * foobar b. Since "foobar b" is
smaller than pad in the term order, commutativity kicks in again and we get
foobar b * pad. Now, the simproc abstracts the simplified body over foobar b
again and replaces it with pb. So we are back to pb * pad. Thus, the simplifier
goes over the whole term again and we are back at step 1.

In my understanding so far, commutative rewrite rules are safe (in the sense of
termination) to add to the simplifier, but the let simproc interferes with this.
Is this a known problem? Can the let simproc be somehow changed to avoid this?

Best,
Andreas







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