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.

翻译：数据库理论、有限模型理论以及整个计算机科学中的一个核心计算任务是在有限结构上评估一阶句子。在此任务背景下，句子的宽度（定义为所有子公式中自由变量的最大数量）已被确立为一个关键度量，其中最小化句子的宽度（同时保持逻辑等价性）被视为高度期望的目标。一个不可判定性结果排除了存在一种算法的可能性，该算法给定一阶句子后能返回逻辑等价的具有最小宽度的句子；这一结果激发了通过句法重写规则进行宽度最小化的研究，这正是本文的焦点。针对若干常见的重写规则（已知能保持逻辑等价性），包括允许量词移动的规则，我们提出了一种算法，该算法给定正一阶句子 φ 后，输出通过应用这些规则从 φ 可获得的最小宽度句子。因此，我们获得了在所研究规则下宽度最小化的完整算法理解；据我们所知，这是首次在这种通用设定下建立此类理解的结果。我们的结果建立在项重写理论之上，并建立了该理论、查询评估与结构分解理论之间的接口。