Services & ResourcesWolfram ForumsMathGroup Archive

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

Re: Re: Re: Wrong limit?

• To: mathgroup at smc.vnet.net
• Subject: [mg104977] Re: [mg104948] Re: [mg104846] Re: Wrong limit?
• From: Syd Geraghty <sydgeraghty at me.com>
• Date: Sun, 15 Nov 2009 20:47:49 -0500 (EST)
• References: <200911061014.FAA07962@smc.vnet.net> <hdbha5$jg8$1@smc.vnet.net>

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

• References:
  • Wrong limit?
    • From: wiso <gtu2003@alice.it>