implicit_predicates_gen/point/error_bound.rs
1//! The error bound of the approximate coordinates of a point type: the
2//! program that computes it and its slack factor, derived and justified in
3//! the documentation of [`error_bound`].
4
5use crate::dyadic::Dyadic;
6use crate::error::Error;
7
8use super::{PointNode, PointType};
9
10/// The largest rounding count [`error_bound`] accepts: it keeps the exact
11/// derivation of the slack factor small.
12pub const MAX_ROUNDS: u32 = 1024;
13
14/// The error bound of the coordinates of a point type, as derived by
15/// [`error_bound`].
16#[derive(Clone, Copy, Debug, PartialEq)]
17pub struct ErrorBound {
18 /// The number of roundings of the computation of the error of each
19 /// coordinate, on its longest chain of operations.
20 pub rounds: [u32; 3],
21 /// The slack factor `S`: the smallest `f64` with `S·(1 - 2^-53)^H >= 1`,
22 /// where `H` is the largest of [`rounds`](Self::rounds).
23 pub slack: f64,
24}
25
26/// A term of the error of a node.
27#[derive(Clone, Copy, Debug, PartialEq, Eq)]
28pub(crate) enum Term {
29 /// The error of a node, as computed.
30 Error(usize),
31 /// The covered product of `|value|` and the error of `error`.
32 ValueTimesError {
33 /// The node whose value is taken.
34 value: usize,
35 /// The node whose error is taken.
36 error: usize,
37 },
38 /// The covered product of the errors of two nodes.
39 ErrorTimesError(usize, usize),
40 /// The rounding of a sum or difference of the nodes `x` and `y`.
41 SumRounding(usize, usize),
42 /// The rounding of a product of the nodes `x` and `y`.
43 ProductRounding(usize, usize),
44}
45
46/// The program that computes the error of every node of a point type: the
47/// terms added, in order, and the rounding count of each node. A node with
48/// no terms has an error of zero for every input.
49#[derive(Clone, Debug, PartialEq, Eq)]
50pub(crate) struct ErrorProgram {
51 pub(crate) terms: Vec<Vec<Term>>,
52 pub(crate) rounds: Vec<u32>,
53}
54
55impl ErrorProgram {
56 /// Builds the program of `point`, whose integers must be representable.
57 pub(crate) fn of(point: &PointType) -> ErrorProgram {
58 let nodes = &point.graph.nodes;
59 let is_zero = |id: usize| nodes[id] == PointNode::Int(0);
60 let mut terms: Vec<Vec<Term>> = Vec::with_capacity(nodes.len());
61 let mut rounds: Vec<u32> = Vec::with_capacity(nodes.len());
62 for node in nodes {
63 let has_error = |id: usize, terms: &[Vec<Term>]| !terms[id].is_empty();
64 let mut node_terms = Vec::new();
65 match *node {
66 PointNode::Coord { .. } | PointNode::Scalar(_) | PointNode::Int(_) => {}
67 PointNode::Neg(x) => {
68 if has_error(x, &terms) {
69 node_terms.push(Term::Error(x));
70 }
71 }
72 PointNode::Add(x, y) | PointNode::Sub(x, y) => {
73 for operand in [x, y] {
74 if has_error(operand, &terms) {
75 node_terms.push(Term::Error(operand));
76 }
77 }
78 if !is_zero(x) && !is_zero(y) {
79 node_terms.push(Term::SumRounding(x, y));
80 }
81 }
82 PointNode::Mul(x, y) => {
83 let (ex, ey) = (has_error(x, &terms), has_error(y, &terms));
84 if ey {
85 node_terms.push(Term::ValueTimesError { value: x, error: y });
86 }
87 if ex {
88 node_terms.push(Term::ValueTimesError { value: y, error: x });
89 }
90 if ex && ey {
91 node_terms.push(Term::ErrorTimesError(x, y));
92 }
93 if !is_zero(x) && !is_zero(y) {
94 node_terms.push(Term::ProductRounding(x, y));
95 }
96 }
97 }
98 let count = node_terms
99 .iter()
100 .map(|&term| term_rounds(term, &rounds))
101 .reduce(|total, term| total.max(term).saturating_add(1))
102 .unwrap_or(0);
103 terms.push(node_terms);
104 rounds.push(count);
105 }
106 ErrorProgram { terms, rounds }
107 }
108}
109
110/// The rounding count of `term`, given the counts of the earlier nodes.
111fn term_rounds(term: Term, rounds: &[u32]) -> u32 {
112 match term {
113 Term::Error(x) => rounds[x],
114 Term::ValueTimesError { error, .. } => rounds[error].saturating_add(2),
115 Term::ErrorTimesError(x, y) => rounds[x].saturating_add(rounds[y]).saturating_add(2),
116 Term::SumRounding(..) => 2,
117 Term::ProductRounding(..) => 3,
118 }
119}
120
121/// Derives the error bound of the approximate coordinates of `point`.
122///
123/// The constructor of a point type evaluates its coordinates in `f64`, one
124/// node of its [`PointGraph`](super::PointGraph) at a time, and with each
125/// value `v` an error `e`, a bound on `|v - V|` where `V` is the exact value
126/// of the node. This function derives the program that computes `e` and the
127/// factor that makes the result an upper bound in spite of the rounding of
128/// that program itself.
129///
130/// # The rule
131///
132/// With `u = 2^-53`, the rule gives each node a real bound `R`:
133///
134/// - an input (a coordinate, an `f64` parameter or an integer that `f64`
135/// represents exactly) has `R = 0`;
136/// - a negation keeps the bound of its operand;
137/// - a sum or difference `s = x ± y` has `R_s = R_x + R_y`, plus `u·|s|`
138/// unless an operand is exactly zero;
139/// - a product `p = x·y` has `R_p = |x|·R_y + |y|·R_x + R_x·R_y`, plus
140/// `u·|p| + 2^-1074` unless an operand is exactly zero.
141///
142/// Here `x`, `y`, `s` and `p` are the computed `f64` values. `R` bounds the
143/// error: rounding to nearest makes `|fl(x ± y) - (x ± y)|` at most
144/// `u·|fl(x ± y)|` (a sum whose result is below `2^-1021` is exact), and
145/// `|fl(x·y) - x·y|` at most `u·|fl(x·y)|` or, when `x·y` is below `2^-1022`,
146/// `2^-1075`; an operation with an operand that is exactly zero is exact.
147/// The errors of the operands then propagate as written, since
148/// `|x·y - X·Y| <= |x|·|y - Y| + (|y| + |y - Y|)·|x - X|`. The condition
149/// "exactly zero" is on the operands, never on the result: a product that
150/// underflows gives zero without being exact.
151///
152/// # The program
153///
154/// The program computes, for each node, the terms of its rule in the order
155/// above and adds them from left to right. Terms that are zero for every
156/// input (the error of an input) are left out; the others are computed even
157/// when they are zero at run time, which costs nothing in the bound because
158/// an operation with a zero operand is exact. Every product of the program
159/// is a *covered product*: `fl(fl(a·b) + 2^-1074)`, or `0` when `a` or `b`
160/// is zero. The rounding terms are the covered product of `u` and `|s|` for
161/// a sum, and the covered product of `u` and `|p|` plus `2^-1074` for a
162/// product, both `0` when an operand of the node is zero.
163///
164/// # The rounding of the program
165///
166/// All the values of the program are non-negative. For non-negative `a` and
167/// `b`, `fl(a + b) >= (1 - u)·(a + b)`: above `2^-1022` by the bound on the
168/// relative error, and below it because the sum is exact. A covered product
169/// satisfies `c >= (1 - u)^2·a·b` whatever the magnitudes, which is why the
170/// program adds `2^-1074` after each product: if `fl(a·b) >= 2^-1022`,
171/// `fl(a·b) >= (1 - u)·a·b` and the addition loses at most another factor
172/// `1 - u`; if `fl(a·b) < 2^-1022`, possibly zero after underflow, then
173/// `fl(a·b) >= a·b - 2^-1075`, and adding `2^-1074` to a value below
174/// `2^-1022` is exact, so `c >= a·b`. That covers the underflow of the
175/// program itself, including a product rounded to zero, and the term is
176/// added only when both operands are nonzero, so a coordinate whose terms
177/// are all zero still gets an error of exactly zero.
178///
179/// Each node is given a count `h` of roundings: one per addition and per
180/// multiplication of the program on the longest chain that leads to its
181/// error, so a covered product counts two. An error `e(x)` with `h(x)` such
182/// roundings satisfies `e(x) >= (1 - u)^h(x)·R(x)`, by induction over the
183/// operations: an input has `h = 0`; the error of an operand has its own
184/// count; a covered product of a value and an error `e(y)` has `h(y) + 2`,
185/// and of two errors `h(x) + h(y) + 2`; the rounding term of a sum has 2 and
186/// that of a product 3; and adding a term to the sum of the previous ones
187/// gives one more than the larger of the two counts.
188///
189/// # The factor and the final rounding
190///
191/// With `H` the largest count of the three coordinates, the slack factor `S`
192/// is the smallest `f64` with `S·(1 - u)^H >= 1`, derived here in exact
193/// arithmetic. The constructor then stores `next_up(fl(e·S))`, which is at
194/// least `e·S >= R`, since the value after the nearest `f64` is above the
195/// exact product; and `0` when `e` is `0`, which happens only when every
196/// term is zero, so only when `R` is zero and the coordinate is exact. If
197/// the coordinate or `fl(e·S)` is not finite, it stores `+∞` instead.
198///
199/// # Errors
200///
201/// An error at the name of the type if an integer of its expression is not
202/// exactly an `f64`, or if the computation of the error of a coordinate
203/// takes more than [`MAX_ROUNDS`] roundings.
204pub fn error_bound(point: &PointType, file: &str) -> Result<ErrorBound, Error> {
205 check_integers(point, file)?;
206 let program = ErrorProgram::of(point);
207 let rounds = point.graph.roots.map(|root| program.rounds[root]);
208 let most = rounds.into_iter().max().unwrap_or(0);
209 if most > MAX_ROUNDS {
210 return Err(Error::at(
211 file,
212 point.position,
213 format!(
214 "the error bound of `{}` takes {most} roundings, more than the {MAX_ROUNDS} \
215 for which its slack factor is derived",
216 point.name
217 ),
218 ));
219 }
220 Ok(ErrorBound {
221 rounds,
222 slack: slack_factor(most),
223 })
224}
225
226/// Checks that every integer of the expression of `point` is exactly an
227/// `f64`, so that it is an input without error.
228fn check_integers(point: &PointType, file: &str) -> Result<(), Error> {
229 for node in &point.graph.nodes {
230 if let PointNode::Int(n) = *node {
231 if !is_exact_f64(n) {
232 return Err(Error::at(
233 file,
234 point.position,
235 format!(
236 "the integer {n} in `{}` is not exactly an `f64`: integers of a point \
237 must have a magnitude of at most 2^53 or be exactly representable",
238 point.name
239 ),
240 ));
241 }
242 }
243 }
244 Ok(())
245}
246
247/// Whether `n` converts to `f64` without rounding.
248pub(crate) fn is_exact_f64(n: i64) -> bool {
249 // `as` rounds to nearest, and the conversion back is exact in i128.
250 #[allow(clippy::cast_precision_loss, clippy::cast_possible_truncation)]
251 let back = (n as f64) as i128;
252 back == i128::from(n)
253}
254
255/// The smallest `f64` `S` with `S·(1 - 2^-53)^rounds >= 1`.
256pub(crate) fn slack_factor(rounds: u32) -> f64 {
257 let one_minus_u = &Dyadic::integer(1) - &Dyadic::pow2(-53);
258 let mut power = Dyadic::integer(1);
259 for _ in 0..rounds {
260 power = &power * &one_minus_u;
261 }
262 let one = Dyadic::integer(1);
263 let mut slack = 1.0f64;
264 while &Dyadic::from_f64(slack) * &power < one {
265 slack = slack.next_up();
266 }
267 slack
268}
269
270#[cfg(test)]
271mod tests {
272 use super::*;
273
274 #[test]
275 fn the_slack_factor_covers_its_rounds_and_no_smaller_factor_does() {
276 assert_eq!(slack_factor(0), 1.0);
277 for rounds in [1, 2, 3, 6, 100, MAX_ROUNDS] {
278 let s = slack_factor(rounds);
279 let one_minus_u = &Dyadic::integer(1) - &Dyadic::pow2(-53);
280 let mut power = Dyadic::integer(1);
281 for _ in 0..rounds {
282 power = &power * &one_minus_u;
283 }
284 assert!(&Dyadic::from_f64(s) * &power >= Dyadic::integer(1));
285 assert!(&Dyadic::from_f64(s.next_down()) * &power < Dyadic::integer(1));
286 }
287 }
288
289 #[test]
290 fn integers_beyond_2_to_the_53_are_exact_only_when_representable() {
291 assert!(is_exact_f64(1 << 53));
292 assert!(!is_exact_f64((1 << 53) + 1));
293 assert!(is_exact_f64(i64::MIN));
294 assert!(!is_exact_f64(i64::MAX));
295 }
296}