Email Gateway (Aug 22 2022 at 12:09): Email Gateway (Aug 22 2022 at 12:09):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 22 2022 at 12:10):From: Ramana Kumar <rk436@cam.ac.uk>
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.
Email Gateway (Aug 22 2022 at 12:10):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 22 2022 at 12:18):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Apr 20 2024 at 08:16 UTC