paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Uniform Envelopes

一致包络
LMCS vol.Volume 18, Issue 32022匹配度 2/10 · 论文属于纯形式语义/域理论,研究不连续函数的连续可得信息与一致包络,未涉及用户关注的静态分析、Agentic 程序、浮点/贝叶斯程序分析或 LLM 与形式化验证交叉,仅与 PL 理论基础有微弱关联。引用 2 inbox
Eike Neumann
crossref: 2026-09-10

AI 速览

一句话:提出一致包络,为不连续函数上连续可得信息提供一致可计算的因子分解与复合定理。

论文研究不连续函数的连续可得信息表示。通用包络可编码这类信息,但其因子分解一般不可一致计算。作者提出一致包络:在通用包络上增加与双重幂空间单子 O^2 乘法相容的映射 u_L: L→O^2(Y),对取值于内射空间的连续映射给出可一致计算的扩张;在一致通用性条件下解决因子分解。文中定义一致包络的复合,给出复合仍一致通用的判别准则及部分逆,并构造任意函数的最接近一致包络的典范包络与类似复合定理。

问题
通用包络能为不连续函数编码连续可得信息,但其因子分解一般不能一致计算;本文要解决如何为包络引入一致可计算性并研究其复合封闭性。
方法
在通用包络上增加与双重幂空间单子乘法相容的映射 u_L,定义一致包络与一致通用性,并用域论/范畴构造建立因子分解、复合准则及典范包络。
评估
理论评估:证明一致扩张与因子分解定理,给出复合判别准则、部分逆及不可轻易改进的证据;无实验评估。
原文摘要(Abstract)

In the author's PhD thesis (2019) universal envelopes were introduced as a tool for studying the continuously obtainable information on discontinuous functions. To any function $f \colon X \to Y$ between $\operatorname{qcb}_0$-spaces one can assign a so-called universal envelope which, in a well-defined sense, encodes all continuously obtainable information on the function. A universal envelope consists of two continuous functions $F \colon X \to L$ and $\xi_L \colon Y \to L$ with values in a $\Sigma$-split injective space $L$. Any continuous function with values in an injective space whose composition with the original function is again continuous factors through the universal envelope. However, it is not possible in general to uniformly compute this factorisation. In this paper we propose the notion of uniform envelopes. A uniform envelope is additionally endowed with a map $u_L \colon L \to \mathcal{O}^2(Y)$ that is compatible with the multiplication of the double powerspace monad $\mathcal{O}^2$ in a certain sense. This yields for every continuous map with values in an injective space a choice of uniformly computable extension. Under a suitable condition which we call uniform universality, this extension yields a uniformly computable solution for the above factorisation problem. Uniform envelopes can be endowed with a composition operation. We establish criteria that ensure that the composition of two uniformly universal envelopes is again uniformly universal. These criteria admit a partial converse and we provide evidence that they cannot be easily improved in general. Not every function admits a uniformly universal uniform envelope. We can however assign to every function a canonical envelope that is in some sense as close as possible to a uniform envelope. We obtain a composition theorem similar to the uniform case.

链接与引用

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

BibTeX
@article{paperbot1683,
  title = {Uniform Envelopes},
  author = {Eike Neumann},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 3},
  year = {2022},
  doi = {10.46298/lmcs-18(3:8)2022}
}