Re: Optimization rules for semi and anti joins

Hello,

On Tue, Feb 10, 2009 at 09:41:46PM +0100, Dimitri Fontaine wrote:
> Hi,
>
> Le 10 févr. 09 à 21:10, Tom Lane a écrit :
>
>> I wrote (in response to Kevin Grittner's recent issues):
>>> Reflecting on this further, I suspect there are also some bugs in the
>>> planner's rules about when semi/antijoins can commute with other
>>> joins;
>>
>> After doing some math I've concluded this is in fact the case. Anyone
>> want to check my work?
>
> I don't know how easy it would be to do, but maybe the Coq formal proof
> management system could help us here:
> http://coq.inria.fr/
>
> The harder part in using coq might well be to specify the problem the
> way you just did, so...

formal theorem proving and mechanized mathematics happen to be one of
my research topics in the last few years; so I think that my
experience could be helpful with such problems.

(Actually instead of Coq I use HOL Light, whereas other people in my
research group work with Coq; but both of them are for the same
purpose)

Perhaps a way to begin would be to start writing a formalization of
the above rules, in order to assess the problem quickly, and then to
get back to pg-hackers soon.

Any comments/warnings/suggestions ?

Thank you,
Dr. Gianni Ciolli - 2ndQuadrant Italia
PostgreSQL Training, Services and Support
gianni(dot)ciolli(at)2ndquadrant(dot)it | www.2ndquadrant.it