Re: [isabelle] Common sub-expression elimination



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.