paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Interpolating Between Choices for the Approximate Intermediate Value Theorem

在近似介值定理的两种选择之间插值
LMCS vol.Volume 16, Issue 32020匹配度 2/10 · 该论文属于构造性数学与定理证明,讨论近似介值定理的弱假设证明,与静态分析、Agent、浮点程序分析、贝叶斯程序分析及 LLM 交叉均无直接关联;仅与形式化验证/证明工程有边缘联系。引用 3 inbox
Matthew Frank
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话:构造性证明近似介值定理:仅需逐点连续,避免可数选择与有理逼近表示。

本文研究构造性数学中近似介值定理的证明条件。经典证明用二分法反复选择区间的左半或右半,但该选择在构造性框架下需要额外假设。作者提出一种连续插值左右选择的算法:每次选取一个规模减半的区间,而非离散地二选一。由此证明:若逐点连续函数在某点取负值、另一点取正值,则其函数值可任意接近 0。该证明仅依赖逐点连续,不假设实数带有有理逼近表示,也不使用可数选择。结果强化了构造性分析中近似介值定理的可用范围。

问题
在构造性数学中,经典二分法证明近似介值定理需要反复选择左半或右半区间,这通常依赖可数选择或更强的连续性/实数表示假设。
方法
提出一种连续插值左右选择的二分算法:每次选取一个规模减半的区间,而非离散地二选一,从而在弱假设下构造性证明定理。
评估
以构造性证明方式论证;证明仅用逐点连续,无需一致连续、有理逼近表示或可数选择。
原文摘要(Abstract)

This paper proves the approximate intermediate value theorem, constructively and from notably weak hypotheses: from pointwise rather than uniform continuity, without assuming that reals are presented with rational approximants, and without using countable choice. The theorem is that if a pointwise continuous function has both a negative and a positive value, then it has values arbitrarily close to 0. The proof builds on the usual classical proof by bisection, which repeatedly selects the left or right half of an interval; the algorithm here selects an interval of half the size in a continuous way, interpolating between those two possibilities.

链接与引用

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

BibTeX
@article{Frank17,
  title = {Interpolating Between Choices for the Approximate Intermediate Value Theorem},
  author = {Matthew Frank},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 16, Issue 3},
  year = {2020},
  doi = {10.23638/lmcs-16(3:5)2020}
}