Re: [isabelle] Common sub-expression elimination



The let_simp simproc in HOL.thy already does some sort of CSE in special cases. Try, e.g.,

  lemma "P (let x = f y in x + x + f y)"
    apply simp

CSE can be great for specific applications (like approximation), but the current state with let is a mess. If you have a clear idea how to control CSE (and deal with let), I'd be all in favour of cleaning up let_simp.

Best,
Andreas

On 19/01/16 12:18, Manuel Eberl wrote:
Yes, you can, of course, always do that, and maybe this is also the best way to do it.

I was thinking of having a "Let"-like construct on the expression level and then using
that to eliminate the subexpressions. Or with approximate, the way you would eliminate a
common sub-expression would be to rewrite something like "pi + pi â {0..10}" to "âx. x =
pi â x + x â {0..10}", which causes approximate to approximate pi, store the bounds it
finds in some context under the name "x", and re-uses these bounds whenever it encounters
"x" from then on.

However, I suppose you could also achieve this by first rewriting it to "let x = pi in x +
x â {0..10}" with the CSE tool and then rewriting that to "âx. x = pi â x + x â {0..10}"
outside the CSE tool.

This might be a nicer solution.

Manuel


On 19/01/16 11:48, Ramana Kumar wrote:
I don't think any user-supplied theorem theorem should be necessary. If
a term tm[s] contains multiple occurrences of a subterm s, then (\x.
tm[x]) s = tm is always provable. There may already be a let-like
construct that is syntactic sugar for that lambda abstraction.

On 19 January 2016 at 21:30, Manuel Eberl <eberlm at in.tum.de
<mailto:eberlm at in.tum.de>> wrote:

    I was wondering whether there is any work on common subexpression
    elimination, ideally in a generic fashion, similar to the
    Reification tool by Amine Chaieb.

    This would, of course, be interesting in general, but parcitularly
    for the approximation decision procedure. I believe that CSE is
    complex enough to make a generic mechanism for it interesting.


    If something like this does not exist, it might make a nice student
    project. What I am envisioning is something that
    â takes a HOL term
    â returns one or all subterms that occur more than once
    â ideally, provides some mechanism for "pulling out" all occurrences
    of a common subexpression, e.g. by putting them in a "let"-like
    construct (e.g. by a user-supplied theorem that says that one can
    "pull out" terms like this)
    To make things easier, one can possibly assume that the term does
    not contain any Î-abstractions.


    Cheers,

    Manuel







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