Repository navigation
EqualitySaturationNeverChangesTheValueItClaimsToPreserve compares two expressions that have no value #1162
Description
Activity
- added 4 commits that reference this issue
on Sep 4, 2026 Retracting this issue's cause
The rule is not unsound, and the description above is wrong. I filed it while declaring growths
for #825, blamedIsLogicfor admitting a free variable, and stated the mechanism before measuring
the values it makes a claim about.Measured:
(0.37 and 0.37) or (0.37 and not 0.37) -> 37/100 and 37/100 or 37/100 and not 37/100 0.37 and (0.37 or not 0.37) -> 37/100 and (37/100 or not 37/100)A boolean operation on a non-boolean does not evaluate to
NaN— it does not evaluate at all.
Both sides come back stuck. Neither has a truth value, so nothing has changed between them.
(a and b) or (a and not b) = a and (b or not b)is a boolean identity and holds.Where the defect actually is
EqualitySaturationNeverChangesTheValueItClaimsToPreservesubstitutes a real for every free
variable and compares what the two sides evaluate to, withcatch { continue; } // a boolean/set-valued corpus entry: not this test's claim
.Evaledon37/100 and 37/100throws nothing, so that skip never fires.EqualsImpreciselythen
compares two different unevaluated forms of a thing with no value and calls it a disagreement. The
test's comment names the entries it means to exclude and its mechanism for excluding them has never
worked — and"a and b or a and not b"is in its own corpus precisely so the boolean rules get
exercised.Fixed in #1166, and made stricter where it matters: skipped only when neither side has a value,
and failing when one has a value and the other does not, since that is a rewrite which lost one
and is exactly what the test is for. Today that case would have been compared structurally and might
have passed.What was right in the original report
Only the general point, which stands on its own: a growth declaration is not metadata. Writing
one moves a rule into the set equality saturation runs, which may be the first time it has ever run,
so a batch of declarations should expect to surface things — and should treat a failure of that
property test as a finding to investigate rather than a number to work around. Here the finding
turned out to be about the test.IsLogicadmitting a free variable is fine as it stands; a variable may be a boolean, and the rules
that need more than that — excluded middle, from #876 — already attach aTruthCondition.Closing as resolved by #1166.
- changed the title
[-]A boolean distribution rule marked Sound changes the value when its operands are not booleans[/-][+]EqualitySaturationNeverChangesTheValueItClaimsToPreserve compares two expressions that have no value[/+]on Sep 5, 2026 - added a commit that references this issue
on Sep 5, 2026
((k and p) or (k and q)) = (k and (p or q))and its dual are declaredSoundness.Soundandguarded with
when: IsLogic(k, p, q). That guard passes a free variable, since a free variablemay turn out to be a boolean — and then the identity does not survive the variable being something
else.
Equality saturation reaches it and the existing property test catches it:
TransformationTest.EqualitySaturationNeverChangesTheValueItClaimsToPreservefails on"a and b or a and not b".Why nobody has seen it
The rule's growth is
Unknown, andSaturation.RulesUpTobuildsSafeRulesas the rules up toRearranges, so equality saturation has never fired it.Unknownwas standing in for asoundness guard without anyone intending it to.
It surfaced while declaring growths for #825: the count for this rule is plainly
-(1 + |k|), soCollectsis the right growth — and writing it down is what let the rule run and fail. Thedeclaration was withdrawn rather than shipped, with the reason recorded beside the rule, because the
growth is not what is wrong here.
What is actually wrong
One of two things, and it wants deciding rather than patching:
IsLogicis meant to admit a free variable, the rule holds only when thatvariable really is a boolean, which is
SoundUnderAssumptionsand notSound.Sound,IsLogichas to refuse a variable whosecodomain does not say it is boolean, and then the rule simply does not fire on
a and b.The second is the stronger reading of what
Soundis supposed to mean here — "holds for every valuethe pattern admits, with nothing assumed" — but it narrows the rule, and how much it narrows it is
worth measuring before choosing.
The general point, which is worth more than this rule
A growth declaration is not metadata. Declaring one moves a rule into the set equality saturation
runs, so it can expose a rule whose soundness was wrong all along. Any batch of declarations should
expect to find this, and should treat a failure of
EqualitySaturationNeverChangesTheValueItClaimsToPreserveas a finding about the rule rather thanabout the declaration.
Worth checking whether other rules guarded by
IsLogichave the same hole; the two distributions aresimply the two that a declaration reached first.