On 02/02/2018 03:26 PM, Tom Lane wrote: > Tomas Vondra <tomas.von...@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