On 02/02/2018 03:26 PM, Tom Lane wrote:
> Tomas Vondra <tomas.vondra@2ndquadrant.com> writes:
>> ISTM this patch got somewhat stuck as we're not quite sure the
>> transformation is correct in all cases. Is my impression correct?
>
> Yeah, that's the core issue.
>
>> If yes, how to we convince ourselves? Would some sort of automated testing
>> (generating data and queries) help? I'm willing to spend some cycles on
>> that, if considered helpful.
>
> I'm not sure if that would be enough to convince doubters. On the other
> hand, if it found problems, that would definitely be useful.
>
OK, I'll take a stab at this, then. I wasn't really suggesting it might
prove definitely prove the transformation is correct - clearly, it can
only find counter-examples. But I think it's worth it anyway.
BTW wouldn't it be possible to derive "traditional" proof in relational
algebra, similarly to other transforms?
regards
--
Tomas Vondra http://www.2ndQuadrant.com
PostgreSQL Development, 24x7 Support, Remote DBA, Training & Services