精确几何计算

形式陈述 ​

几何算法的正确性理路算法正确性Algorithm correctness · Partial and total correctness所有合法执行都符合规格，并在完全正确时保证终止。要求组合分支符合所声明的精确输入与输出规格。输入可用整数、有理数，或把有限二进制浮点值视作精确的二进有理数；NaN 与无穷不属于这里的有限平面坐标。在浮点数系统理路浮点数系统与 IEEE 754Floating-point system · IEEE 754以有限尾数和指数表示机器数，并说明 IEEE 754 的特殊值、格式与运算语义。上实现快速路径时，有限个谓词的符号常决定组合结构，例如

精确几何计算原则要求：只要输入坐标被模型精确表示，算法用于分支的谓词符号必须与相应实数或整数表达式的数学符号一致。构造出的交点、距离或坐标可以近似，但任何会改变拓扑或组合结构的分支不得由未经误差控制的浮点近似决定。

一种常见过滤框架是：

1. 用普通浮点快速计算近似值 $\hat{p}$；
2. 同时计算可靠误差界 $E$；
3. 若 $|\hat{p}|>E$，直接返回其符号；
4. 否则转入能确定包括零在内的精确符号后端，例如对这些有限整数或有理输入计算精确展开；也可先提高精度，再在仍不确定时回退。

例如验证区间算术理路验证数值计算与区间算术Verified numerics · Validated numerics · Interval arithmetic用向外舍入的区间运算构造包含真实结果的可检查外包络，并分辨可靠包含与界的紧致程度。可给出包含真值的区间 $[\hat{p}-E,\hat{p}+E]$，其中 $E\ge 0$；只有区间完全位于零的一侧，才据此返回正或负。包含零表示尚未决定，不表示已证明真值为零。连续缩窄区间也未必能在真值恰为零时停止，例如 $[-2^{-k},2^{-k}]$ 始终包含零。因此完整算法还须有精确零检验或其他可证明终止的符号程序；对更一般的代数坐标，应另外给出相应表示与判零方法。误差界也须覆盖实际舍入、溢出和下溢行为。

该接口返回的是符号证书，而不是“看起来足够精确”的数值。