paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The principle of pointfree continuity

无点连续性原则
LMCS vol.Volume 15, Issue 12019匹配度 0/10 · 该论文研究构造性无点拓扑与Brouwer连续性原则,属于纯数学逻辑/形式语义基础,与用户关注的静态分析、Agentic程序、LLM辅助形式化验证、浮点程序分析及贝叶斯程序分析均无直接关联。引用 2 inbox
Tatsuji Kawai, Giovanni Sambin
crossref: 2026-09-10

AI 速览

一句话:在构造性无点拓扑中提出无点连续性原则,用基间关系诱导连续操作,并联系空间性与紧致性。

本文在构造性无点拓扑中研究 Brouwer 连续性原则的严格表述。作者引入无点拓扑间的连续操作:若点间操作由拓扑基间的关系诱导,则称其连续;相应的无点连续性原则断言,对无点拓扑 S、T,任何诱导连续操作的关系都是 S 到 T 的态射。工作以 Minimalist Foundation 为基础,采用 positive topology,区分理想对象与构造性对象,并将选择序列解释为形式 Baire 空间的点。主要结果:当 S 具有双空间性时原则成立;当 S 为形式 Baire 空间或形式单位区间、T 为自然数形式拓扑时,该原则等价于相应空间性。空间性、bar induction 与单位区间紧致性的若干联系由此被重新表述。

问题
在构造性无点拓扑中,如何定义并证明无点连续性原则,为 Brouwer 连续性原则提供严格条件,并刻画其与空间性、bar induction 和紧致性的关系。
方法
引入由拓扑基间关系诱导的连续操作,提出无点连续性原则;在 Minimalist Foundation 与 positive topology 下,将选择序列解释为形式 Baire 空间的点。
评估
证明 S 双空间时原则成立;对形式 Baire 空间或形式单位区间与自然数形式拓扑,证明该原则分别等价于相应空间性,并重述若干已知联系。
原文摘要(Abstract)

In the setting of constructive pointfree topology, we introduce a notion of continuous operation between pointfree topologies and the corresponding principle of pointfree continuity. An operation between points of pointfree topologies is continuous if it is induced by a relation between the bases of the topologies; this gives a rigorous condition for Brouwer's continuity principle to hold. The principle of pointfree continuity for pointfree topologies $\mathcal{S}$ and $\mathcal{T}$ says that any relation which induces a continuous operation between points is a morphism from $\mathcal{S}$ to $\mathcal{T}$. The principle holds under the assumption of bi-spatiality of $\mathcal{S}$. When $\mathcal{S}$ is the formal Baire space or the formal unit interval and $\mathcal{T}$ is the formal topology of natural numbers, the principle is equivalent to spatiality of the formal Baire space and formal unit interval, respectively. Some of the well-known connections between spatiality, bar induction, and compactness of the unit interval are recast in terms of our principle of continuity. We adopt the Minimalist Foundation as our constructive foundation, and positive topology as the notion of pointfree topology. This allows us to distinguish ideal objects from constructive ones, and in particular, to interpret choice sequences as points of the formal Baire space.

链接与引用

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

BibTeX
@article{paperbot816,
  title = {The principle of pointfree continuity},
  author = {Tatsuji Kawai and Giovanni Sambin},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 15, Issue 1},
  year = {2019},
  doi = {10.23638/lmcs-15(1:22)2019}
}