paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Point-free Construction of Real Exponentiation

实数指数运算的无点构造
LMCS vol.Volume 18, Issue 32022匹配度 0/10 · 该论文构造的是无点拓扑/几何理论下的实数指数与对数,属于构造性数学、拓扑斯与数论基础研究,既不涉及静态分析、程序验证或浮点程序分析,也未与 LLM/Agent 交叉。引用 0 inbox
Ming Ng, Steven Vickers
crossref: 2026-09-10

AI 速览

一句话:用无点拓扑与几何理论构造实数指数和对数,建立其代数规则并发展提升与粘合技术。

论文在无点拓扑(point-free topology)框架下构造实数指数与对数,即定义 exp:(0,∞)×R→(0,∞) 与 log:(1,∞)×(0,∞)→R 并建立熟悉的代数法则。其方法将空间点视为几何理论的模型而非集合元素,因此构造是构造性的,并可作用于非 Set 的 topos 中的点。作者发展了无点拓扑中的提升(lifting)与粘合(gluing)新技术,揭示 Q 的性质如何决定实数指数性质。该工作由通过 topos 理论发展 adelic geometry 的研究计划驱动,尤其希望构造 Q 的 places 的分类 topos,以几何视角理解 R 与 Q_p 的关系。评估方式为构造性数学证明与代数规则验证。

问题
如何在无点(构造性)拓扑中定义实指数与对数,使其可作用于非 Set 的 topos 中的点,并服务于 adelic geometry 与 Q 的 places 分类 topos 的构造。
方法
将空间点定义为几何理论的模型,在无点拓扑与 topos 框架下构造 exp 和 log,并发展提升与粘合技术以推出代数规则。
评估
通过构造性数学证明给出 exp/log 映射及其代数法则,说明 Q 的性质对实数指数的影响;摘要未报告实验评估。
原文摘要(Abstract)

We define a point-free construction of real exponentiation and logarithms, i.e.\ we construct the maps $\exp\colon (0, \infty)\times \mathbb{R} \rightarrow \!(0,\infty),\, (x, \zeta) \mapsto x^\zeta$ and $\log\colon (1,\infty)\times (0, \infty) \rightarrow\mathbb{R},\, (b, y) \mapsto \log_b(y)$, and we develop familiar algebraic rules for them. The point-free approach is constructive, and defines the points of a space as models of a geometric theory, rather than as elements of a set - in particular, this allows geometric constructions to be applied to points living in toposes other than Set. Our geometric development includes new lifting and gluing techniques in point-free topology, which highlight how properties of $\mathbb{Q}$ determine properties of real exponentiation. This work is motivated by our broader research programme of developing a version of adelic geometry via topos theory. In particular, we wish to construct the classifying topos of places of $\mathbb{Q}$, which will provide a geometric perspective into the subtle relationship between $\mathbb{R}$ and $\mathbb{Q}_p$, a question of longstanding number-theoretic interest.

链接与引用

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

BibTeX
@article{paperbot1673,
  title = {Point-free Construction of Real Exponentiation},
  author = {Ming Ng and Steven Vickers},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 3},
  year = {2022},
  doi = {10.46298/lmcs-18(3:15)2022}
}