Optimally Rewriting Formulas and Database Queries: A Confluence of Term Rewriting, Structural Decomposition, and Complexity

TL;DR

This paper presents an algorithm for minimizing the width of positive first-order sentences through syntactic rewriting, connecting term rewriting, query evaluation, and structural decomposition.

Contribution

It provides the first complete algorithmic framework for width minimization of first-order sentences using known equivalence-preserving rewriting rules.

Findings

Algorithm computes minimum-width equivalent sentences for positive first-order formulas.

Establishes a theoretical interface between term rewriting, query evaluation, and structural decomposition.

First to achieve such a comprehensive understanding in this general setting.

Abstract

A central computational task in database theory, finite model theory, and computer science at large is the evaluation of a first-order sentence on a finite structure. In the context of this task, the \emph{width} of a sentence, defined as the maximum number of free variables over all subformulas, has been established as a crucial measure, where minimizing width of a sentence (while retaining logical equivalence) is considered highly desirable. An undecidability result rules out the possibility of an algorithm that, given a first-order sentence, returns a logically equivalent sentence of minimum width; this result motivates the study of width minimization via syntactic rewriting rules, which is this article's focus. For a number of common rewriting rules (which are known to preserve logical equivalence), including rules that allow for the movement of quantifiers, we present an algorithm that, given a positive first-order sentence $\phi$, outputs the minimum-width sentence obtainable from $\phi$ via application of these rules. We thus obtain a complete algorithmic understanding of width minimization up to the studied rules; this result is the first one -- of which we are aware -- that establishes this type of understanding in such a general setting. Our result builds on the theory of term rewriting and establishes an interface among this theory, query evaluation, and structural decomposition theory.