---
tag: 64V8MA4FH4
kind: definition
name: Validated numerics
msc: [65G20, 65G30, 65G40]
defines: DW7FG506QJ
uses: [QPKKTE1ZY0, CPN6SD3BTV, 4AKCQERM89]
sources:
  - url: https://en.wikipedia.org/wiki/Validated_numerics
---

## Definition

Let $y \in \R^n$ be a quantity defined by a mathematical problem, such as a zero of a function or the value of an integral.
A *validated* (or *verified*) computation of $y$ is an algorithm, run in floating-point arithmetic, with the following property.
It either reports failure or outputs a set $Y \subseteq \R^n$, usually a box of [[intervals|QPKKTE1ZY0]], such that $y \in Y$ is guaranteed.
The guarantee must account for every [[round-off error|CPN6SD3BTV]] and every [[truncation error|4AKCQERM89]] of the computation.
*Validated numerics* is the study and use of such algorithms.

## Remarks

Example: the interval Newton test.
Let $f(x) = x^2 - 2$ and $X = [1.4, 1.5]$; with midpoint $m = 1.45$ and the enclosure $[2.8, 3.0]$ of $f'$ on $X$, the interval Newton step is $N(X) = m - f(m)/[2.8, 3.0] = 1.45 - 0.1025/[2.8, 3.0] \subseteq [1.4133, 1.4159]$.
Since $N(X) \subseteq X$ and $0 \notin [2.8, 3.0]$, the interval Newton theorem shows that $f$ has exactly one zero in $X$, and it lies in $N(X)$.
Done with outward rounding, this proves $1.4133 \le \sqrt{2} \le 1.4159$.
Non-example: running Newton's method in floating point until two iterates agree to $15$ digits gives an excellent approximation, but no guarantee, so it is not a validated computation.