Repository navigation
Where the rewrite graph actually stands is held by a test (#746) - #1190
Merged
Merged
Conversation
#746 tier 2 is the rewrite graph, and what it can do today was described in documents and measured nowhere. Two facts, pinned: The safe ceiling is nearly inert on ordinary input. Of five expressions -- (a + b) / (a * b), x / x, (x + 1) / (x + 1), the Pythagorean identity and (x + 1) * (x - 1) -- saturation under SafeRules moves exactly one and hands four back unchanged. That is not a defect in the expressions; it is the trade tier 2 has not resolved. SafeRules is RulesUpTo(Rearranges), 142 of 324, and the 152 at Unknown are excluded because their growth was never judged: the ceiling that is safe finds little, and the ceiling that finds things admits rewrites nobody measured. And no written pattern can put a condition into the graph at all. Only 35 of the 324 rules have a right-hand side written as a pattern, and none mentions `provided` -- so a Providedf reaches an e-class only along the code-built path, where a rule extracts a witness term, runs code on it and puts the result back. That last one narrows a question EqualitySaturationReviewFindings.md was still being read as leaving open. The document had already retracted the claim that the e-graph cannot represent a conditional equivalence -- it was the buildable type table, and a line in Construct was the fix -- and this says why the case is hard to reach at all: the union that would need a meaning is not one e-matching can currently form. Held at zero, so the first two-sided conditional rule fails there rather than quietly making it live again. Both were written first as `>= 0` assertions, which pass by asking nothing. Replaced with the numbers, which is the only version worth having. Full suite 9567 passed, 0 failed. Part of #746. 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.
#746 tier 2 is the rewrite graph, and what it can do today was described in documents and measured
nowhere. Two facts, now pinned.
The safe ceiling is nearly inert on ordinary input
Of five expressions —
(a + b) / (a * b),x / x,(x + 1) / (x + 1), the Pythagorean identity and(x + 1) * (x - 1)— saturation underSafeRulesmoves one and hands four back unchanged.That is not a defect in the expressions. It is the trade tier 2 has not resolved:
SafeRulesisRulesUpTo(Rearranges), 142 of 324 rules, and the 152 sitting atUnknownare excluded becausetheir growth was never judged. The ceiling that is safe to run finds little; the ceiling that finds
things admits rewrites nobody measured. Stating it as a number makes it something that can move
rather than something described.
No written pattern can put a condition into the graph at all
Only 35 of the 324 rules have a right-hand side written as a pattern, and none of them
mentions
provided. So aProvidedfreaches an e-class only along the code-built path, where a ruleextracts a witness term, runs code on it, and puts the result back.
This narrows a question
EqualitySaturationReviewFindings.mdis still being read as leaving open.That document had already retracted the claim that the e-graph cannot represent a conditional
equivalence — it was the buildable-type whitelist, and a line in
Constructwas the whole fix. Whatthis adds is why the case is hard to reach at all: the union that would need a meaning is not one
e-matching can currently form.
Held at zero, so the first two-sided conditional rule fails there rather than quietly making the
question live again.
A note on how these were written
Both started as
>= 0assertions — which pass by asking nothing, and are exactly the failure modethis repository's other checks are careful about. I ran them, read the real numbers out, and replaced
them. The first version would have been worse than no test, because it would have looked like
coverage.
What this does not do
It does not decide the open question, which is the one the document actually states: how much
should ride on an e-node beyond its bare shape — a general "attach anything, forget nothing"
representation, or a list of special cases extended as each is found, with
Codomainthe only liveinstance. That is a design decision and not mine to take unilaterally.
Checks
Full suite 9567 passed, 0 failed, 14 skipped.
Part of #746.
🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura