paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Proper Functors and Fixed Points for Finite Behaviour

有限行为的 proper 函子与不动点
LMCS vol.Volume 14, Issue 32018匹配度 1/10 · 论文属于余代数、范畴论与自动机理论的形式语义研究,关注 proper functor、有理不动点以及加权自动机的正则表达式演算,与用户研究方向(ML/Agent 程序的静态分析、LLM 与静态分析/形式化验证/浮点/贝叶斯程序分析的交叉)几乎没有直接交集。引用 1 inbox
Stefan Milius
crossref: 2026-09-10

AI 速览

一句话:引入 proper functor,证明其理性不动点是终结余代数的子余代数,用于余代数正则表达式演算的可靠性/完备性。

本文研究代数范畴上集合函子的理性不动点,它通常刻画有限余代数的行为,但在代数范畴上可能不再是完全抽象的,即未必是终结余代数的子余代数。受 Ésik 与 Maletti 的 proper semiring 概念启发,作者引入 proper functor。主要结果是:对 proper 函子,理性不动点可表示为所有以自由有限生成代数为载体对象的余代数的余极限,并且是终结余代数的子余代数;同时证明该余极限是终结余代数的子余代数当且仅当函子是 proper 的。这些结果为余代数正则表达式演算(如加权自动机)的可靠性与完备性证明提供技术工具。

问题
代数范畴上理性不动点可能不再是终结余代数的子余代数,因此有限行为无法由最终语义完全抽象地刻画。
方法
受 proper semiring 启发定义 proper functor,并用自由有限生成代数载体的余代数余极限刻画理性不动点。
评估
证明 proper 性与该余极限为终结余代数子余代数等价,并说明其对加权自动机等余代数正则表达式演算的可靠性/完备性有应用。
原文摘要(Abstract)

The rational fixed point of a set functor is well-known to capture the behaviour of finite coalgebras. In this paper we consider functors on algebraic categories. For them the rational fixed point may no longer be fully abstract, i.e. a subcoalgebra of the final coalgebra. Inspired by \'Esik and Maletti's notion of a proper semiring, we introduce the notion of a proper functor. We show that for proper functors the rational fixed point is determined as the colimit of all coalgebras with a free finitely generated algebra as carrier and it is a subcoalgebra of the final coalgebra. Moreover, we prove that a functor is proper if and only if that colimit is a subcoalgebra of the final coalgebra. These results serve as technical tools for soundness and completeness proofs for coalgebraic regular expression calculi, e.g. for weighted automata.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot373,
  title = {Proper Functors and Fixed Points for Finite Behaviour},
  author = {Stefan Milius},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 14, Issue 3},
  year = {2018},
  doi = {10.23638/lmcs-14(3:22)2018}
}