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