paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Operations on Fixpoint Equation Systems

不动点方程系统上的操作
LMCS vol.Volume 20, Issue 32024匹配度 4/10 · 该论文研究完备格上不动点方程系统在代入、重排等操作下的解保持条件，属于静态分析与形式验证的基础理论，与用户关注的形式化/静态分析理论有间接联系；但它不涉及 LLM/Agentic、浮点程序分析或贝叶斯程序分析，因此与当前核心研究方向匹配度有限。引用 0 inbox
Thomas Neele, Jaco van de Pol
形式语义定理证明与证明工程
crossref: 2026-09-10

AI 速览

一句话：研究完备格上不动点方程系统在变量代入、方程重排等操作下解保持不变的条件，并提供机器检查证明。

本文研究任意完备格上的不动点方程系统（FES），关注对其施加操作后解是否保持不变。具体考察将变量替换为其定义、交换方程顺序等操作，分析这些操作保持 FES 解的充分条件。作者给出严格且经计算机检查的证明，并在过程中系统整理完备格中极值不动点的若干已知与新恒等式和不等式。该工作为不动点方程系统的代数操作提供了严格且机器验证的基础。

问题
在任意完备格上，对不动点方程系统进行变量代入、方程重排等操作时，何种条件下仍保持原系统的解？
方法
以完备格上的极值不动点理论为框架，形式化定义相关操作，并用计算机检查的证明建立保持解的条件，同时整理不动点的恒等式与不等式。
评估
通过机器检查的证明验证所有结论，而非实验评估；结果为操作保持解的条件及若干不动点代数性质。
原文摘要（Abstract）

We study operations on fixpoint equation systems (FES) over arbitrary complete lattices. We investigate under which conditions these operations, such as substituting variables by their definition, and swapping the ordering of equations, preserve the solution of a FES. We provide rigorous, computer-checked proofs. Along the way, we list a number of known and new identities and inequalities on extremal fixpoints in complete lattices.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@article{paperbot2744,
  title = {Operations on Fixpoint Equation Systems},
  author = {Thomas Neele and Jaco van de Pol},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 20, Issue 3},
  year = {2024},
  doi = {10.46298/lmcs-20(3:5)2024}
}