SHF:Small:Techniques for Generating Correctly Rounded Math Libraries

每种编程语言都需要数学库，这些库为浮点表示及其变体提供基本函数的实现。该项目旨在为广泛的近似实数表示开发正确的四舍五入数学库。这个项目的新颖之处在于创建多项式近似，产生初等函数f(x)的正确四舍五入值（即f(x)的值四舍五入到目标表示），而不是f(x)的实际值。它在生成有效多项式的同时，为识别正确的多项式提供了更大的余地。这个项目的影响是在为大量数据类型逼近基本函数方面推进了最先进的技术，同时允许领域科学家对其数据类型的精度和动态范围进行实验。它有可能影响各种标准的委员会，要求对现有和新的陈述进行正确的四舍五入。这个项目也将教育实践者、研究生和本科生基本的计算抽象。这个项目结构的任务是产生有效的多项式近似，产生正确的四舍五入的结果作为一个线性规划问题。具体来说，它提出了反例引导的多项式生成，用于为所有具有大数据类型的输入生成正确的结果。为了生成性能良好的实现，提出了分段多项式的生成方法。它还探讨了适用于线性规划公式的新的距离缩减技术。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Every programming language needs math libraries, which provide implementations of elementary functions for the floating-point representation and its variants. This project aims to develop correctly rounded math libraries for a wide range of representations that approximate real numbers. This project's novelty lies in creating polynomial approximations that produce the correctly rounded value of an elementary function f(x) (i.e., the value of f(x) rounded to the target representation) rather than the real value of f(x). It provides more margin to identify correct polynomials while generating efficient polynomials. This project's impacts are in advancing the state-of-the-art in approximating elementary functions for a large number of data types while allowing domain scientists to experiment with both precision and dynamic range of their data types. It has the potential to influence committees on various standards to mandate correctly rounded results for existing and new representations. This project also will educate practitioners, graduate and undergraduate students on foundational abstractions in computing.This project structures the task of generating efficient polynomial approximations that produce correctly rounded results as a linear-programming problem. Specifically, it proposes counterexample-guided polynomial generation for generating correct results for all inputs with large data types. To generate implementations with good performance, it proposes the generation of piecewise polynomials. It also explores new range-reduction techniques that are amenable to the linear-programming formulation.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.