[red-knot] Should A ∧ !A always be false?

[dcreager]

This mimics a simplification we have on the OR side, where we simplify A ∨ !A to true. Should the dual hold for AND? We currently get a couple of test case regressions with in place.

[carljm]

I don't think this holds, because we are dealing with three-valued logic (there is the Ambiguous possibility), and a value of Ambiguous truthiness can change truthiness between one time it is checked and another.

Multiple checks of the truthiness of the same condition only occur in while loops, which is why all of the test failures occur in while-loop tests. This PR models the premise that a while-loop test can never change truthiness over time, which would indeed lead to the conclusion seen in the test failures, that a while loop with no break must either be never entered at all, or must be an infinite loop once entered.

I think in order for this PR to be valid, we would need to create two separate visibility constraints for the same while-loop test expression, one for "as checked on first entry" and another for "as checked on subsequent iteration", so that we wouldn't actually see those as "the same constraint", and would thus model the possibility of entering the loop and then leaving it on a later iteration. (I think this same change in while loop visibility constraints would be necessary if we switch to BDDs for visibility constraints.)

I think technically the existing OR simplification is wrong for the same reason? But in practice it doesn't cause a problem, either because the OR simplification case doesn't arise with while loops, or because simplifying to ALWAYS_TRUE doesn't lead us to eliminate paths as unreachable, or for both reasons.

[carljm]

cc @sharkdp, you might find this interesting.

[dcreager]

a value of Ambiguous truthiness can change truthiness between one time it is checked and another.

Yep, that makes sense! The part that I wasn't sure about was what the scope of "one time it is checked and another" is. My intuition would be that a literal (in the boolean formula sense, not the Python source sense) might evaluate to Ambiguous, meaning that we don't know if it's true or false — but that within the context of a particular evaluation of the boolean formula, it would have the same true or false value each time it appears. Which would make A ∧ !A == 0 hold.

Multiple checks of the truthiness of the same condition only occur in while loops, which is why all of the test failures occur in while-loop tests.

Or put another way, while-loop tests are the only place (at least for now) where we need a visibility constraint to model the relationship between two different states in the execution trace of the program.

I think technically the existing OR simplification is wrong for the same reason?

Definitely agree — and I think that's a better wording of my question! 😄 Either both A ∧ !A == 0 and A ∨ !A == 1 should hold, or neither should.

[carljm]

within the context of a particular evaluation of the boolean formula, it would have the same true or false value each time it appears

The problem is that we construct boolean formulae (for visibility of paths through a while loop) which contain a single constraint that represents checks of the while-test expression's truthiness at different points in execution state (first entry vs later iteration). Because we do this, we create the scenario that "the same constraint" in the same boolean formula doesn't necessarily have a consistent truthiness value, even for a single evaluation of the formula.

If we instead created separate visibility constraints (referring to the same test expression) for the truthiness checks in these two different execution states, then the simplification would hold. (I think this change in the semantic index builder's handling of while loops would not be too difficult, but I haven't tried to make the change.)

[carljm]

Once we model the back-edge in control flow in a while loop, we could even evaluate the test expression under two different conditions, one without the back-edge (for first entry) and one with the back-edge (for later iteration). This could change our evaluation of its static truthiness, too. (Imagine an x = True; while x: x = get_bool().)