Repository navigation
The growth corpus reaches 194 rules instead of 84 (#825) - #1160
Merged
Merged
Conversation
A declaration is only checked if the corpus makes the rule fire, and the arithmetic grammar reached 84 of the 324. Six whole sets -- trigonometry, booleans, sets, comparisons and both factorial ones -- were never exercised at all, so a declaration on any of their rules was checked by a test that never ran it. Two changes. Shapes the generated grammar does not build are supplied on top of it, the way MatchedRulesAgreeWithTheSwitchTest already supplies its own: the trigonometric identities and their arguments, logarithms, factorials both ways round, the boolean laws, comparisons, set operations, and the polynomial shapes the division, gcd and factorisation sets want. And a rule is now tried at every node of every corpus expression rather than only at the root, since a rule matches where its shape sits and asking only about whole expressions leaves most of them never firing. 139 rules now fire, 51 of them carrying a declaration, against 84 and 18 before. The counts are asserted so that the check cannot quietly stop being exercised. Every one of the 51 existing declarations was re-run against the wider corpus. None is contradicted, which is worth knowing rather than assuming: the coverage this adds is exactly where an untested claim would have been hiding, and the one false declaration found when this test was written was found the same way. No rule's growth changes here. The 88 undeclared rules that now fire are the measured evidence for declaring them, and that is a separate change because Collects and Rearranges alter which rules equality saturation fires. Full suite 9552 passed, 0 failed. Part of #825. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
194 of the 324 rules now fire, against 139 after the first extension and 84 before it. 59 of those carry a declaration, so that many are checked rather than merely asserted. The largest block that was out of reach is the comparison set. Its rules key on zero or a number being on the left of the operator, on both sides being the same thing, and on a negative factor or divisor standing beside a zero -- none of which an arithmetic grammar produces, since it builds comparisons only in the form the writer would. So `0 > x`, `x >= x`, `x / (-2) > 0` and `(-2) * x <= 0` are given directly, over all five comparison operators. The rest are De Morgan in both directions, which the earlier shapes gave only one way round; the trigonometric reciprocal pairs, where a cosecant times a sine and a cotangent of an arccotangent are the shapes rules exist for and nothing built; logarithms in and of reciprocal bases; and the differences and products that contain their own operand a second time. No declaration is contradicted by any of it. Full suite 9552 passed, 0 failed. Part of #825. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
The rules about comparisons bind their operands with `Any`, so one of those operands can be a comparison itself. Building the replacement with `<` or `>` then chains, where the same rule written with `EqualTo` would not: `(x > y) < 0` is `x > y and y < 0`, seven nodes rather than three. That is not hypothetical and it is the difference between a true declaration and a false one. `(a / k > 0) = (a < 0)` for a negative k measures -2 at every point the corpus reached, and counting its pattern against its replacement gives -(|k| + |zero|), which is at most -2 as well. Both say Collects. On `((x > y) / (-2)) > 0` the pattern is seven nodes and so is the replacement, the delta is 0, and Collects is false. The same holds for the fifteen rules of that family and for the comparison rules that turn an operand round. The comment on `a-equals-with-zero-on-the-left-turns-round` says exactly this -- that `EqualTo` does not chain "the way `Equalizes` and the comparison operators do" -- and its comparison twins were left undeclared for that reason. A corpus of a hundred and ninety-four rules could not refute the wrong declaration, because it never built a comparison inside a comparison. Now it does, so a rule whose replacement chains no longer looks like a clean shrink at every point that is looked at. No declaration is contradicted, so the fifty-nine that exist are unaffected. Full suite 9552 passed, 0 failed. Part of #825. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
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.
A declaration is only checked if the corpus makes the rule fire. The arithmetic grammar reached 84
of the 324, and six whole sets — trigonometry, booleans, sets, comparisons and both factorial ones
— were never exercised at all. A declaration on any of their rules was being checked by a test that
never ran it.
Three changes
A rule is tried at every node, not only at the root. A rule matches where its shape sits, and
asking only about whole corpus expressions left most of them never firing.
Shapes the generated grammar does not build, supplied on top of it the way
MatchedRulesAgreeWithTheSwitchTestalready supplies its own: the trigonometric identities and thearguments the multiple-angle rules want, logarithms, factorials both ways round, the boolean laws,
set operations, and the polynomial shapes the division, gcd and factorisation sets match.
The comparison set, which was the largest block still out of reach. Its rules key on zero or a
number being on the left of the operator, on both sides being the same thing, and on a negative
factor or divisor standing beside a zero — none of which an arithmetic grammar produces, because it
builds comparisons only in the form a person would write:
over all five comparison operators. With those, De Morgan in both directions rather than one, the
trigonometric reciprocal pairs (
cosec(x) * sin(x),cotan(arccotan(x))— shapes rules exist forand nothing built), logarithms in and of reciprocal bases, and the differences and products that
contain their own operand a second time.
Both counts are asserted, so the check cannot quietly stop being exercised.
Nothing it newly reaches contradicts a declaration
Worth stating rather than assuming: this coverage is exactly where an untested claim would have been
hiding, and the one false declaration this test found when it was written (#1158) was found the same
way — by making a rule fire that nothing had made fire before. All 59 declarations that now run
survive it.
No growth changes here
This alters nothing that runs. The undeclared rules it newly exercises are the measured evidence for
declaring them, which is #1161 and its successors —
Saturation.RulesUpTobuilds its set as therules up to
Rearranges, so those declarations do change which rules equality saturation fires.Verification
Full suite 9552 passed, 0 failed, 14 skipped.
Part of #825.