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.