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

Simplify and evaluation disagreed about three-valued logic. Simplify gave the Kleene answer
and evaluation absorbed everything into NaN, so "True or (True and (x < 0))" simplified to
True and evaluated at x := i to NaN -- the same expression, two answers, and one of them
claiming the thing does not exist.

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 a
single line in the shared ExpandOnTwoArguments -- if (left.IsNaN || right.IsNaN) return
MathS.NaN -- running before the table was consulted. The four connectives now get first
refusal on an undefined operand, through a settlesNaN flag, and hand back null where they
cannot settle it, which is what still reaches NaN. Checked row by row against Kleene's tables
first: and, or, implies and xor each already give the right answer for an unknown operand,
including leaving it unknown where it decides the result.

Opted in per node rather than changed in the helper for everything, because arithmetic must
stay strict: a rule for a zero factor exists and NaN * 0 must not reach it. Measured, not
assumed -- (0/0) * 0, (0/0) + 1 and (0/0) - (0/0) are all still NaN.

#880 set this out as a fork between Kleene and strict and left it open for want of one
measurement: how much of the suite pins strict propagation. The answer is one assertion of
6385, and it is that issue's own guard clause -- the row asserting `x < 0 and x = 0` is NaN at
x = i, written to keep the test from going vacuous if a comparison ever gained a truth value.
It has gained one indirectly: `i = 0` is decidably False, and False and u is False.

That row moves to a test of its own, which also records the consequence: Simplify answers
`False provided x in RR` there, and the condition is over-strong for that reduction, which
needs one conjunct false rather than both operands real. So Simplify is now weaker than
evaluation on it rather than stronger. The rules #876 conditioned want going through one at a
time to see which still need it; that is not this change.

Suite 6389 passed, F# wrapper 130 passed; casbench 117/119 with 0 wrong; rootcheck 596/596;
simpsweep 10463/10463; propcheck 1340 checks 0 failures; crashcheck 1652 cases 0 crashes and 0
unexpected throws; boundcheck unchanged at 2 disagreements.

Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: Rafael-SOWNet

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