paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Overlap Algebras as Almost Discrete Locales

重叠代数作为几乎离散的 locale
LMCS vol.Volume 19, Issue 42023匹配度 1/10 · 该论文属于构造性拓扑与形式语义理论,研究重叠代数与几乎离散locale的刻画,与用户关注的静态分析、LLM/Agent、浮点程序分析、贝叶斯程序分析等方向无直接关联,也未涉及工程实现或工业落地。引用 5 inbox
Francesco Ciraulo
crossref: 2026-09-10

AI 速览

一句话:提出重叠代数可构造地刻画几乎离散 locale,并在 LEM 下与 Boolean locale 一致。

经典地,Boolean locale 是“几乎离散”的:空间化后恰为离散 locale。但该事实依赖排中律,不能构造性证明;构造性地看,除平凡情形外离散 locale 从不是 Boolean。本文追问构造性意义下何为几乎离散 locale,并主张 Sambin 的重叠代数是合适候选。作者证明重叠代数包含离散 locale,可作为 overt locale 的最小强稠密 sublocale 得到,并在 LEM 成立时恰好与 Boolean locale 重合。

问题
经典下 Boolean locale 的“几乎离散性”依赖 LEM;构造性地如何刻画几乎离散 locale,尤其离散 locale 通常不再 Boolean,是本文的问题。
方法
作者提出以 Sambin 的重叠代数为构造性候选,并考察其与离散 locale、overt locale 的强稠密 sublocale 构造之间的关系。
评估
通过构造性证明表明重叠代数包含离散 locale,并作为 overt locale 的最小强稠密 sublocale;在加入 LEM 后与 Boolean locale 一致。
原文摘要(Abstract)

Boolean locales are "almost discrete", in the sense that a spatial Boolean locale is just a discrete locale (that is, it corresponds to the frame of open subsets of a discrete space, namely the powerset of a set). This basic fact, however, cannot be proven constructively, that is, over intuitionistic logic, as it requires the full law of excluded middle (LEM). In fact, discrete locales are never Boolean constructively, except for the trivial locale. So, what is an almost discrete locale constructively? Our claim is that Sambin's overlap algebras have good enough features to deserve to be called that. Namely, they include the class of discrete locales, they arise as smallest strongly dense sublocales (of overt locales), and hence they coincide with the Boolean locales if LEM holds.

链接与引用

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

BibTeX
@article{paperbot2172,
  title = {Overlap Algebras as Almost Discrete Locales},
  author = {Francesco Ciraulo},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 19, Issue 4},
  year = {2023},
  doi = {10.46298/lmcs-19(4:21)2023}
}