a-term-subtracted-from-itself-vanishes — k - k = 0 — is declared Soundness.Sound, which means
"holds for every value the pattern admits, with nothing assumed". It assumes something: that k
has a value.
x ^ (-2) - x ^ (-2) at x = 0 is undefined
0 at x = 0 is 0
So the rewrite turns an expression with no value into one with a value. Where k is undefined,
k - k is undefined and not zero.
It is the odd one out
The sibling rule for the same shape gets it right.
a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero writes
a / a = 1, provided a is not zero
and attaches the condition. k - k = 0 attaches nothing. The boolean rules do the same thing where
they need it — a and False = False carries
.Provided(a.DomainCondition).Provided(b.DomainCondition).
Two ways to fix it, and they are not equivalent
- Attach the condition, as
a / a does: Integer.Zero.Provided(k.DomainCondition). That makes
the answer honest, and it changes answers, so it wants a BREAKING-CHANGES.md entry measured on a
build of each version.
- Re-tier it to
SoundUnderAssumptions. That is a one-word change and it costs nothing in
saturation membership — Saturation.RulesUpTo admits both tiers — but it makes the label true
without making the answer true, and a derivation would still report a step that invented a value.
The first is the better answer if the added condition does not degrade ordinary results; that is
worth measuring rather than assuming, since a Provided competes on complexity and travels.
How it was found
RuleEffectsMeasuredTest.NoSoundRuleChangesWhereItsResultHasAValue, which substitutes a real for
every free variable and compares whether both sides evaluate to something finite. It asks this only
of Sound rules, because SoundUnderAssumptions is already the way of saying "given something I do
not check" — a / (b / c) = a * c / b turns NaN into 0 at c = 0 and its tier says so.
Two things had to be right for the check to see this at all, and both were wrong first:
- Zero has to be among the check points. Arithmetic definedness changes where a denominator
vanishes; four comfortable reals ran the check without ever asking the question.
NaN is a Number. Testing Evaled is Number calls the undefined case defined. Removing the
Provided from a / a = 1 did not trip the check until it asked for a finite number.
Pinned in that test as the one known exception, so a new one fails and so does this one going away.
a-term-subtracted-from-itself-vanishes—k - k = 0— is declaredSoundness.Sound, which means"holds for every value the pattern admits, with nothing assumed". It assumes something: that
khas a value.
So the rewrite turns an expression with no value into one with a value. Where
kis undefined,k - kis undefined and not zero.It is the odd one out
The sibling rule for the same shape gets it right.
a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zerowritesand attaches the condition.
k - k = 0attaches nothing. The boolean rules do the same thing wherethey need it —
a and False = Falsecarries.Provided(a.DomainCondition).Provided(b.DomainCondition).Two ways to fix it, and they are not equivalent
a / adoes:Integer.Zero.Provided(k.DomainCondition). That makesthe answer honest, and it changes answers, so it wants a
BREAKING-CHANGES.mdentry measured on abuild of each version.
SoundUnderAssumptions. That is a one-word change and it costs nothing insaturation membership —
Saturation.RulesUpToadmits both tiers — but it makes the label truewithout making the answer true, and a derivation would still report a step that invented a value.
The first is the better answer if the added condition does not degrade ordinary results; that is
worth measuring rather than assuming, since a
Providedcompetes on complexity and travels.How it was found
RuleEffectsMeasuredTest.NoSoundRuleChangesWhereItsResultHasAValue, which substitutes a real forevery free variable and compares whether both sides evaluate to something finite. It asks this only
of
Soundrules, becauseSoundUnderAssumptionsis already the way of saying "given something I donot check" —
a / (b / c) = a * c / bturnsNaNinto0atc = 0and its tier says so.Two things had to be right for the check to see this at all, and both were wrong first:
vanishes; four comfortable reals ran the check without ever asking the question.
NaNis aNumber. TestingEvaled is Numbercalls the undefined case defined. Removing theProvidedfroma / a = 1did not trip the check until it asked for a finite number.Pinned in that test as the one known exception, so a new one fails and so does this one going away.