Decline a connective over a number rather than answering (#897) - #908
Merged
Conversation
A number is not a truth value: 0 is not False and 1 is not True. The same category error was reported three ways, depending on which operator met it and in which position -- NaN where the operator had to look at the number, False or True by short-circuit where it did not, and a rewritten `not 0` for `true xor 0`. Now none of them answers. NaN was the worst of the three. It means "this does not exist", and `true and 0` exists perfectly well; it is not a proposition. That is a wrong claim about the mathematics rather than a graceful failure, and it is the one an if on EvaluableBoolean does not save a caller from. The NaN was not the connective's judgement, which is why it read as arbitrary: Andf's table answers `(Boolean(true), _) => right`, hands back the 0, and the domain check in InnerSimplifyWithCheck then finds a non-boolean where Domain.Boolean was declared and mints MathS.NaN. The connectives now decline the pair outright, so nothing reaches that check. Two answers are withdrawn on purpose. `false and 0` and `true or 0` were False and True by short-circuit, and whether an operand is admissible cannot depend on whether the operator happened to need it. There is no proposition there for False to be the truth of. A caller who insists is unaffected: EvalBoolean throws CannotEvalException for an unevaluated node exactly as it did for NaN, so the type error still surfaces where insisting happens. The distinction this rests on, and the reason it is not a retreat from #880: NaN is how this library spells "no truth value", which is what an order comparison over the complex plane produces, and a connective settles what it can with one. A number is a value of the wrong sort. So (0/0) and False and (i < 0) and False are both still False, and a bare variable is Domain.Any and may yet be a truth value, so `false and x` is still False. Only a genuine number declines. Comparison nodes are untouched -- Equalsf, Greaterf and their kind take numbers, which is their job. The new tests fail 11 of 284 against master and pass 284 of 284 here. 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. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #897, taking the first of its two options: a number is not a truth value here. A truth value
that is neither true nor false is what
MathS.Quantumis for.true and 0,false or 0,false xor 0NaNfalse and 0,true or 0False,True— by short-circuittrue xor 0not 0not 0,0 xor 0true and 1,true and 1/2,true and iNaNThe
NaNwas not the connective's judgementWhich is why it read as arbitrary.
Andf's table answers(Boolean(true), _) => right, hands back the0, and then the domain check inInnerSimplifyWithCheckfinds a non-boolean whereDomain.Booleanisdeclared and returns
MathS.NaN. So the logic never claimed nonexistence — a guard downstream converted"this isn't a boolean" into "this doesn't exist". The connectives now decline the pair outright and
nothing reaches that check.
NaNwas the worst of the three answers for the reason AGENTS.md gives: it means this doesnot exist, and
true and 0exists perfectly well — it is not a proposition. That is a wrong claim aboutthe mathematics, and the one an
ifonEvaluableBooleanwill not save a caller from.Two answers are withdrawn on purpose
false and 0andtrue or 0wereFalseandTrue, settled by short-circuit before the number waslooked at. Those are gone. Whether an operand is admissible cannot depend on whether the operator
happened to need it, and there is no proposition there for
Falseto be the truth of.Nothing is lost for a caller who insists:
EvalBoolean()throwsCannotEvalExceptionfor an unevaluatednode exactly as it did for
NaN, so the type error still surfaces at the layer where insisting happens.DomainConditionstops contradicting evaluation as a side effect —domain(a xor 0)saysTrue, andthere is no longer a
NaNfor it to disagree with, which was #897's second complaint.Why this is not a retreat from #880
A number and an undefined truth value are different things and must not be treated alike.
NaNis howthis library spells no truth value — what an order comparison over the complex plane produces — and a
connective settles what it can with one, which is what #907 just landed. A number is a value of the
wrong sort.
The guard therefore excludes
NaNexplicitly, and it is on the four connectives only. Comparison nodesare untouched:
Equalsf,Greaterfand their kind take numbers, which is their whole job.A correction to the issue's own table
Two rows I wrote up as defects are not, and inspection says so:
false and 0 → Falsewas not "correct by accident." The table answersFalsewithout consultingthe operand, which is Kleene-sound and type-clean. It is withdrawn here for the sort reason above, not
because it was wrong logic.
true xor 0 → not 0was not "nonsense."NotfdeclaresDomain.Boolean, so it passed the guardand came back as an unevaluated node — which is the honest "I could not settle this", not a claim.
So only three of the eight rows were wrong answers, and they were the three where the connective handed
back its non-boolean operand. The uniform decline is what makes the remaining five consistent with them
rather than merely harmless.
Measured
The new tests fail 11 of 284 against
masterand pass 284 of 284 here, checked by restoring master'sfile underneath them.
Suite 6389 passed / 0 failed, F# wrapper 130 passed. casbench 117/119 with 0 wrong, rootcheck 596/596,
simpsweep 10463/10463, propcheck 1340 checks with 0 failures, crashcheck 1652 cases with 0 crashes and 0
unexpected throws, boundcheck unchanged at 2 disagreements.
Cut from
masterat63bd11d7.