Incorrect behavior of || in list comprehension

[BastiaanHeeren]

Operator || behaves incorrectly in a list comprehension (probably caused by the operator's backtracking behavior).

rascal>[ x | x <- [0..10], true || true ]
list[int]: [0,0,1,1,2,2,3,3,4,4,5,5,6,6,7,7,8,8,9,9]

This result is incorrect: true || true should ALWAYS be semantically equivalent to true (i.e. give the same result).

Suggested fix if backtracking semantics turns out to be (too) complex: let && and || be the standard (boolean) operators, and introduce new operators (&&& and ||| come to mind) for the more experimental features.

[jurgenvinju]

Thanks for the report Bastiaan; we need to either clarify or fix this.

@PaulKlint interesting to see what the compiler makes of this right now.

[jurgenvinju]

to comment and separate some issues:

• true || true does evaluate to true and is functionally semantically equivalent to true in the current implementation
• due to the semantics of || there are possibly three ways of making the || evaluate to true (either the left hand side or the right hand side or both, and given nested boolean expressions which are not-unitary either (say a list match) there may be many different ways to arrive at true which must be iterated over.
• however, the side-effect of repeatedly evaluating true || true, searching for different valuations and variable bindings for the left hand and the right hand of ||, even though there are no different bindings, is that the left hand side of the comprehension is repeatedly executed.

So here we see that the operational semantics of backtracking over boolean expression operands interferes with the natural semantics of the boolean expression.

Either we make completely predictable how often true || true should be executed for every binding of x, or we make sure that in case of the absence of backtracking, such a boolean expression is evaluated only once, or at least the left hand side of the comprehension or the right hand side of a for-loop are executed only once for every unique variable binding.

I suspect that fixing this in the interpreter is really complex, while the compiler may have enough static analysis capabilities to "do this right"..

[jurgenvinju]

One explanatory one-liner would be: a comprehension condition is a generator of bindings, and that the comprehension semantics should iterate over all distinguishable bindings at least once, and also maximally once.

Bastiaan reports that this is not true because true || true generates exactly one kind of binding (the empty environment), and not two as we can see in the output example. It iterates more than once over the same environment. From this perspective we have a bug.

Another simple explanatory one-liner would be that: "the comprehension iterates as many times as the algorithm backtracks". This would make the current bug a "feature". But, I find it quite unsatisfactory that such an algorithmic detail seeps into the formal semantics of the Rascal language. Also this would prohibit different implementation strategies that skip or optimize false valuations (for example by short-circuiting the && or using other meta-information about pattern matching and static types and grammatical reachability for deep matching)

The previous one-liner which focuses on unique bindings (including the empty environment) allows for many different implementation strategies which can be compared on efficiency, but would all result in the same amount of elements in the list comprehension.