Mathematica 9 is now available
Services & Resources / Wolfram Forums / MathGroup Archive
-----

MathGroup Archive 2009

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

Search the Archive

Re: problem with reduce

  • To: mathgroup at smc.vnet.net
  • Subject: [mg100365] Re: [mg100347] problem with reduce
  • From: Andrzej Kozlowski <akoz at mimuw.edu.pl>
  • Date: Tue, 2 Jun 2009 06:41:39 -0400 (EDT)
  • References: <200906011111.HAA26170@smc.vnet.net>

First the reason. This is an example of what is called "quantifier  
elimination" (in this case one eliminates the quantifier Exists).  
Algorithms for quantifier elimination exist only for polynomial  
formulas with real number coefficients (or more generally with  
coefficients in real closed fields). This was first shown by the  
Polish logician Alfred Tarski, although modern algorithms are much  
faster. However, there is no algorithm for quantifier elimination over  
the integers. It's not just that one is now known, we know that there  
cannot be any general algorithm. Mathematica can, however, do this in  
certain special cases by using heuristic methods.

However, since everything in your system is linear, you can simply  
eliminate quantifiers over the reals and then add Simplify using the  
assumption that everything is an integer:


sols=Simplify[Reduce[
   Exists[{C[1], C[2]},
    Element[{C[1], C[2]}, Reals] && C[1] >= 0 && C[2] >= 0 && i == 1 +  
C[1] &&
     N == 1 + C[1] + C[2] &&
          iP == 1 + C[1] + C[2] && jP == j - C[2]], {iP, jP},
   Backsubstitution -> True],
  Element[C[1] | C[2] | i | j | N | iP | jP, Integers]]

(N == 1 && i == 1 && iP == 1 && j == jP) || (N > 1 && 1 <= i <= N &&  
iP == N &&
    i + j == jP + N)


Lets now try to check if these really satisfy the original conditions.  
First, the original conditions (over the Integers) were:

cond = Exists[{C[1], C[2]},
    Element[{C[1], C[2]}, Integers] && C[1] >= 0 && C[2] >= 0 &&
     i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] &&
     jP == j - C[2]];

It is easy to verify that the first solution  N == 1 && i == 1 && iP  
== 1 && j == jP  is a solution because now quantifier elimination over  
the integers has become trivial:

  Reduce[cond /. ToRules[sols[[1]]]]
True

In fact, you can simply what C[1] and C[2] must be, treating the  
condition as a linear system of  equations and inequalities:

  Reduce[C[1] >= 0 && C[2] >= 0 && i == 1 + C[1] && N == 1 + C[1] +  
C[2] &&
   iP == 1 + C[1] + C[2] && jP == j - C[2] && sols[[1]], {C[1], C[2],  
iP,
   jP}, Reals,
    Backsubstitution -> True]

N == 1 && i == 1 && C[1] == 0 && C[2] == 0 && iP == 1 && jP == j

 From which you can see that C[1] and C[2] are both zero, and zero is,  
of course, an integer. So we are sure we have one solution:

N == 1 && i == 1 && iP == 1 && jP==j


In the other case,  Reduce still cannot prove that a solution exists  
if we try quantifier eleimination, but you can simply again consider  
everything as a linear system and find C[1] and C[2]:

Reduce[C[1] >= 0 && C[2] >= 0 && i == 1 + C[1] && N == 1 + C[1] + C[2]  
&&
   iP == 1 + C[1] + C[2] && jP == j - C[2] && sols[[2]], {C[1], C[2],  
iP,
   jP}, Reals,
    Backsubstitution -> True]

  N > 1 && 1 <= i <= N && C[1] == i - 1 && C[2] == N - i && iP == N &&
  jP == i + j - N


This again shows you that provided both N and i are integers, C[1] and  
C[2] will also be integers, so the system has actually been solved  
over the integers. So the second solution you want can be written


Element[N, Integers] && Element[i, Integers] &&  N > 1 && 1 <= i <= N  
&& iP == N && jP == i + j - N


Andrzej Kozlowski

On 1 Jun 2009, at 20:11, olfa wrote:

> Hi mathematica community,
> I have to solve this example
> In[88]:= Reduce[Exists[{C[1], C[2]},
>  Element[{C[1], C[2]}, Integers] && C[1] >= 0 && C[2] >= 0 &&
>   i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] &&
>   jP == j - C[2]], {iP, jP}, Backsubstitution -> True]
>
> During evaluation of In[88]:= Reduce::nsmet: This system cannot be
> solved with the methods available to \
> Reduce. >>
>
> I have observed that when I remove Element[{C[1], C[2]}, Integers]  
> && C
> [1] >= 0 && C[2] >= 0 like that:
> In[89]:= Reduce[
> Exists[{C[1], C[2]},
>  i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] &&
>   jP == j - C[2]], {iP, jP}, Backsubstitution -> True]
>
> it gives me an output which is:
>
> Out[89]= iP == N && jP == i + j - N
>
>
> I need to keep the information that Element[{C[1], C[2]}, Integers] &&
> C[1] >= 0 && C[2] >= 0  but reduce tells me that it cannot solve this
> system. why and how to deal with this problem?
> thank you.
>



  • Prev by Date: Re: 100,000 posts!
  • Next by Date: Re: problem with reduce
  • Previous by thread: problem with reduce
  • Next by thread: Re: problem with reduce