Re: [isabelle] Common sub-expression elimination

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