I think ungrouping make sense if you consider reverse parentheses as a syntactic construct added to the language, and not replacing the existing parentheses.
For instance, using "] e [" as the notation for reverse parentheses around expression e, the second line showing reverse parenthese simplification, third line showing the
grouping after parsing, and the fourth line using postfix notation:
A + B * (C + D) * (E + F)
=> A + B * (C + D) * (E + F)
=> (A + (B * (C + D) * (E + F)))
=> A B C D + E F + * * +
A + ] B * (C + D) [ * (E + F)
=> A + B * C + D * (E + F)
=> ((A + (B * C)) + (D * (E + F)))
=> A B C * + D E F * + +
So what ungrouping would mean is to undo the grouping done by regular parentheses.
However, this is not what is proposed later in the article.
Possibilities include reversing the priority inside the reverse parentheses, or lowering the priority wrt the rest of the expression.
I believe you misread. My reading is that Gemini 3 gave a good result on a certain input, so they gave the same input to this model and the result was poor.
> A formally verified program can still have bugs, because the spec (which requires specialized skills to read and understand) may not satisfy the intent of the requirements in some way.
That's not a bug, that's a misunderstanding, or at least an error of translation from natural language to formal language.
Edit:
I agree that one can categorize incorrect program behavior as a bug (apparently there's such a thing as "behavioral bug"), but to me it seems to be a misnomer.
I also agree that it's difficult to tell that to a customer when their expectations aren't met.
In some definitions (that I happen to agree with but because we wanted to save money by first not properly training testers and then getting rid of them is not present so much in public discourse) the purpose of testing (or better said quality control) is:
1) Verify requirements => this can be done with formal verifications
2) Validate fit for purpose => this is where we make sure that if the customer needs addition it does not matter if our software does very well substraction and it has a valid proof of doing that according with specs.
I know this second part is kinda lost in the transition from oh my god waterfall is bad to yeyy now we can fire all testers because the quality is the responsibility of the entire team.
>an error of translation from natural language to formal language
Really? Programming languages are all formal languages, which means all human-made errors in algorithms wouldn't be "bugs" anymore. Some projects even categorize typos as bugs, so that's a unusually strict definition of "bug" in my opinion.
Sure, I guess you can understand what I said that way, but that's not what I meant. I wasn't thinking about the implementation, but the specifications.
Read again the quote I was refering to if you need better context to understand my comment.
If you have good formal specifications, you should be able to produce the corresponding code. Any error in that phase should be considered a bug, and yes, a typo should fit that category, if it makes the code deviate from the specs.
But an error in the step of translating the requirements (usually explained in natural language) to specifications (usually described formally) isn't a bug, it's a translation error.
I think it does indeed make a lot of sense in the particular example given.
But what if we add 2 extra nodes: n5 dependent on n2 alone, and n6 dependent on n3 alone? Should we keep n2 and n3 separate and split n4, or should we merge n2 and n3 and keep n4, or should we keep the topology as it is?
The same sort of problem arises in a class inheritance graph: it would make sense to merge classes n2 and n3 if n4 is the only class inheriting from it, but if you add more nodes, then the simplification might not be possible anymore.
Your comment is funny, but please note: it's not drawing a pelican riding a bike, it's describing in SVG a pelican riding a bike. Your candidate would at least displays some knowledge of the SVG specs.
I don't know what GP meant, but I can give an example of how I understand it (disregarding the spurious "the" in his comment): in a type system with sub-typing, your expression could be statically typed to return a certain type, and at runtime return any of its sub-types.
For instance, in typescript you could ascribe an expression with the type Any, yet the actual runtime type will not be Any, it will be any concrete type.
In object oriented languages, you may define a hierarchy of classes, say with "Car" and "Truck" being sub-classes of "Vehicle", each having a concrete implementation, and have an expression returning either a "Car" or a "Truck", or maybe even a "Vehicle". This expression will be statically typed as returning a "Vehicle", yet the dynamic type of the returned value will not necessary be (exactly) that.
reply