Testbed for predtest.c ... and some arguable bugs therein

On Thu, Mar 8, 2018 at 12:33 AM, Tom Lane <tgl@sss.pgh.pa.us> wrote:

A bit of hacking later, I have the attached. The set of test cases it
includes at the moment were mostly developed with an eye to getting to
full code coverage of predtest.c, but we could add more later. What's
really interesting is that it proves that the "weak refutation" logic,
i.e. predicate_refuted_by() with clause_is_check = true, is not
self-consistent.

Oops.

I'm not sure that that's worth fixing right now. Instead I'm tempted
to revert the addition of the clause_is_check argument to
predicate_refuted_by, on the grounds that it's both broken and currently
unnecessary.

Hmm, I think you were the one who pushed for adding that argument in
the first place: /messages/by-id/31878.1497389320@sss.pgh.pa.us

I have no problem with taking it back out, although I'm disappointed
that I failed to find whatever was broken about it during review.

--
Robert Haas
EnterpriseDB: http://www.enterprisedb.com
The Enterprise PostgreSQL Company

Robert Haas <robertmhaas@gmail.com> writes:

On Thu, Mar 8, 2018 at 12:33 AM, Tom Lane <tgl@sss.pgh.pa.us> wrote:

I'm not sure that that's worth fixing right now. Instead I'm tempted
to revert the addition of the clause_is_check argument to
predicate_refuted_by, on the grounds that it's both broken and currently
unnecessary.

Hmm, I think you were the one who pushed for adding that argument in
the first place: /messages/by-id/31878.1497389320@sss.pgh.pa.us

I'm kind of disappointed that you failed to take the *other* advice
in that message, as I still think that clause_is_check is a poor
choice of name for the flag. It could have been salvaged with a
clear comment defining the semantics, but that's not there either.

I have no problem with taking it back out, although I'm disappointed
that I failed to find whatever was broken about it during review.

Maybe I'll spend a few minutes trying to isolate why the current
results are wrong. However, it's certainly arguable that we shouldn't
spend much time on this with no use-case in sight.

regards, tom lane

Robert Haas <robertmhaas@gmail.com> writes:

On Thu, Mar 8, 2018 at 12:33 AM, Tom Lane <tgl@sss.pgh.pa.us> wrote:

A bit of hacking later, I have the attached. The set of test cases it
includes at the moment were mostly developed with an eye to getting to
full code coverage of predtest.c, but we could add more later. What's
really interesting is that it proves that the "weak refutation" logic,
i.e. predicate_refuted_by() with clause_is_check = true, is not
self-consistent.

Oops.

After further navel-gazing, I've concluded that my initial opinion of the
"correct" semantics for weak refutation was wrong. When I revise the
test logic to follow my revised understanding, it no longer claims that
any proofs are mistaken, although there are still things that could be
proven and aren't being. Let me summarize my thoughts here for the
record.

For predicate_implied_by, we have two plausible definitions of
implication:

* "strong" form: A implies B if truth of A implies truth of B.
We need this to prove that a row satisfying one WHERE clause or
index predicate must satisfy another one.

* "weak" form: A implies B if non-falsity of A implies non-falsity of B.
We need this to prove that a row satisfying one CHECK constraint
must satisfy another one.

We could conceivably use a third proof rule that tries to prove
non-falsity of B from truth of A, but AFAICS there are no places in
the current code that need exactly that behavior, and the "strong" rule
seems like an adequate substitute unless such a need becomes mainstream.
(There aren't that many cases where we could prove something per this rule
but not per the strong rule, anyway.)

The fourth possible proof rule is to prove truth of B from non-falsity
of A, but the number of cases where you can make such a proof is so
small that this option isn't actually interesting in practice.
(For instance, you can't even conclude "X implies X" with such a rule.)

On the predicate_refuted_by side, I was confused about how to choose
among some similar options:

* R1: A refutes B if truth of A implies falsity of B.

* R2: A refutes B if truth of A implies non-truth of B.

* R3: A refutes B if non-falsity of A implies non-truth of B.

* R4: A refutes B if non-falsity of A implies falsity of B.

We can discard R4, again because there are too few cases where we
could prove anything per that rule, eg NOT X wouldn't refute X
or vice versa.

R1 is the traditional behavior of predicate_refuted_by, and as its
comment says, is needed because we want to disprove a CHECK
constraint (ie prove it would be violated) given a WHERE clause.

R2 is of use for disproving one WHERE clause given another one.
It turns out that of the two extant calls to predicate_refuted_by,
one of them would actually like to have that semantics, because
it's looking for mutually contradictory WHERE clauses. We've been
getting by with R1 for that, but R2 would let us optimize some
more cases.

R3 could be of use for disproving a WHERE clause given a CHECK constraint,
and is the one I'd supposed should be the alternate behavior of
predicate_refuted_by. However, we have no actual use cases for that;
relation_excluded_by_constraints goes the other way.

Moreover, although R3 seems like it'd be the more tractable rule on
grounds of symmetry, it's looking to me like R2 is about equivalent
for proof purposes. For instance see the code near predtest.c:700,

* If A is a strong NOT-clause, A R=> B if B equals A's arg
*
* We cannot make the stronger conclusion that B is refuted if B
* implies A's arg; that would only prove that B is not-TRUE, not
* that it's not NULL either. Hence use equal() rather than
* predicate_implied_by_recurse(). We could do the latter if we
* ever had a need for the weak form of refutation.

The previous patch to add weak implication rules missed the opportunity
for improvement here. If we are using R1 or R2, then we have the
assumption "NOT A is true", allowing us to conclude A is false. Then,
if we can prove B implies A under weak implication (not-false B implies
not-false A), we have proven B must be false, satisfying the proof rule for
R1. But also, if we can prove B implies A under strong implication (true
B implies true A), we have proven B is not true, satisfying the proof rule
for R2. So in either case there's potential to recurse to
predicate_implied_by rather than only being able to handle the tautology
"NOT A refutes A".

Now, the same logic would go through if we were using R3. We'd be
starting with non-falsity of "NOT A", only allowing us to conclude
non-truth of A, but a proof of strong B => A would still let us conclude
B is not true, satisfying R3.

Alternatively, consider if we were starting with A and trying to refute
NOT B. Intuitively you'd figure that if you can prove A => B, that oughta
be enough to refute NOT B. That certainly works for R1 with strong
implication: truth of A implies truth of B implies falsity of NOT B.
And it works for R2 with either type of implication: truth of A implies
(at least) non-falsity of B which implies non-truth of NOT B. For R3,
you'd need weak implication: non-falsity of A implies non-falsity of B
implies non-truth of NOT B. Now generally, strong implication is easier
to prove than weak implication (cf. existing handling of clause_is_check
in predtest.c), so R2 is marginally better in this case.

So my initial feeling that we ought to define predicate_refuted_by's
alternate behavior as R3 seems wrong: we're better off with R2, which
matches present needs better and is roughly equally tractable as far
as the actual proof logic goes.

I propose to change test_predtest so that what it checks for as
"w_r_holds" is R2 not R3, and to improve the documentation in predtest.c
about this, and maybe to fix some of the cases where we can do better
by adding mutual recursion between the "implied" and "refuted" cases.
I feel a little guilty about taking time out of the commitfest to deal
with this, but I'd rather get it done while this reasoning is still
swapped in.

regards, tom lane

On Thu, Mar 8, 2018 at 6:24 PM, Tom Lane <tgl@sss.pgh.pa.us> wrote:

* R1: A refutes B if truth of A implies falsity of B.
* R2: A refutes B if truth of A implies non-truth of B.
* R3: A refutes B if non-falsity of A implies non-truth of B.
* R4: A refutes B if non-falsity of A implies falsity of B.

The use of the terms "refutes", "non-truth", and "non-falsity" drive
me a little batty; they've all got an internal negation built into
them, and that's confusing. It seems very tempting to propose getting
rid of predicate_refuted_by altogether and to simply have one
function:

if we know that everything in clause_list is { true | false } [ or
null ], does that imply that everything in predicate_list must be {
true | false } [ or null ]?

Internally, we could represent what we know about various clauses by
some combination of CLAUSE_MIGHT_BE_TRUE = 0x01, CLAUSE_MIGHT_BE_FALSE
= 0x02, CLAUSE_MIGHT_BE_NULL = 0x04. I have a feeling this might work
out to be a lot easier to understand than what we've got now, because
saying that "A weakly refutes B" is a heck of a lot less clear, at
least in my book, than saying "If A is true or null, B must also be
true or null."

I realize this is all a little to one side of what you're talking
about here, but the fact that even you got confused about whether the
existing logic was correct, and that you found that there were
multiple possible definitions of what "correct" means, seems like
pretty good evidence that this is not as clear as it could be.

--
Robert Haas
EnterpriseDB: http://www.enterprisedb.com
The Enterprise PostgreSQL Company

Robert Haas <robertmhaas@gmail.com> writes:

The use of the terms "refutes", "non-truth", and "non-falsity" drive
me a little batty; they've all got an internal negation built into
them, and that's confusing. It seems very tempting to propose getting
rid of predicate_refuted_by altogether and to simply have one
function:

if we know that everything in clause_list is { true | false } [ or
null ], does that imply that everything in predicate_list must be {
true | false } [ or null ]?

I don't think that's terribly practical, because the proof rules are
different. To prove an AND condition true, you must prove all its
elements true; to prove it false, you need only prove one element
false. The reverse for OR. No doubt we could physically merge the two
functions, but I do not think it'd end up being any sort of improvement.

saying that "A weakly refutes B" is a heck of a lot less clear, at
least in my book, than saying "If A is true or null, B must also be
true or null."

Well, I beg to differ. Once you've internalized the definitions, the
former is a lot shorter. Or in other words: programming is all about
inventing a suitable notation for expressing your thoughts.

I realize this is all a little to one side of what you're talking
about here, but the fact that even you got confused about whether the
existing logic was correct, and that you found that there were
multiple possible definitions of what "correct" means, seems like
pretty good evidence that this is not as clear as it could be.

To my mind, the pre-v10 logic was fine, and the confusion was created
by muddled thinking while introducing the weak proof rules. What we're
trying to do now is pin down exactly what the weak rules need to be
so we can document them properly. It's conceivable that a different
code-level representation of the rules would be clearer, but I'm not
convinced of that, and anyway there's no hope of finding such a
representation when we don't have the rules straight.

As an example of the sort of documentation I'm thinking of, here's
what I've written so far about why operator_predicate_proof isn't
already broken:

* We mostly need not distinguish strong vs. weak implication/refutation here.
* This depends on an assumption (which we cannot check) that a pair of
* related operators will not return one NULL and one non-NULL result for the
* same inputs. Then, for the proof types where we start with an assumption
* of truth of the clause, the predicate operator could not return NULL
* either, so it doesn't matter whether we are trying to make a strong or weak
* proof. For weak implication, it could be that the clause operator returned
* NULL, but then the predicate operator would as well, so that the weak
* implication still holds. This argument doesn't apply in the case where we
* are considering two different constant values, since then the operators
* aren't being given identical inputs. But we only support that for btree
* operators, for which we can assume that all non-null inputs result in
* non-null outputs, so that it doesn't matter which two non-null constants
* we consider. Currently the code below just reports "proof failed" if
* either constant is NULL, but in some cases we could be smarter.

(I expect the last sentence, as well as the code, will get some revisions
arising from the "constraint exclusion and null values" thread; but this
is correct today.)

I don't really think this would be any clearer if I'd avoided the
implication/refutation jargon.

regards, tom lane