paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Fixed Point Logics on Hemimetric Spaces

半度量空间上的不动点逻辑
LICS 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2023匹配度 2/10 · 该论文研究 µ-演算在半度量空间上的度量完备性与混合缠结的表达力,属于纯逻辑/拓扑形式语义,与用户关注的可用于程序分析、LLM/Agent 交叉、浮点或贝叶斯程序分析等方向几乎没有直接交集。仅在形式化验证的逻辑基础层面存在非常间接的关联。引用 3 inbox
David Fernández-Duque, Quentin Gougeon
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话:在更广的半度量空间上建立 wK4 及相关逻辑的度量完备性,并提出混合缠结以刻画 µ-演算的表达力。

µ-演算可在度量空间上解释,并具有 McKinsey-Tarski 完备性定理和 Dawar-Otto 模态刻画定理的变体;但在不满足基本分离公理的空间中,基模态逻辑不是 K4 而是较弱的 wK4,相关结果失效。本文把语义推广到更广的半度量空间,证明 wK4 及相关逻辑的度量完备性。作者指出 Dawar-Otto 定理仍然失效源于缠结导数在任意拓扑空间中定义不当,因而引入混合缠结:它在度量空间上与缠结导数一致,但在一般情况下表现更好。最后证明只有混合缠结足以定义有限结构的可模拟性,这是 µ-演算表达完备片段的关键测试用例。

问题
经典 µ-演算的度量/拓扑语义结果依赖于分离公理;在不满足基本分离性的空间中,基模态逻辑变为较弱的 wK4,且现有完备性与 Dawar-Otto 刻画失效。
方法
将语义推广到半度量空间,证明 wK4 及相关逻辑的度量完备性,并引入混合缠结(hybrid tangle)替代缠结导数。
评估
通过证明 wK4 及相关逻辑在半度量空间上的度量完备性,并以有限结构可模拟性作为关键测试用例,说明混合缠结足以定义该性质。
原文摘要(Abstract)

The µ-calculus can be interpreted over metric spaces and is known to enjoy, among other celebrated properties, variants of the McKinsey-Tarski completeness theorem and of Dawar and Otto’s modal characterization theorem. In its topological form, this theorem states that every topological fixed point may be defined in terms of the tangled derivative, a polyadic generalization of Cantor’s perfect core. However, these results fail when spaces not satisfying basic separation axioms are considered, in which case the base modal logic is not the well-known K4, but the weaker wK4.In this paper we show how these shortcomings may be overcome. First, we consider semantics over the wider class of hemimetric spaces, and obtain metric completeness results for wK4 and related logics. In this setting, the Dawar-Otto theorem still fails, but we argue that this is due to the tangled derivative not being suitably defined for general application in arbitrary topological spaces. We thus introduce the hybrid tangle, which coincides with the tangled derivative over metric spaces but is better behaved in general. We show that only the hybrid tangle suffices to define simulability of finite structures, a key ‘test case’ for an expressively complete fragment of the µ-calculus.

链接与引用

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

BibTeX
@inproceedings{Fernandez-Duque23,
  title = {Fixed Point Logics on Hemimetric Spaces},
  author = {David Fernández-Duque and Quentin Gougeon},
  booktitle = {LICS},
  year = {2023},
  doi = {10.1109/lics56636.2023.10175784}
}