Repository navigation
Membership in a set operation is decided by Kleene's connectives - #2221
Merged
Merged
Conversation
Unionf.TryContains returned the right side's verdict whenever the left
did not say yes, so a left side that left membership open and a right
side that excluded the element made the union False. 2^89 - 1 is a
Mersenne prime, past the machine word, where PP leaves membership open:
(2^89 - 1) in (PP \/ [0; 1]) False, on 2.6.0 and master
(2^89 - 1) in ([0; 1] \/ PP) left as written
A union contains what either side contains. It is now Kleene's or: a
member where either side decides it is, outside where both decide it is
not, and open otherwise.
Intersectionf and SetMinusf were not wrong. Each decided only where both
sides did. They are now Kleene's and: an element one side decides is
outside, or that a difference's right side decides is inside, is outside
whatever the other side says. So (2^89 - 1) in ([0; 1] \ PP) and
(2^89 - 1) in (PP \ [0; 10^30]) are False, where they were left open.
Contains.cs pinned 1 in {x} \ {1} as undecided. 1 is in {1}, so it is
outside the difference whatever x is, and the row now expects it decided
False. Every other row of that table is unchanged.
MembershipInASetOperationTest: 17 cases, of which 5 fail on master,
the three union answers and the two differences.
Fixes #2219.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## master #2221 +/- ##
==========================================
- Coverage 86.65% 86.64% -0.01%
==========================================
Files 306 306
Lines 67536 67550 +14
Branches 19587 19588 +1
==========================================
+ Hits 58523 58532 +9
- Misses 4897 4901 +4
- Partials 4116 4117 +1
Flags with carried forward coverage won't be shown. Click here to find out more.
🚀 New features to boost your workflow:
|
Rafael-SOWNet
added a commit
that referenced
this pull request
Oct 30, 2026
x in S and a divides b were refused by both compilers. Each now compiles to the truth value evaluation gives: 1, 0 or NaN in FastExpression, and true, false or null in the LINQ compiler. The set is fixed when the expression is compiled, so only the element is computed. CompiledMembership rewrites a membership, before either compiler sees it, into the statement it makes about its element: - a union, an intersection and a difference become Kleene's or, and, and and-not of the memberships in their sides, as evaluation decides them since #2221; - an interval becomes the element's imaginary part being 0 and the two comparisons with its ends, since a number that is not real is in no interval, and i in [0; 1] is False rather than undecided; - a finite set becomes an equality with one of its members; - a conditional set becomes its predicate of the element. A membership in RR, CC, ZZ, ZZ+, ZZ* or PP is left for each compiler, which calls NumberStatements.In: a new FastExpression instruction, CALL_MEMBER, whose reference names the set, and a method call in LINQ. It has no truth value at NaN. An infinity is in RR and CC, as evaluation holds it until #2220 is decided, and in none of the sets of whole numbers. Primality comes from Primes.IsPrime, the interpreter's trial division, and is left open past 2^63, where the interpreter leaves it. QQ stays refused, because every finite double is a rational while pi in QQ is False. BB stays refused too. So does any set with one of those inside it. Divisibility is NumberStatements.Divides, through CALL_DIVIDES in FastExpression. Between whole numbers it is whether the remainder is 0, with 0 dividing only 0, and a double's remainder is exact however large. It has no truth value anywhere else, as evaluation gives NaN for 2 divides 5/2. MembershipCompilationTest compares both compilers with evaluation: - 21 sets at 20 points, among them i, 1 + i, 2i, +oo and -oo; - divisibility on a 10 by 9 grid, with 10^20, 5/2, 2i and +oo; - memberships inside an Iverson bracket, a piecewise and connectives; - the refusals. Infinities are left out of the piecewise case, since a compiled -x at +oo has a NaN imaginary part. That is #2222, and it predates this change. Part of #2195. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Member
|
It feels as though |
Member
Author
|
Yes. Two tests decide it, and both are proofs:
Looking turned up something worse. The trial division 🤖 Generated with Claude Code |
Rafael-SOWNet
added a commit
that referenced
this pull request
Oct 30, 2026
…2232) Primes.IsPrime was trial division, decided only for a number that fits a long, and it had three defects: - It hung. The loop was divisor * divisor <= value, and past divisor = 3037000499 the square overflows long and wraps negative. So for a prime between 3037000499^2 and 2^63 the loop ran until the divisor reached the number itself. 9223372036854775783 in PP, the largest prime below 2^63, did not finish on 2.6.0 or on master. - It was slow: about 1.5e9 divisions for a prime near 2^63, and 1.1 s for 2^61 - 1. - It left every number past 2^63 open, the Mersenne prime 2^89 - 1 and the composite 2^67 - 1 alike. @Happypig375 pointed to that on #2221. It is now: - Miller-Rabin to the first thirteen primes as bases. That is exact below psi13 = 3317044064679887385961981, the least strong pseudoprime to all thirteen (Sorenson and Webster, "Strong pseudoprimes to twelve prime bases", Math. Comp. 86 (2017)). The first twelve bases already suffice below 2^64. - Lucas-Lehmer for a Mersenne number 2^p - 1, after checking that p is prime, for p up to 5000. - Past psi13 and up to 4096 bits, a failed round still proves a number composite. A number that passes every round is left open, since passing is not a proof. 9223372036854775783 in PP is True in 81 ms, 2^89 - 1 is prime, and 10^30 + 1 is composite. 10^30 + 57, a prime past psi13, stays open, as does psi13 itself. The compiled PP membership calls the same test for any whole double. It was left open past 2^63. #2221's MembershipInASetOperationTest, and its BREAKING-CHANGES entry, used 2^89 - 1 as a number PP leaves open. Lucas-Lehmer now decides it, so both use 10^30 + 57 instead, with an interval that holds it, [0; 10^31], and the entry's values re-measured on 2.6.0 and on this build. PrimalityTest has 16 decided cases under a 30-second cap, among them the largest prime below 2^63, seven Mersenne numbers from 2^61 - 1 to 2^4423 - 1, the least strong pseudoprime to the first twelve bases, Carmichael numbers and base-2 strong pseudoprimes. It has two cases that stay open, every n below 200000 against a sieve, and 2000 random odd n below 10^12 against trial division. Fixes #2230. Co-Authored-By: Claude Opus 5.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
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.
Fixes #2219.
Membership in a union, an intersection and a set difference is now decided from each side's membership by Kleene's connectives.
The wrong answer.
Unionf.TryContainsreturned the right side's verdict whenever the left side did not say yes. So when the left side left membership open and the right side excluded the element, the union came outFalse.2^89 - 1is a Mersenne prime past the machine word, andPPleaves its membership open:(2^89 - 1) in (PP \/ [0; 1])False(2^89 - 1) in ([0; 1] \/ PP)(2^89 - 1) in ([0; 1] \ PP)False(2^89 - 1) in (PP \ [0; 10^30])FalseThe union is now Kleene's or: a member where either side decides it is one, outside where both sides decide it is not, and open otherwise.
The intersection and the difference were not wrong, but each decided only where both sides did. They are now Kleene's and, so an element is outside whatever the other side says when:
Contains.cspinned1 in {x} \ {1}as undecided. Since 1 is in{1}, it is outside the difference whateverxis, so that row now expects a decidedFalse. Every other row of that table is unchanged.Tests:
MembershipInASetOperationTesthas 17 cases, and 5 of them fail on master: the three union answers and the two differences. Full suite 17981/0, interactive trio, AOT smoke 72/0, all frameworks build.🤖 Generated with Claude Code