A Strategy for Dynamic Programs: Start over and Muddle Through
A Strategy for Dynamic Programs: Start over and Muddle Through
复制标题
DOI：
10.23638/lmcs-15(2:12)2019
复制
发表时间：
2017-04
期刊：
影响因子：
--
通讯作者：
Samir Datta;A. Mukherjee;T. Schwentick;N. Vortmeier;T. Zeume
中科院分区：
文献类型：
--
作者：
Samir Datta;A. Mukherjee;T. Schwentick;N. Vortmeier;T. Zeume
在 DynFO 的设置中，只要底层数据发生变化，动态程序就会更新查询的存储结果。这种更新用一阶逻辑表示。我们介绍了一种构建动态程序的策略，它利用了从头开始定期计算辅助数据以及在有限的变化步骤中保持查询的能力。我们证明，如果某个程序能在可计算的 AC$^1$ 初始化后保持查询对数 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.