格局上的固定点游戏证据

我们构造了可用于推导固定点游戏中策略的证据，并证明函数的最小固定点要么位于某个给定界限之上，要么不位于其下方。我们采用格论方法，包括一种 Galois 联系，将代表“逻辑宇宙”的格（其中证据居住）与代表“行为宇宙”的格相连接（函数在其上定义）。事实上，我们考虑了两种类型的游戏—— primal 游戏和 dual 游戏——并在两种情况下展示了如何从证据中推导获胜策略，以及如何从策略中构造证据。两种游戏在规则和格的基选择方面存在差异。该理论可实例化于已知示例：特别是我们与标准二分相似性中区分公式的构造以及概率系统的行为度量进行比较。作为一种新案例，我们考虑用于证明马尔可夫链终止概率下界的证据。