不动点理论 -- 倒置
摘要：Knaster-Tarski定理将一个单调函数在完备格上的最大不动点特征化为最大后不动点，自然地引出了所谓的共归证明原则，用于证明某个元素在最大不动点下方（例如，提供相似性证书）。用于证明一个元素在最小不动点上方的对偶原则与归纳不变量有关。本文提供了类似精神的证明规则，用于显示一个元素位于最大固定点之上，或者对偶地位于最小固定点之下。该理论是针对适当的形式$mathbb{M}^Y$上的非扩展单调函数（其中$Y$是有限集，$mathbb{M}$是MV代数）的格子的，它基于原始函数的（有限）近似的构造。我们展示了我们的理论适用于各种例子，包括终止概率、度量转换系统、概率自动机的行为距离和相似性。此外，它还允许我们确定解决简单随机博弈的原始算法。
作者：Paolo Baldan, Richard Eggert, Barbara K"onig, Tommaso Padoan
论文ID：2101.08184
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-07