The goal of the COKO-KOLA project [10, 91 is to express rules of rule-basedoptimizers in a mannerpermitting verification with a theoremprover. In [IO], we consideredquerytransformationsthatweretoogeneral to be expressedwith rewrite rules. In this paper,we considerthe complementaryissueof expressingquery transformationsthat aretoo specific for rewrite rules. Suchtransformationsrequirerewriterulesto besupplementedwith semanticconditions to guardrule firing. This work considerstheexpressionof suchtransformationsusingconditional rewriterules,andtheexpression of inferencerules to guide the optimizer in deciding if semanticconditions hold. This work differs from existing work in semanticquery optimization in that semantictransformationsin our frameworkareverifiable with a theoremprover. Further, our use of inference rules to guidesemanticreasoningmakesour optimizer extensiblein amannerthat is complementaryto theextensibility benefitsof existing rule-basedtechnology.
Mitch Cherniack, Stanley B. Zdonik