diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index f5bb6eb44..ed5c82ee3 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -73,6 +73,7 @@ read first. | **silent** | `DirectChildren` of a conditional set | a name off the predicate's hash, and one in 26^4 threw | `%1`, fresh by construction | | **silent** | `-(a - b)` inside a power, a function or a matrix | left as written | `b - a`, as at the root | | **silent** | `Expand` of a matrix | the matrix, unexpanded | expanded entry by entry | +| **silent** | `false and u`, `true or u`, `false implies u` for an undefined `u` | `NaN` | `False`, `True`, `True` — what the truth table settles | | **silent** | `arctan(x) + arccotan(x)` | `pi/2`, wrong for every negative `x` | `pi/2` or `-pi/2` where the sign is known, else left as written | | **silent** | `log(1, 1)` | `0` | `NaN`, since it is `0/0` | | **silent** | `log(b, 1)` | `0` for any base | `0 provided not b = 1` | @@ -407,6 +408,55 @@ have their own test asserting the unevaluated node, so a future fix flips them b `ln(x) + ln(x+1)`, both recorded elsewhere as wanting a decision rather than a guard. Issue [#902](https://github.com/asc-community/AngouriMath/issues/902). +### A logical connective is no longer strict in `NaN` + +`Simplify` and evaluation disagreed about three-valued logic. `Simplify` gave the Kleene answer and +evaluation absorbed everything into `NaN`, so the two contradicted each other on the same expression: + +``` +"True or (True and (x < 0))".Simplify() -> True +the same, at x := i, evaluated as written -> NaN (was) + -> True (is) +``` + +`i < 0` has no truth value — the default codomain is `Domain.Complex` and the complex numbers are not +ordered — so it evaluates to `NaN`. What changed is what a connective does with such an operand. + +| expression | was | is | +|---|---|---| +| `(i < 0) and False` | `NaN` | `False` | +| `(i < 0) or True` | `NaN` | `True` | +| `False implies (i < 0)` | `NaN` | `True` | +| `(i < 0) implies True` | `NaN` | `True` | +| `(i < 0) and True` | `NaN` | `NaN`, unchanged | +| `(i < 0) or False` | `NaN` | `NaN`, unchanged | +| `not (i < 0)` | `NaN` | `NaN`, unchanged | +| `(i < 0) xor (i < 0)` | `NaN` | `NaN`, unchanged | +| `(0/0) * 0`, `(0/0) + 1` | `NaN` | `NaN`, unchanged | + +The rule is the ordinary one for three-valued logic: an operand with no truth value cannot change an +answer the table settles without it, and where the answer does depend on it the result stays `NaN`. +**Arithmetic is untouched** — `NaN` still absorbs there, which is why this is opted into per node +rather than changed for everything: a rule for a zero factor exists, and `NaN * 0` must not reach it. + +The tables were already three-valued. `Andf` reads `(_, Boolean(false))` as `False` and +`(Boolean(true), _)` as its right operand, which is Kleene as written; what overrode them was one line +in the shared `ExpandOnTwoArguments`, `if (left.IsNaN || right.IsNaN) return MathS.NaN;`, running +*before* the table was consulted. The connectives now get first refusal on an undefined operand and +hand back `null` where they cannot settle it, which is what still reaches `NaN`. + +**One consequence to know about.** For `x < 0 and x = 0` the evaluator now settles `False` for every +`x`, since `x = 0` is decidably false at `x = i` and `False and u` is `False`. `Simplify` answers +`False provided x in RR`, whose condition +([#876](https://github.com/asc-community/AngouriMath/issues/876)) is over-strong for that row: the +reduction needs one conjunct false, not both operands real. So `Simplify` is now weaker than evaluation +there rather than stronger. It is recorded in a test rather than fixed here, because the rules #876 +conditioned want going through one at a time. + +Issue [#880](https://github.com/asc-community/AngouriMath/issues/880), which set this out as a fork +between Kleene and strict evaluation and left it open for want of a measurement. The measurement: one +assertion in the suite changed, and it was that issue's own guard clause. + ### A negated difference is turned round wherever it sits, and `Expand` descends into a matrix `-(a - b)` became `b - a` for a whole expression and not for the same expression inside another node, diff --git a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Classes.cs b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Classes.cs index 97f065302..80a1d581d 100644 --- a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Classes.cs +++ b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Classes.cs @@ -45,19 +45,37 @@ public partial record Variable /// /// Set operations should not be applied on all pairs of elements when it cannot be simplified. /// + /// + /// Whether is asked about a NaN operand instead of the + /// result being NaN outright. A logical connective can settle one -- false and u + /// is false whatever u is -- and arithmetic cannot, so this is off by default: + /// NaN * 0 must not become 0 just because a rule for a zero factor exists. + /// https://github.com/asc-community/AngouriMath/issues/880 + /// private Entity ExpandOnTwoArguments( Entity left, - Entity right, - Func operation, - Func defaultCtor, + Entity right, + Func operation, + Func defaultCtor, bool isExact, - bool propagateSet = true) + bool propagateSet = true, + bool settlesNaN = false) { if (isExact && this.Evaled is (Number { IsExact: true } or Boolean) and var n) return n; left = left.InnerSimplified(isExact); right = right.InnerSimplified(isExact); - if (left.IsNaN || right.IsNaN) return MathS.NaN; + if (left.IsNaN || right.IsNaN) + { + // A connective gets first refusal on an undefined operand, and hands back null where + // it cannot settle the case, which is what falls through to NaN here. Its own table + // is already the three-valued one: `and` reads (_, false) as false and (true, _) as + // its right operand, so a NaN that genuinely decides nothing stays NaN by arriving + // back out of the switch. + if (settlesNaN && operation(left, right) is { } settled) + return settled; + return MathS.NaN; + } if (operation(left, right) is { } preRes) return preRes; diff --git a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Discrete/Evaluation.Discrete.Classes.cs b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Discrete/Evaluation.Discrete.Classes.cs index 6e8f11527..d7be9992d 100644 --- a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Discrete/Evaluation.Discrete.Classes.cs +++ b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Discrete/Evaluation.Discrete.Classes.cs @@ -52,7 +52,7 @@ protected override Entity InnerSimplify(bool isExact) (_, Boolean(true)) => left, _ => null }, - (@this, a, b) => ((Andf)@this).New(a, b), isExact); + (@this, a, b) => ((Andf)@this).New(a, b), isExact, settlesNaN: true); } partial record Orf @@ -69,7 +69,7 @@ protected override Entity InnerSimplify(bool isExact) (_, Boolean(false)) => left, _ => null }, - (@this, a, b) => ((Orf)@this).New(a, b), isExact); + (@this, a, b) => ((Orf)@this).New(a, b), isExact, settlesNaN: true); } partial record Xorf @@ -88,7 +88,7 @@ protected override Entity InnerSimplify(bool isExact) (_, Boolean(false)) => left, _ => null }, - (@this, a, b) => ((Xorf)@this).New(a, b), isExact); + (@this, a, b) => ((Xorf)@this).New(a, b), isExact, settlesNaN: true); } partial record Impliesf @@ -107,7 +107,7 @@ protected override Entity InnerSimplify(bool isExact) (_, Boolean(false)) => !left, _ => null }, - (@this, a, b) => ((Impliesf)@this).New(a, b), isExact); + (@this, a, b) => ((Impliesf)@this).New(a, b), isExact, settlesNaN: true); } partial record Equalsf diff --git a/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs b/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs index 06e112faa..0467bba53 100644 --- a/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs +++ b/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs @@ -473,7 +473,6 @@ public void ExcludedMiddleHoldsWhicheverOperandCarriesTheNegation(string input) [Theory] [InlineData("x < 0 and x >= 0")] [InlineData("x > 0 and x <= 0")] - [InlineData("x < 0 and x = 0")] [InlineData("x < 0 or x >= 0")] [InlineData("x <= 0 or x > 0")] [InlineData("x < x")] @@ -490,6 +489,29 @@ public void DecidingAPairOfComparisonsKeepsItsValueOffTheRealLine(string input) Assert.Equal(atI, original.Simplify().Substitute("x", "i").Evaled); } + // https://github.com/asc-community/AngouriMath/issues/880 + // `x < 0 and x = 0` was a row of the theory above until evaluation became Kleene, and it + // no longer belongs there: at x = i one conjunct is *decidably* false -- `i = 0` is False, + // not NaN -- and `False and u` is False whatever `u` is. So there is something to decide + // here, and the value is False rather than NaN. + // + // Which leaves the pair disagreeing the other way round from #876. Evaluation now settles + // the conjunction everywhere, while Simplify answers `False provided x in RR`, whose + // condition is unnecessary for this row: the reduction needs one conjunct to be false, not + // both operands to be real. The condition is over-strong rather than wrong, so it is + // recorded here rather than removed -- the rules #876 conditioned would want going through + // one at a time to see which of them still need it, and that is not this change. + [Fact] + public void AConjunctionWithOneFalseConjunctIsFalseOffTheRealLineToo() + { + var original = "x < 0 and x = 0".ToEntity(); + Assert.Equal(Entity.Boolean.False, original.Substitute("x", "i").Evaled); + + // And what Simplify gives is weaker, which is the follow-up rather than a regression: + // it declines off the real line where the evaluator decides. + Assert.Equal(MathS.NaN, original.Simplify().Substitute("x", "i").Evaled); + } + // https://github.com/asc-community/AngouriMath/issues/876 §3 // The unsatisfiable conjunction was decided and the valid disjunction was not, so the // library took the half of excluded middle that is unsound off the real line and @@ -876,5 +898,57 @@ public void ASystemsAnswerSimplifiesEntryByEntry() $"the system's answer simplified to {simplified.Stringize()}, which is no shorter " + $"than the {answer.Stringize()} it came from"); } + + // https://github.com/asc-community/AngouriMath/issues/880 + // A connective is no longer strict in NaN. `false and u` is false and `true or u` is true + // whatever `u` is, so an operand with no truth value does not absorb an answer the truth + // table settles without it. Simplify already answered this way -- `true or (true and + // (x < 0))` is True -- while evaluation answered NaN, so the two contradicted each other. + // + // `i < 0` is the undefined operand throughout: the default codomain is Domain.Complex and + // the complex numbers are not ordered. + [Theory] + [InlineData("(i < 0) and false", "false")] + [InlineData("false and (i < 0)", "false")] + [InlineData("(i < 0) or true", "true")] + [InlineData("true or (i < 0)", "true")] + [InlineData("false implies (i < 0)", "true")] + [InlineData("(i < 0) implies true", "true")] + public void AConnectiveSettlesWhatItsTruthTableSettles(string expression, string expected) => + Assert.Equal(expected.ToEntity(), expression.ToEntity().Evaled); + + // And what the table does not settle stays unsettled: NaN means "this does not exist", so + // a connective may not invent a value for it either. + [Theory] + [InlineData("(i < 0) and true")] + [InlineData("(i < 0) or false")] + [InlineData("not (i < 0)")] + [InlineData("(i < 0) xor (i < 0)")] + [InlineData("(i < 0) xor true")] + [InlineData("(i < 0) implies false")] + public void AConnectiveInventsNothingItCannotSettle(string expression) => + Assert.Equal(MathS.NaN, expression.ToEntity().Evaled); + + // Arithmetic stays strict, which is the reason this is opted into per node rather than + // done in the shared helper for everything: a rule for a zero factor exists, and NaN * 0 + // must not reach it. + [Theory] + [InlineData("(0/0) * 0")] + [InlineData("(0/0) + 1")] + [InlineData("(0/0) - (0/0)")] + [InlineData("(0/0) ^ 0")] + public void ArithmeticIsStillStrictInNaN(string expression) => + Assert.Equal(MathS.NaN, expression.ToEntity().Evaled); + + // The contradiction this removes, stated as the commutation it broke. + [Theory] + [InlineData("true or (true and (x < 0))")] + [InlineData("false and (x < 0)")] + public void SimplifyAndEvaluationAgreeOffTheRealLine(string input) + { + var original = input.ToEntity(); + Assert.Equal(original.Substitute("x", "i").Evaled, + original.Simplify().Substitute("x", "i").Evaled); + } } }