Clarify potential uses for implies

[JLLeitschuh]

Clarify how if .. then .. else can be equivalent to implies in certain scenarios.

[p0]

This is exactly right -- it is desugared in this way internally. 👍

[p0]

This is not quite right. It means the same, but is not operationally equivalent.

The desugaring for if A then B else C is in fact (A and B) or ((not A) and C). Thus, if C is any(), the if/then/else desugars to (A and B) or (not A). We can distribute the terms to see this is equivalent to (A or (not A)) and (B or (not A)), which simplifies to (not A) or B, so logically they are the same.

Practically, however, it may be that (A and B) is much faster to evaluate than just B -- perhaps A has very few tuples, while B has very many, and so it's faster to just check whether B holds of the tuples in A rather than enumerating all the tuples in B. Or, in other words, writing if A then B else any() evaluates the then part only for contexts that satisfy the condition, while this constraint does not exist in A implies B.

[You might argue that we should therefore desugar A implies B to (not A) or (A and B), but that can be worse if A in fact does not significantly restrict the values in B, and therefore it would be a potentially breaking change. Still, it might be less surprising. 🤔]

Suggested change

	* ``A implies B`` is the same as writing ``if A then B else any()``.
	* ``A implies B`` means the same as writing ``if A then B else any()``, though the latter is in fact evaluated as ``A implies (A and B)``.

[p0]

... I'm actually not sure whether we want this kind of operational detail in the language reference -- how do others feel?

[p0]

Suggested change

	``if A then B else any()`` can also be represented as `A implies B`.
	``if A then B else any()`` can also be represented as ``A implies (A and B)``, and it means the same as ``A implies B``.

(See my other comment for explanation.)

[jbj]

I suggest not adding this line at all since it encourages the use of implies. Use of implies tends to be confusing to readers who weren't in exactly the same frame of mind as the author. I'm fine with giving hints in the other direction, suggesting how to replace implies with either or or if.

[jbj]

We sometimes rewrite implies to the if form manually for performance reasons. That trick is probably worth mentioning somewhere, but I'm not sure the QL language reference is the ideal place. If we should mention it here, it should be clearly marked as an optimisation trick that may be manually applied.

[jbj]

While A implies B is logically equivalent to if A then B else any(), they're not equivalent as QL formulas for all purposes. The most important differences are:

1. They generate different code and can therefore have different performance. The if expansion duplicates the A formula (see line 333 of this file), while the or expansion does not. Having an extra copy of A could make execution slower (because there is more code to run) or faster (because more optimisations may apply to B when it's in the context of A and B).
2. The various checks applied to a QL program will behave slightly differently in the two cases. The or expansion is anti-monotonic in A, while the if expansion is non-monotonic. I'm fairly confident that the two expansions can also give different binding check results in edge cases, and QL's checks for empty formulas might also apply slightly differently.

As an example of how monotonicity is different, consider this predicate, which is a convoluted way to write i = [1,2,3,4]:

predicate foo(int i) {
    i < 5 and
    (not foo(i-1) implies i = 1)
}

If you use the if expansion of implies, then the program no longer compiles.

[JLLeitschuh]

There seems to be a lot of debate on my PR about my update to the explanation around ``implies``.

It doesn't seem clear to me what the "best" way to express if .. then .. else any() in codeQL. I'm just looking for an easy way to communicate: if 'predicate holds' then 'this predicate must also hold' else 'give me everything'. I want to communicate this in CodeQL in a way that is easy to understand and interpret.

Given this, what would you like to see the documentation changed to?

[aschackmull]

It doesn't seem clear to me what the "best" way to express if .. then .. else any() in codeQL. I'm just looking for an easy way to communicate: if 'predicate holds' then 'this predicate must also hold' else 'give me everything'. I want to communicate this in CodeQL in a way that is easy to understand and interpret.

The if .. then .. else any() matches up directly with your sentence "if 'predicate holds' then 'this predicate must also hold' else 'give me everything'", so if that's what you want to communicate, then that piece of QL seems fine. Anecdotally, I also think this tends to perform a bit better than implies in most cases (although this isn't clear-cut).

Given this, what would you like to see the documentation changed to?

I don't see the need to change the documentation here - both if .. then .. else .. and implies seem to be adequately explained, and I don't think a discussion of if A then B else any() vs. A implies B belongs here. It's true that it is an interesting comparison with some subtlety as discussed in the various comments above, but it is also fairly corner-case, and I'm not sure it needs explicit mention outside of, say perhaps, as an example in some highly technical performance debugging deep-dive.

I suggest just closing this PR.

[JLLeitschuh]

Personally, I think that if A then B else any() should be discussed somewhere even if it's not in the context of implies. It took a bit of brain rattling to figure out how to create the predicate I was attempting to generate. Maybe this is better documented under if .. then .. else ..?

[aschackmull]

Maybe this is better documented under if .. then .. else ..?

I'm not sure what else you'd expect in the documentation? if A then B else C seems perfectly adequately documented, so I don't know why we'd want to special-case C = any().

[owen-mc]

I agree with @JLLeitschuh . any() is not something that a relatively new user would be familiar with, and this is one of the first times they might want to use it. Could we add a line to the end of the if-then-else section like:

Note that when no restriction is required in the else case, the built-in predicate any() may be used: if A then B else any()?

[aschackmull]

Right, I see what's missing now, we're not actually documenting the "true" (any()) and "false" (none()) in the list of logical connectives. In fact, the only mention of none() is in an example that's blatantly wrong (it's not valid QL). PR with a suggested fix: #8701

[aschackmull]

If we still want to mention something like if A then B else any() then I think it fits better as an example in the section on any().