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 $φ$, outputs the minimum-width sentence obtainable from $φ$ 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.

翻译：在数据库理论、有限模型理论乃至整个计算机科学中，一个核心的计算任务是在有限结构上评估一阶语句。在此任务背景下，语句的\emph{宽度}（定义为所有子公式中自由变量的最大数量）已被确立为一个关键度量，其中最小化语句的宽度（同时保持逻辑等价）被认为是高度可取的。一个不可判定性结果排除了存在一种算法的可能性：该算法在给定一个一阶语句时，能返回一个逻辑等价的最小宽度语句；这一结果促使我们通过语法重写规则来研究宽度最小化，这正是本文的重点。对于一系列常见的重写规则（已知这些规则能保持逻辑等价），包括允许量词移动的规则，我们提出了一种算法：给定一个正一阶语句 $φ$，该算法输出通过应用这些规则可从 $φ$ 获得的最小宽度语句。由此，我们获得了对所研究规则范围内宽度最小化的完整算法理解；据我们所知，这是在如此一般性设定下首次确立此类理解的结果。我们的结果建立在项重写理论的基础上，并在该理论、查询评估与结构分解理论之间建立了一个接口。