Repository navigation
ConditionalSet should support extended definition #330
Description
Activity
Measured on
masterata45a7256, because the case for this is stronger than the issue body claims.The body says the quantifier encoding is "correct, [but] inconvenient for computers". It is not correct today — membership does not decide.
expression result 1 in { x : x > 0 }True4 in { y : x > 0 and y = x^2 }4 in { y : x > 0 and y = x ^ 2 }— unevaluated2 in { y : x > 0 and y = x^2 }2 in { y : x > 0 and y = x ^ 2 }— unevaluated4is in that set (takex = 2) and2is not (no positivexhasx² = 2…sqrt(2)does, so take2as a poorer example — the point stands for any value). Neither answers. A plainConditionalSetdecides membership fine; the moment the predicate carries a free variable standing in for the missing existential, it cannot, because nothing bindsx.So the workaround is not a slower route to the same answer, it is a non-answer. That makes this a gap in what
ConditionalSetcan express rather than an ergonomic wish, which I think is a stronger argument for the proposal than the one in the body.Two notes on shape, from adjacent work:
The transformation must be inside the binder.
{ f(x) : x : p(x) }bindsxand uses it in two places. #878 was exactly a bug of this kind — a set-builder's predicate was expanded as if it were an ordinary function argument, so its condition escaped the binder and{ x : 1/x = 0 }simplified to{ } provided not x = 0, where thatxwas not the bound one. Fixed in #879, but it is the failure mode this feature will re-open if the transformation is treated as just another child. Worth a test pinning that the transformation's own conditions stay inside.The syntax
{ f(x) : x : x > 0 }does not currently parse (UnhandledParseException), so it is free to take. Whatever is chosen, I would suggest holding it to printing and parsing back to the same tree —EveryNodeSurvivesEveryPipelineTestchecks that, andRationalandComplexare its only known failures (#873), so it is a property worth not adding a third exception to.I have not implemented anything here — flagging that the motivating example is a harder failure than recorded, in case that changes the priority.
It is preferable to follow the math and somehow interpret quantifiers instead.
I don't think any mathematician writes
{ f(x) : x : x > 0}or{ x : x : p(x)}. So let's just keep the nodes as close to how mathematicians express them. Part of v3 redesignIt is preferable to follow the math and somehow interpret quantifiers instead.
Done as of #1421 (
463f1688): the quantifiers exist and a set builder written the way the mathematics writes it now decides membership, which is what my earlier comment measured as the actual gap."4 in { y : exists x in RR : x > 0 and y = x^2 }".ToEntity().Simplify() // True "-4 in { y : exists x in RR : x > 0 and y = x^2 }".ToEntity().Simplify() // False "2 in { y : exists x in RR : x > 0 and y = x^2 }".ToEntity().Simplify() // True (x = sqrt(2)) "5 in { y : exists x in ZZ : x > 0 and y = x^2 }".ToEntity().Simplify() // False "3 in { y in ZZ : exists x in ZZ : y = 2 x + 1 }".ToEntity().Simplify() // True "4 in { y in ZZ : exists x in ZZ : y = 2 x + 1 }".ToEntity().Simplify() // False
Membership substitutes the candidate for
y, andexists x in RR : x > 0 and 4 = x^2is decided by the solver (solution set{2, -2}, one member positive). So the "extended definition" of the body —{ f(x) : x : p(x) }— is not needed for the use the issue names, and #322 is done independently in #1423 (images of intervals under monotone functions, products of intervals). What is still not done is the set itself as an object:{ y : exists x in RR : x > 0 and y = x^2 }is not rewritten to(0; +oo), which is the image computation the issue also wants and belongs to the same v3 design as thef(x)spelling.
Currently
Currently, it has
VarandPredicate, for example,{ x : x > 0 }. But what if we need every element to bef(x)?In math we would write
{ y : there exists x such that x > 0 and y = f(x) }Although it's correct, it's inconvenient for computers (and quantifiers are not yet supported).
Proposal
To add the
Transformationfor every element{ f(x) : x : x > 0}- the syntax is yet to be discussed, but the general idea should be clear.{ x : x : p(x)}is equivalent to current{ x : p(x) }(the old syntax will be kept).Usefulness
This will help to close #322 and #318.