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.
>
- References:
- problem with reduce
- From: olfa <olfa.mraihi@yahoo.fr>
- problem with reduce