Let a connective settle what its truth table settles (#880)

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,

Sources/AngouriMath/Functions/Evaluation/Evaluation.Classes.cs

@@ -45,19 +45,37 @@ public partial record Variable
         /// <param name="propagateSet">
         /// Set operations should not be applied on all pairs of elements when it cannot be simplified.
         /// </param>
+        /// <param name="settlesNaN">
+        /// Whether <paramref name="operation"/> is asked about a <c>NaN</c> operand instead of the
+        /// result being <c>NaN</c> outright. A logical connective can settle one -- <c>false and u</c>
+        /// is <c>false</c> whatever <c>u</c> is -- and arithmetic cannot, so this is off by default:
+        /// <c>NaN * 0</c> must not become <c>0</c> just because a rule for a zero factor exists.
+        /// https://github.com/asc-community/AngouriMath/issues/880
+        /// </param>
         private Entity ExpandOnTwoArguments(
             Entity left,
-            Entity right, 
-            Func<Entity, Entity, Entity?> operation, 
-            Func<Entity, Entity, Entity, Entity> defaultCtor, 
+            Entity right,
+            Func<Entity, Entity, Entity?> operation,
+            Func<Entity, Entity, Entity, Entity> 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;

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

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);
+        }
     }
 }