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

On Thu, Mar 8, 2018 at 6:24 PM, Tom Lane <tgl(at)sss(dot)pgh(dot)pa(dot)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