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

Robert Haas <robertmhaas(at)gmail(dot)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