Solve reads a membership, and no longer answers the empty set for a statement it cannot read - #1440
Merged
Merged
Conversation
…tatement it cannot read
"x^2 in (0; 1)".Solve("x") was {} -- and so was every f(x) in S with anything but a bare x
on the left, and every statement the solver had no arm for: the arm at the end of the
dispatch answered the empty set, a claim that there is no such x. A membership is solved
now: the members of a listed set each as an equation, an interval as its bounds, each
strict or not as the end is; and a statement that is not read is the set of x with the
property, left as written, which is not a claim. A quantifier that put the negated body
to the solver read that emptiness as a proof: forall x in RR : x^2 in ZZ was True, and is
False, by the witness 1/2.
On the way, the subset decision reads membership of a union, an intersection and a
difference as the connectives they are, so that the solver's answer to x^2 in (0; 1),
((-oo; 0) \/ (0; +oo)) /\ (-1; 1), is compared with (-1; 0) \/ (0; 1) as a set.
The reference's pre-images (Sullivan and Mackey, Ex 7.3.10) are the rows; the book prints
(-1, 1) for the pre-image of (0, 1) under x^2, which is wrong at 0.
#1409
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
Rafael-SOWNet
added a commit
that referenced
this pull request
Sep 21, 2026
Item 6 of the reference's docket (#1409), the half that needs no pair. image(f(x), x in A) is { f(x) : x in A }, which is union({f(x)}, x in A): listed over a listed A, an interval by interval arithmetic where x occurs once in f -- exact for one occurrence and the operations that have images (#1423); the reference's 9c/5 + 32 on (0, 100) is (32, 212) -- and otherwise the family, which answers membership through the quantifiers. preimage(f(x), x in A, Y) is { x in A : f(x) in Y }, and a set builder of that shape is solved on evaluation where the statement solver reads the membership (a listed Y, an interval; #1440), the solutions cut by A: the pre-images of x^2 (Ex 7.3.10), with the one of (0, 1) excluding 0 where the book prints (-1, 1). That shape only: a set builder is not solved on evaluation in general, that being a search on every evaluation. The performance baseline moves to this run. ParseHard reached +3.2% over the baseline recorded at 86af577, and it is the ten function tokens added to the grammar since -- about 12 KB/op each, whatever the input, measured by removing the two of this change and nothing else (3,727,130 to 3,703,015 B/op): a cost in the ANTLR runtime's per-parse work, filed as #1441. Every other row is within 1% of the old baseline. #1409 Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura 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
1 participant
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.
Wrong answer fixed, found measuring the reference's pre-image rows for item 6 of #1409:
"x^2 in (0; 1)".Solve("x")was{}. The statement solver's dispatch hadInf(x, S)for a barexonly, and its last arm answered the empty set for every statement it had no arm for — everyf(x) in S, and everything else unread — which claims there is no suchx. A quantifier that put the negated body to the solver read that emptiness as a proof:forall x in RR : x^2 in ZZwasTrue.Now:
f(x) in Sis solved: a listedSas the union of the equationsf(x) = s; an interval as its bounds, each strict or not as the end is (x^2 in (0; 1)→((-oo; 0) \/ (0; +oo)) /\ (-1; 1),x^2 in {1, 4}→{1, -1, 2, -2},sin(x) in {0}keeps itsn_1family); any otherSis left.{ x : statement }, left as written — no claim. The suite pinned nothing on the old emptiness (12180 passed).MembershipSolvingTest: Ex 7.3.10's pre-images ofx^2compared at ten points (the book prints(-1, 1)for the pre-image of(0, 1), wrong at0), the unread statement left as written, the quantifier nowFalse. BREAKING-CHANGES.md rows measured on a v2.5.0 build (all{}there). Benchmark gate PASSED (the Solve benchmarks within 0.1% of the baseline).Part of #1409.
🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura