一句话：提出构造 DynFO 动态程序的“重算+有限步维护”策略，将 AC^1 初始化后 log n 步能力化为 DynFO。
论文研究 DynFO 框架中动态程序的构造问题：数据变化时，程序需用一阶逻辑更新查询结果。作者提出一种策略，周期性从头计算辅助数据，并仅在有限变化步内维护查询；证明若某程序在 AC^1 可计算初始化后能维护查询 log n 步，则该查询可由一阶动态程序维护，即属于 DynFO。作为应用，若变化序列产生的图始终有界树宽，则由一元二阶（MSO）公式定义的判定与优化问题属于 DynFO。为证明该结果，还建立了一个 MSO 的 Feferman–Vaught 型组合定理，其本身也可能有独立价值。
In the setting of DynFO, dynamic programs update the stored result of a query whenever the underlying data changes. This update is expressed in terms of first-order logic. We introduce a strategy for constructing dynamic programs that utilises periodic computation of auxiliary data from scratch and the ability to maintain a query for a limited number of change steps. We show that if some program can maintain a query for log n change steps after an AC$^1$-computable initialisation, it can be maintained by a first-order dynamic program as well, i.e., in DynFO. As an application, it is shown that decision and optimisation problems defined by monadic second-order (MSO) formulas are in DynFO, if only change sequences that produce graphs of bounded treewidth are allowed. To establish this result, a Feferman-Vaught-type composition theorem for MSO is established that might be useful in its own right.
@article{paperbot795,
title = {A Strategy for Dynamic Programs: Start over and Muddle through},
author = {Samir Datta and Anish Mukherjee and Thomas Schwentick and Nils Vortmeier and Thomas Zeume},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 2},
year = {2019},
doi = {10.23638/lmcs-15(2:12)2019}
}