Re: [GENERAL] Question about partial functional indexes and the query planner

Brian Dunavant <brian(at)omniti(dot)com> writes:
> I am using a partial functional index on a table where F(a) = a. Querying
> whre F(a) = a hits the index as expected. However the reverse statement a
> = F(a) does not. I have verified this in 9.3.4.
> Is this a deficiency with the query planner, or are these not actually
> equivalent? I've been stumped on it.

Interesting. The reason this doesn't work is that predicate_implied_by()
fails to prove "a = b" given "b = a", at least in the general case.
It will figure that out if either a or b is a constant, but not if
neither one is. The fact that it works with constants might explain
the lack of previous complaints, but this is still pretty surprising
given the amount of knowledge about equality that the system evinces
otherwise. (I'm also wondering whether the EquivalenceClass logic
might not sometimes rewrite "a = b" into "b = a", causing a failure
of this sort even when the user *had* phrased his query consistently.)

It would be fairly straightforward to add a proof rule along the lines of
"if both expressions are binary opclauses, and the left input expression
of each one is equal() to the right input of the other, and the operators
are each other's commutators, then the implication holds".

An objection might be made that this would add noticeably to the cost of
failing proofs, but I think it wouldn't be that bad, especially if we did
the syscache lookup for the commutator check last. In most scenarios the
equal() checks would fail pretty quickly when the proof rule doesn't
apply. Also, I believe that in the case where a or b is a constant,
even though we can make the proof already, this approach would succeed
noticeably more quickly than btree_predicate_proof() can. (Worth noting
also is that predicate_implied_by() isn't even used unless you have
things like partial indexes involved, so that its cost is not especially
relevant to "simple" queries.)

I'd be inclined to add some similar proof rules to predicate_refuted_by,
along the lines of "a op1 b refutes a op2 b if op1 is op2's negator" and
"a op1 b refutes b op2 a if op1 is the negator of op2's commutator".
Again, the code is currently unable to make such deductions unless a or b
is a constant.

Given the lack of previous complaints, I'm not sure this amounts to
a back-patchable bug, but it does seem like something worth fixing
going forward.

regards, tom lane