Services & Resources / Wolfram Forums / MathGroup Archive

MathGroup Archive 2009

[Date Index] [Thread Index] [Author Index]

Search the Archive

Re: Re: Re: Wrong limit?

Reals is certainly used in evaluation, e.g.

 Resolve[Exists[x, x^2 + 1 == 0], x]

True

Resolve[Exists[x, x^2 + 1 == 0], x, Reals]

False

I do see a difference in context coloring between

Resolve[Exists[x, x^2 + 1 == 0], x, Reals]

and

Reduce[Exists[x, x^2 + 1 == 0], x, Reals]

but its different from the one reported by you. Here, Reals is not 
colored in either case but the variable x is colored in the case of 
Resolve but not in the case of Reduce: I have no idea why.

Andrzej Kozlowski


On 16 Nov 2009, at 07:17, Syd Geraghty wrote:

> Hi all,
>
> Reduce[ForAll[eps, eps > 0,
>    Exists[del, del > 0,
>     ForAll[x,
>      Implies[0 < Abs[x - a] < del,
>       Abs[(x^2 - a^2)/(5 x^2 - 4 a x - a^2) - M] < eps]]]],  Reals] // AbsoluteTiming
> 									
>
> {2.947591, (a < 0 && M == 1/3) || (a == 0 && M == 1/5) || (a > 0 && M == 1/3)}
>
> Reals above is colored green and the reason given is >> Variable made special by use in arguments
>
> However using Resolve below:
>
> Resolve[ForAll[eps, eps > 0,
>    Exists[del, del > 0,
>     ForAll[x,
>      Implies[0 < Abs[x - a] < del,
>       Abs[(x^2 - a^2)/(5 x^2 - 4 a x - a^2) - M] < eps]]]],  Reals] // AbsoluteTiming
>
>
>  Reals is not colored and therefore is, presumably, not special or not used in the evaluation.
>
> This seems at odds with the documentation which implies the Domain of Reals should be treated in the same way (and is the default if not explicitly included).
>
> Is this perhaps why Resolves fails to return the correct answer in a reasonable (<10 minutes) time?
>
> Incidentally on my 2 core machine Reduce is slightly faster than ParallelQE - by about 9%
>
>
> Cheers .... Syd
>
> Syd Geraghty B.Sc, M.Sc.
>
> sydgeraghty at mac.com
>
> Mathematica 7.0.1.0 for Mac OS X x86 (64 - bit) (12th September 2009)
> MacOS X V 10.6.1 Snow LeopardMacBook Pro 2.33 GHz Intel Core 2 Duo  2GB RAM
>
>>
>> Andrzej Kozlowski wrote:
>>> I find it curious (and perhaps slightly disappointing) that replacing Reduce by Resolve seems to fail (or at least it outruns my patience while Reduce does not). This is puzzling because Resolve and not Reduce is supposed to be "the principal tool" for quantifier elimination and, according to the documentation "Resolve is in effect automatically applied by Reduce." Presumably Reduce applies some additional transformations not available to Resolve, which make it possible for it to succeed where Resolve fails (or takes far too long), but what could they be?
>>>
>>> Andrzej Kozlowski
>>
>
> On Nov 13, 2009, at 10:57 PM, Adam Strzebonski wrote:
>
>> The difference between Reduce and Resolve in this example is that
>> Reduce uses cylindrical algebraic decomposition (because it needs
>> to produce a result solved for the free variables) and Resolve
>> uses virtual substitution. Virtual substitution is often faster
>> than cylindrical algebraic decomposition, but not for this example.
>> Unfortunately, there is no way to tell a priori which method will
>> be faster and the difference is often between one method hanging
>> and the other returning reasonably fast. One way of solving this
>> problem would be to try both methods in parallel.
>>
>> In[2]:= LaunchKernels[2]
>> Out[2]= {KernelObject[1, "local"], KernelObject[2, "local"]}
>>
>> In[3]:= ParallelQE[form_] :=
>>  ParallelTry[#[form, Reals] &, {Resolve, Reduce}]
>>
>> In[6]:= ParallelQE[
>>   ForAll[eps, eps > 0,
>>    Exists[del, del > 0,
>>     ForAll[x,
>>      Implies[0 < Abs[x - a] < del,
>>       Abs[(x^2 - a^2)/(5 x^2 - 4 a x - a^2) - M] <
>>        eps]]]]] // AbsoluteTiming
>>
>> Out[6]= {12.181224, (a < 0 && M == 1/3) || (a == 0 &&
>>     M == 1/5) || (a > 0 && M == 1/3)}
>>
>> I have run this on a single processor machine, so ParallelQE is
>> slower than Reduce. If my computer had two (or more) processors
>> there should be not much timing difference between ParallelQE
>> and the faster of Reduce and Resolve.
>>
>> Best regards,
>>
>> Adam Strzebonski
>> Wolfram Research
>
  • Prev by Date: Re: Re: Re: Wrong limit?
  • Next by Date: Undo in Mathematica
  • Previous by thread: Re: Re: Wrong limit?
  • Next by thread: Re: Re: Re: Wrong limit?