On Sun, Dec 18, 2011 at 16:34, Robert Dodier <robert.dodier at gmail.com>wrote:
> ...Given that the inner integral is evaluated before the outer
> one, there's no way to know that x > -1 and x < 1.
>
> I don't see a way to change the outcome, short of giving integrate a
> different evaluation scheme. That's not out of the question, but it would
> be an uphill battle to convince everyone it's a good idea....
I think it makes perfect sense to have sum, integrate, limit, if, etc.
interpret their arguments in appropriate environments. When I say
"interpret", I'm intentionally not limiting that to evaluation.
Simplification should have similar properties. But I don't think it's
going to be easy to do all that cleanly. I don't think the right way to do
it is with some sort of "evaluation scheme", but some sort of rewriting
(macro expansion) to a semantically more transparent form. Then again,
right now, we don't even have a way of expressing that an assumption only
applies to a bounded part of an expression. That might be a good first
step.
-s