Re: Re: Re: Wrong limit?
- To: mathgroup at smc.vnet.net
- Subject: [mg105006] Re: [mg104948] Re: [mg104846] Re: Wrong limit?
- From: Adam Strzebonski <adams at wolfram.com>
- Date: Tue, 17 Nov 2009 05:16:24 -0500 (EST)
- References: <200911061014.FAA07962@smc.vnet.net> <hdbha5$jg8$1@smc.vnet.net> <200911121059.FAA18372@smc.vnet.net> <D1312EAF-941E-4C71-98D4-3D05D1E67798@mimuw.edu.pl> <200911140657.BAA18048@smc.vnet.net> <35770DBE-AE16-4A84-96C4-EAAF01D4EA48@me.com> <649321C1-89A0-4E1D-9B98-865F37D9F081@mimuw.edu.pl>
- Reply-to: adams at wolfram.com
Syntax coloring is a feature that is quite independent from kernel
evaluation. All arguments are used in evaluation, even if they are
not correctly colored. Syntax coloring expects the documented
argument structure:
Reduce[expr, vars] or Reduce[expr, vars, dom]
Resolve[expr] or Resolve[expr, dom]
Variables are colored green, so the second argument of Reduce
is colored green. The second argument of Resolve is expected
to be a domain, so it is not colored green. If you use
extensions of the documented syntax, like Reduce[expr, dom]
or Resolve[expr, vars, dom], then syntax coloring may not
recognize the intended meaning of arguments correctly.
Reduce evaluation code, on the other hand, can recognize
that Reals is a domain not a variable, even if it appears
as the second argument.
Best regards,
Adam Strzebonski
Wolfram Research
Andrzej Kozlowski wrote:
> 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
>
- References:
- Wrong limit?
- From: wiso <gtu2003@alice.it>
- Re: Wrong limit?
- From: Maxim <m.r@inbox.ru>
- Re: Re: Wrong limit?
- From: Adam Strzebonski <adams@wolfram.com>
- Wrong limit?