Reference

DedekindCutArithmetic

Julia library implementing exact real arithmetic using Dedekind cuts and abstract stone duality.

Abstract type for a generic cut.

Abstract type representing a generic real number.

Represents a dyadic number or a dyadic interval.

Composite cut lazily representing the result of applying an arithmetic binary operation f to child1 and child2.

Representation of a real number $x$ as a dedekind cut.

Fields

• low : function approximating the number from below. Evaluates to true for every number $< x$.
• high : function approximating the number from above. Evaluates to true for every number $> x$.
• mpa : Cached most precise approximation computed so far. This is a dyadic interval bound $x$ which is updated every time the cut is refined to a higher precision.

Represents an interval with lower and uppper bound expressed as dyadic numbers. Note this is a generalized interval, that is, the lower bound can be greater than the upper bound.

Represents a dyadic number in the form $\frac{m}{2^{-e}}$, with $d ∈ ℤ$ and $e ∈ ℕ$.

This represents a dyadic interval [(m-1)/2^e, (m+1)/2^e] approximating a non-dyadic rational number.

This is a special-case of Dedekind cut representing a rational number for which we do not need iterative refinement

Composite cut lazily representing the result of applying an arithmetic unary operation f to child.

Split the interval in two halves.

Given the interval $[a, b]$, return its dual $[b, a]$.

Check whether $∃ x ∈ dom : f(x) < 0$

Check whether $∀ x ∈ dom : f(x) < 0$

Right endpoint of the dyadic interval.

Returns true if the lower bound is strictly bigger than the upper bound.

Returns true if the lower bound is smaller or equal of the upper bound.

Left endpoint of the dyadic interval.

Given precision p and interval i, compute a precision which is better than p and is suitable for working with intervals of width i.

Taken from: https://github.com/andrejbauer/marshall/blob/c9f1f6466e879e8db11a12b9bc030e62b07d8bd2/src/eval.ml#L22-L26

Midpoint of the dyadic interval

Whether or not the given dyadic intervals overlap.

Transformations on the expression before being processed by @cut

Half the width of the given interval.

Refine the given cut to give an approximation with precision bits of accuracy. If the required accuracy cannot be achieved within max_iter iterations, return the current estimate with a warning.

Evaluate the Cauchy sequence representing a rational number with n bits of precision.

Return two points that divide the interval in three parts with ratio 1/4, 1/2, 1/2

Width of the dyadic interval.

Note this is always positive, also for improper intervals.

Macro to construct a DedekindCut.

A cut is defined using the following syntax

@cut x ∈ [a, b], low, high

This defines a real number $x$ in the interval $[a, b]$ which is approximated by the inequality $φ(x)$ from below and $ψ(x)$ from above.

$φ$ and $ψ$ can be any julia expression, also referring to variables in the scope where the macro is called.

Similarly, $a$ and $b$ can also be julia expressions, but they cannot depend on $x$.

Parse a decimal literal into an exact real

julia> a = exact"0.1"
[0.099999999999999867, 0.10000000000000009]

julia> refine!(a; precision = 80)
[0.099999999999999992, 0.10000000000000001]

This is needed because literals are already parsed before constructing the AST, hence when writing :(x - 0.1) one would get the floating point approximation of 1//10 instead of the exact rational.

Check whether $∃ x ∈ dom : prop(x)$

Check whether $∀ x ∈ dom : prop(x)$