Related papers: Exact Constructive Digit-by-Digit Algorithms for I…

Based on a new coinductive characterization of continuous functions we extract certified programs for exact real number computation from constructive proofs. The extracted programs construct and combine exact real number algorithms with…

Many algorithms feature an iterative loop that converges to the result of interest. The numerical operations in such algorithms are generally implemented using finite-precision arithmetic, either fixed- or floating-point, most of which…

Exact representations of real numbers such as the signed digit representation or more generally linear fractional representations or the infinite Gray code represent real numbers as infinite streams of digits. In earlier work by the first…

This work presents and extends a known spigot-algorithm for computing square-roots, digit-by-digit, that is suitable for calculation by hand or an abacus, using only addition and subtraction. We offer an elementary proof of correctness for…

We present a structural resolution to the exact evaluation of the partition function $p_k(n)$, systematically overcoming the limitations of traditional recursive and asymptotic methods. By framing the partition polytope $\mathcal{P}_{n,k}$…

We present an approach (the biroot method) for nth root approximation that yields closed-form rational functions with coefficients derived from binomial structures, Gaussian functions, or qualifying DAG structures. The method emerges from…

We extract verified algorithms for exact real number computation from constructive proofs. To this end we use a coinductive representation of reals as streams of binary signed digits. The main objective of this paper is the formalisation of…

Floating-point arithmetic performance determines the overall performance of important applications, from graphics to AI. Meeting the IEEE-754 specification for floating-point requires that final results of addition, subtraction,…

We introduce a new approach to isolate the real roots of a square-free polynomial $F=\sum_{i=0}^n A_i x^i$ with real coefficients. It is assumed that each coefficient of $F$ can be approximated to any specified error bound. The presented…

We consider the problem of approximating all real roots of a square-free polynomial $f$. Given isolating intervals, our algorithm refines each of them to a width of $2^{-L}$ or less, that is, each of the roots is approximated to $L$ bits…

The real numbers are important in both mathematics and computation theory. Computationally, real numbers can be represented in several ways; most commonly using inexact floating-point data-types, but also using exact arbitrary-precision…

Let f be a univariate polynomial with real coefficients, f in R[X]. Subdivision algorithms based on algebraic techniques (e.g., Sturm or Descartes methods) are widely used for isolating the real roots of f in a given interval. In this…

Exact real computation is an alternative to floating-point arithmetic where operations on real numbers are performed exactly, without the introduction of rounding errors. When proving the correctness of an implementation, one can focus…

We propose an efficient algorithm to compute the real roots of a sparse polynomial $f\in\mathbb{R}[x]$ having $k$ non-zero real-valued coefficients. It is assumed that arbitrarily good approximations of the non-zero coefficients are given…

We give an algorithm for computing all roots of polynomials over a univariate power series ring over an exact field $\mathbb{K}$. More precisely, given a precision $d$, and a polynomial $Q$ whose coefficients are power series in $x$, the…

This paper contains an algebraic constructive and self-contained account of the invariance rule of the digital root under division for an arbitrary natural basis representation. Both the cases of repeating and non-repeating fractionals are…

It is well known that the R, the set of real numbers, is an abstract set, where almost all its elements cannot be described in any finite language. We investigate possible approaches to what might be called an epi-constructionist approach…

Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithms for achieving consistency in replicated systems are still…

We describe several algorithms for computing $e$-th roots of elements in a number field $K$, where $e$ is an odd prime-power integer. In particular we generalize Couveignes' and Thom\'e's algorithms originally designed to compute…

Lattice rules are among the most prominently studied quasi-Monte Carlo methods to approximate multivariate integrals. A rank-1 lattice rule to approximate an $s$-dimensional integral is fully specified by its generating vector $\mathbf{z}…