SHF:Small:Techniques for Generating Correctly Rounded Math Libraries

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

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.