[isabelle] Common sub-expression elimination
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
To make things easier, one can possibly assume that the term does not
contain any Î-abstractions.
This archive was generated by a fusion of
Pipermail (Mailman edition) and