|x| = a is inverted to a parametric set without the condition that makes it valid, so for a negative right-hand side it returns solutions that are not solutions.
"abs(x) = -1".ToEntity().Solve("x") // { -e ^ (i * r_1) provided r_1 in RR }
The correct answer is the empty set: |x| ≥ 0 for every complex x, so |x| = -1 has no solution.
It is wrong, not merely unhelpful
Take the member at r_1 = 0:
x = -e ^ (i * 0) = -1
abs(-1) = 1 <- measured
1 ≠ -1, so that member does not satisfy the equation it was returned for. The same holds for every member, since abs(a * e^(i*r)) = |a| regardless of r.
Measured on master (21f0d16)
|
|
abs(x) = -1 |
{ -e ^ (i * r_1) provided r_1 in RR } ← wrong |
abs(x) + 1 via SolveEquation |
{ -e ^ (i * r_1) provided r_1 in RR } ← same, wrong |
abs(x) = a |
{ a * e ^ (i * r_1) provided r_1 in RR } ← right shape, missing the guard |
abs(x) = 3 |
{ 3 * e ^ (i * r_1) provided r_1 in RR } ← correct |
abs(x) = 0 |
{ 0 provided r_1 in RR } ← correct |
eval abs(-1 * e ^ (i * 0)) |
1 ← the check that makes the first row wrong |
Cause, and its relation to #318
#318 asks for exactly this inversion and states the missing piece in its own text:
|x| = a should return { a e ^ (i * r) : r in RR and a >= 0 }
The r in RR half is implemented; the a >= 0 half is not. So the parametric-set part of #318 is done, and what is left of it is the guard — which turns out not to be a cosmetic refinement but the difference between a right answer and a wrong one.
For a symbolic a the guard cannot be decided, so the honest result is a Providedf on a >= 0 rather than a decision. For a literal negative a it is decidable and the answer is the empty set.
Why the harnesses did not find it
rootcheck verifies that returned roots satisfy their equation, which is precisely the property violated here — but it generates polynomial and rational equations, not ones under abs. Extending it to absolute-value and other non-invertible-on-the-reals shapes would have caught this, and is worth doing whether or not this is fixed first.
|x| = ais inverted to a parametric set without the condition that makes it valid, so for a negative right-hand side it returns solutions that are not solutions.The correct answer is the empty set:
|x| ≥ 0for every complexx, so|x| = -1has no solution.It is wrong, not merely unhelpful
Take the member at
r_1 = 0:1 ≠ -1, so that member does not satisfy the equation it was returned for. The same holds for every member, sinceabs(a * e^(i*r)) = |a|regardless ofr.Measured on
master(21f0d16)abs(x) = -1{ -e ^ (i * r_1) provided r_1 in RR }← wrongabs(x) + 1viaSolveEquation{ -e ^ (i * r_1) provided r_1 in RR }← same, wrongabs(x) = a{ a * e ^ (i * r_1) provided r_1 in RR }← right shape, missing the guardabs(x) = 3{ 3 * e ^ (i * r_1) provided r_1 in RR }← correctabs(x) = 0{ 0 provided r_1 in RR }← correcteval abs(-1 * e ^ (i * 0))1← the check that makes the first row wrongCause, and its relation to #318
#318 asks for exactly this inversion and states the missing piece in its own text:
The
r in RRhalf is implemented; thea >= 0half is not. So the parametric-set part of #318 is done, and what is left of it is the guard — which turns out not to be a cosmetic refinement but the difference between a right answer and a wrong one.For a symbolic
athe guard cannot be decided, so the honest result is aProvidedfona >= 0rather than a decision. For a literal negativeait is decidable and the answer is the empty set.Why the harnesses did not find it
rootcheckverifies that returned roots satisfy their equation, which is precisely the property violated here — but it generates polynomial and rational equations, not ones underabs. Extending it to absolute-value and other non-invertible-on-the-reals shapes would have caught this, and is worth doing whether or not this is fixed first.