进一步退半步：无色任务的 FLP 式证明与轮数归约技术

本文比较了分布式计算中用于推导下界与不可能性结果的两种通用技术。首先，我们证明了一个加速定理（类似于 Brandt, 2019），针对无等待无色算法，旨在捕捉确立环的 3-着色轮数下界（Linial, 1992）的开创性轮数归约证明的本质，并采用逆向归纳。其次，我们考虑 FLP 式证明，旨在捕捉开创性的共识不可能性证明（Fischer, Lynch, and Paterson, 1985）的本质并使用正向归纳。我们表明，尽管这两种证明形式性质迥异，却紧密关联。特别地，我们证明对于每个无色任务 $\Pi$，若存在轮数归约证明确立无等待无色算法求解 $\Pi$ 的不可能性，则存在 FLP 式证明确立同一不可能性。对于一维无色任务（对任意进程数 $n\geq 2$），我们证明这两种证明技术具有完全相同的能力，且更重要的是二者皆完备：若一个一维无色任务不能被 $n\geq 2$ 个进程无等待求解，则该不可能性可由两种证明技术证得。此外，轮数归约证明可自动导出，且可从中自动生成 FLP 式证明。最后，我们通过确立任意维无色覆盖任务不能被无等待算法求解的不可能性，说明了这两种技术的运用。