AI 中文总结
针对非局部紧致状态空间（如无限维Banach空间）中现有域论框架的局限，提出利用Gromov的horofunction紧化，通过Lipschitz嵌入和Scott连续映射实现单调映射的鲁棒逼近，为可分空间提供可度量的有效构造途径。
AI 中文摘要
鲁棒性分析在计算系统和混合系统的验证与设计中扮演核心角色，尤其是当系统行为连续依赖于受扰动影响的参数时。现有的域论框架通过闭集格上的单调映射，为推理此类扰动提供了原则性基础。然而，当底层状态空间非局部紧致时（例如分析、机器学习和控制理论中出现的无限维空间，如$\ell_p$和$L_p$空间），这些框架面临显著限制。在这些情形下，闭子集格不连续，经典紧化要么牺牲精度，要么缺乏可计算结构。我们提出将Gromov的horofunction紧化作为一类具有实际重要性的可分度量空间（包括可分自反Banach空间）上鲁棒性分析的新工具。给定度量空间$\mathbb{S}$，我们证明其horofunction扩张产生一个紧致度量空间及一个Lipschitz嵌入，这使得能够通过紧化域上的Scott连续映射对单调映射进行鲁棒逼近。对于可分空间，horofunction紧化是可度量的，这为有效的域论构造提供了途径。
英文摘要
Robustness analysis plays a central role in the verification and design of computational and hybrid systems, particularly when system behaviour depends continuously on parameters subject to perturbation. Existing domain-theoretic frameworks provide a principled foundation for reasoning about such perturbations via monotone maps on lattices of closed sets. However, these frameworks face significant limitations when the underlying state space is not locally compact, as is the case for the infinite-dimensional spaces that arise in analysis, machine learning, and control theory (e.g., $\ell_p$ and $L_p$ spaces). In these settings, the lattice of closed subsets fails to be continuous, and classical compactifications either sacrifice precision or lack computable structure. We propose Gromov's horofunction compactification as a new tool for robustness analysis over a class of separable metric spaces of practical importance, including separable reflexive Banach spaces. Given a metric space $\mathbb{S}$, we show that its horofunction extension yields a compact metric space together with a Lipschitz embedding, which enables robust approximations of monotone maps via Scott-continuous maps on the compactified domain. For separable spaces, the horofunction compactification is metrizable, which provides a path toward effective domain-theoretic constructions.
Comments42nd Conference on the Mathematical Foundations of Programming Semantics (MFPS 2026)
