On Tue, 15 Feb 2005 15:22:34 -0800 (PST), Robert Dodier
wrote:
> For my part, I'd feel better about interactive queries if
> the assumptions made that way didn't just evaporate.
> At present assertions established by asksign are purged
> at the end of the current computation. Maybe asksign
> assertions can just stay put?
I agree that they shouldn't evaporate, but I do NOT want them to
persist! The correct solution (which I think RJF has been advocating
for some time) is attaching the assumptions to any results that depend
on them. This is of course not a trivial matter to implement. And
you get some strange situations. For example, using the (arbitrary
and not thought-through) syntax // to mean "assuming that", suppose
you have
expr1: x // x>=0
expr2: x // x<=0
Then clearly it's OK to have the unevaluated conditional
'if x>0 then expr1 else expr2
and you might even simplify that to
x
but what is the meaning of expr1+expr2? Maybe x // equal(x,0) == 0 //
equal(x,0) ? And if the conditionals don't intersect, then simply 0
// false ?
-s