DedekindCutArithmetic.jl

A Julia library for exact real arithmetic using Dedekind cuts and Abstract Stone Duality. Heavily inspired by the Marshall programming language.

Installation

1. If you haven't already, install Julia. The easiest way is to install Juliaup. This allows to easily install and manage julia versions.

2. Open the terminal and start a julia session by typing julia.

3. Install the library by typing

   using Pkg; Pkg.add("DedekindCutArithmetic")

4. The package can now be loaded (in the interactive REPL or in a script file) with the command

   using DedekindCutArithmetic

5. That's it, have fun!

Quickstart example

The following snippet shows how to define the squareroot of a number and the maximum of a function $f: [0, 1] \rightarrow \mathbb{R}$ using Dedekind cuts. It also shows this definition is actually computable and can be used to give a tight rigorous bound of the value.

using DedekindCutArithmetic

# Textbook example of dedekind cuts, define square-root
my_sqrt(a) = @cut x ∈ ℝ, (x < 0) ∨ (x * x < a), (x > 0) ∧ (x * x > a)

# lazy computation, however it is automatically evaluated to 53 bits of precision if printed in the REPL.
sqrt2 = my_sqrt(2);

# evaluate to 80 bits precision, this gives an interval with width <2⁻⁸⁰ containing √2
refine!(sqrt2; precision=80)
# [1.4142135623730949, 1.4142135623730951]

# Define maximum of a function f: [0, 1] → ℝ as a Dedekind cut
my_max(f::Function) = @cut a ∈ ℝ, ∃(x ∈ [0, 1] : f(x) > a), ∀(x ∈ [0, 1] : f(x) < a)

f = x -> x * (1 - x)

fmax = my_max(f);

refine!(fmax) # evaluate to 53 bits of precision by default
# [0.24999999999999992, 0.25000000000000006]

Documentation

• STABLE: Documentation of the latest release
• DEV: Documentation of the in-development version on main

Contributing

Contributions are welcome! Here is a small decision tree with useful links. More details in the contributor's guide.

• There is a discussion section on GitHub. You can use the helpdesk category to ask for help on how to use the software or the show and tell category to simply share with the world your work using DedekindCutArithmetic.jl

• If you find a bug or want to suggest a new feature, open an issue.

• You are also encouraged to send pull requests (PRs). For small changes, it is ok to open a PR directly. For bigger changes, it is advisable to discuss it in an issue first. Before opening a PR, make sure to check the contributor's guide.

Copyright

• Copyright (c) 2024 Luca Ferranti, released under MIT license