paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Sound and robust solid modeling via exact real arithmetic and continuity

基于精确实数算术与连续性的可靠且鲁棒实体建模
ICFP 3(ICFP)2019匹配度 2/10 · 论文聚焦函数式语言、精确实数算术与实体建模 DSL,虽涉及浮点有限精度导致的不可靠问题,但并不属于浮点程序分析,也没有与 LLM/Agent、ML 系统静态分析或贝叶斯程序分析产生直接交集。其核心领域是 CAD/图形学中的可靠实体建模,与用户研究画像匹配度很低。引用 26 inbox
Benjamin Sherman, Jesse Michel, Michael Carbin
crossref: 2026-09-10

AI 速览

一句话:提出 StoneWorks 库、MarshallB 语言与 K-rep 表示,使实体建模在精确实数算术和连续性下可靠且鲁棒。

实体建模(CAD 与计算机图形学)算法通常在实数上定义,却用浮点等有限精度实现,导致实现无法可靠地计算规约所预期的结果。本文提出 StoneWorks 库,提供可靠且鲁棒的实体建模原语;它实现于 MarshallB——一种面向精确实数算术的纯函数式语言,其中类型表示拓扑空间、函数表示连续映射,从而保证程序可靠且鲁棒。MarshallB 是 Marshall 语言的扩展。作者还提出新的形状表示 K-rep:一种描述形状中所有点的非确定性单子,支持 Minkowski 和、Hausdorff 距离等传统表示难以完成的操作与分析。结果表明,短小的 StoneWorks 程序即可规约并执行可靠、鲁棒的实体建模算法与任务。

问题
实体建模(CAD 与计算机图形学)算法常在实数上规约,却用浮点等有限精度实现,导致实现无法可靠地计算规约所预期的结果。
方法
提出 StoneWorks 库,并在纯函数式语言 MarshallB 中实现;该语言的类型表示拓扑空间、函数表示连续映射,以保证可靠性与鲁棒性;还提出基于非确定性单子的 K-rep 形状表示。
评估
作者以库、语言与表示的组合,展示短小的 StoneWorks 程序即可规约并执行可靠且鲁棒的实体建模算法与任务。
原文摘要(Abstract)

Algorithms for solid modeling, i.e., Computer-Aided Design (CAD) and computer graphics, are often specified on real numbers and then implemented with finite-precision arithmetic, such as floating-point. The result is that these implementations do not soundly compute the results that are expected from their specifications. We present a new library, StoneWorks, that provides sound and robust solid modeling primitives. We implement StoneWorks in MarshallB, a pure functional programming language for exact real arithmetic in which types denote topological spaces and functions denote continuous maps, ensuring that all programs are sound and robust. We developed MarshallB as an extension of the Marshall language. We also define a new shape representation, compact representation ( K-rep ), that enables constructions such as Minkowski sum and analyses such as Hausdorff distance that are not possible with traditional representations. K-rep is a nondeterminism monad for describing all the points in a shape. With our library, language, and representation together, we show that short StoneWorks programs can specify and execute sound and robust solid modeling algorithms and tasks.

链接与引用

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

BibTeX
@article{paperbot596,
  title = {Sound and robust solid modeling via exact real arithmetic and continuity},
  author = {Benjamin Sherman and Jesse Michel and Michael Carbin},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {ICFP},
  year = {2019},
  doi = {10.1145/3341703}
}