From 1f9a63ee5349e7bc332697852c5b3d576b55801a Mon Sep 17 00:00:00 2001 From: lucaferranti Date: Fri, 25 Oct 2024 11:16:33 +0300 Subject: [PATCH 1/3] update documentation --- README.md | 48 ++++++--- docs/Project.toml | 4 +- docs/make.jl | 17 ++- docs/src/90-contributing.md | 2 +- docs/src/91-developer.md | 37 +++++-- docs/src/assets/citations.css | 17 +++ docs/src/index.md | 14 +-- docs/src/references.md | 4 + docs/src/refs.bib | 27 +++++ docs/src/tutorial.md | 194 ++++++++++++++++++++++++++++++++++ 10 files changed, 325 insertions(+), 39 deletions(-) create mode 100644 docs/src/assets/citations.css create mode 100644 docs/src/references.md create mode 100644 docs/src/refs.bib create mode 100644 docs/src/tutorial.md diff --git a/README.md b/README.md index dac1247..59036c6 100644 --- a/README.md +++ b/README.md @@ -1,21 +1,23 @@ # DedekindCutArithmetic.jl -[![license: MIT][license-img]][license-url] -[![Stable Documentation][stabledoc-img]][stabledoc-url] -[![In development documentation][devdoc-img]][devdoc-url] -[![Build Status][ci-img]][ci-url] -[![Coverage][cov-img]][cov-url] -[![Contributor Covenant](https://img.shields.io/badge/Contributor%20Covenant-2.1-4baaaa.svg)](CODE_OF_CONDUCT.md) -[![ColPrac: Contributor's Guide on Collaborative Practices for Community Packages][colprac-img]][colprac-url] -[![SciML Code Style][style-img]][style-url] +|**Info**|**Documentation**|**Build status**|**Contributing**| +|:------:|:--------------:|:---------------:|:--------------:| +|[![version][ver-img]][ver-url] [![license: MIT][license-img]][license-url]
[![DOI][doi-img]][doi-url]|[![Stable Documentation][stabledoc-img]][stabledoc-url] [![In development documentation][devdoc-img]][devdoc-url]|[![Build Status][ci-img]][ci-url] [![Coverage][cov-img]][cov-url]
[![pkgeval-img]][pkgeval-url]|[![Contributor Covenant][coc-img]][coc-url] [![ColPrac: Contributor's Guide on Collaborative Practices for Community Packages][colprac-img]][colprac-url]
[![SciML Code Style][style-img]][style-url]| A Julia library for exact real arithmetic using [Dedekind cuts](https://en.wikipedia.org/wiki/Dedekind_cut) and [Abstract Stone Duality](https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=02c685856371aac16ce81bf7467ffc4d533d48ff). Heavily inspired by the [Marshall](https://github.com/andrejbauer/marshall) programming language. -## Installation +## Table of Content -1. If you haven't already, install Julia. The easiest way is to install [Juliaup](https://github.com/JuliaLang/juliaup#installation). This allows to easily install and manage julia versions. +- [💾 Installation](https://github.com/lucaferranti/DedekindCutArithmetic.jl#--installation) +- [🌱 Quickstart example](https://github.com/lucaferranti/DedekindCutArithmetic.jl#--quickstart-example) +- [📚 Documentation](https://github.com/lucaferranti/DedekindCutArithmetic.jl#--documentation) +- [🤝 Contributing](https://github.com/lucaferranti/DedekindCutArithmetic.jl#--contributing) -2. Open the terminal and start a julia session by typing `julia`. +## 💾 Installation + +1. If you haven't already, install Julia. The easiest way is to install [Juliaup](https://github.com/JuliaLang/juliaup#installation). 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 @@ -31,9 +33,9 @@ A Julia library for exact real arithmetic using [Dedekind cuts](https://en.wikip 5. That's it, have fun! -## Quickstart example +## 🌱 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. +The following snippet shows how to define the square root 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 on the value. ```julia using DedekindCutArithmetic @@ -59,12 +61,12 @@ refine!(fmax) # evaluate to 53 bits of precision by default # [0.24999999999999992, 0.25000000000000006] ``` -## Documentation +## 📚 Documentation - [**STABLE**][stabledoc-url]: Documentation of the latest release - [**DEV**][devdoc-url]: Documentation of the in-development version on main -## Contributing +## 🤝 Contributing Contributions are welcome! Here is a small decision tree with useful links. More details in the [contributor's guide](https://lucaferranti.github.io/DedekindCutArithmetic.jl/dev/90-contributing). @@ -72,15 +74,21 @@ Contributions are welcome! Here is a small decision tree with useful links. More - If you find a bug or want to suggest a new feature, [open an issue](https://github.com/lucaferranti/DedekindCutArithmetic.jl/issues). -- 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](https://lucaferranti.github.io/DedekindCutArithmetic.jl/dev/90-contributing). +- 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 [developer's guide](https://lucaferranti.github.io/DedekindCutArithmetic.jl/dev/91-developer). -## Copyright +## 📜 Copyright - Copyright (c) 2024 [Luca Ferranti](https://github.com/lucaferranti), released under MIT license +[ver-img]: https://juliahub.com/docs/DedekindCutArithmetic/version.svg +[ver-url]: https://github.com/lucaferranti/DedekindCutArithmetic.jl/releases/latest + [license-img]: https://img.shields.io/badge/license-MIT-yellow.svg [license-url]: https://github.com/lucaferranti/DedekindCutArithmetic.jl/blob/main/LICENSE +[doi-img]: https://zenodo.org/badge/876330838.svg +[doi-url]: https://doi.org/10.5281/zenodo.13989059 + [stabledoc-img]: https://img.shields.io/badge/docs-stable-blue.svg [stabledoc-url]: https://lucaferranti.github.io/DedekindCutArithmetic.jl/stable @@ -93,6 +101,12 @@ Contributions are welcome! Here is a small decision tree with useful links. More [cov-img]: https://codecov.io/gh/lucaferranti/DedekindCutArithmetic.jl/branch/main/graph/badge.svg [cov-url]: https://codecov.io/gh/lucaferranti/DedekindCutArithmetic.jl +[pkgeval-img]: https://juliaci.github.io/NanosoldierReports/pkgeval_badges/D/DedekindCutArithmetic.svg +[pkgeval-url]: https://juliaci.github.io/NanosoldierReports/pkgeval_badges/D/DedekindCutArithmetic.html + +[coc-img]: https://img.shields.io/badge/Contributor%20Covenant-2.1-4baaaa.svg +[coc-url]: https://github.com/lucaferranti/DedekindCutArithmetic.jl/blob/main/CODE_OF_CONDUCT.md + [colprac-img]: https://img.shields.io/badge/ColPrac-Contributor's%20Guide-blueviolet [colprac-url]: https://github.com/SciML/ColPrac diff --git a/docs/Project.toml b/docs/Project.toml index 91789dd..53d3710 100644 --- a/docs/Project.toml +++ b/docs/Project.toml @@ -1,7 +1,9 @@ [deps] +DedekindCutArithmetic = "a9cf20ff-59c8-5762-8ce8-520b700dfeff" Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4" +DocumenterCitations = "daee34ce-89f3-4625-b898-19384cb65244" +IntervalArithmetic = "d1acc4aa-44c8-5952-acd4-ba5d80a2a253" LiveServer = "16fef848-5104-11e9-1b77-fb7a48bbb589" -DedekindCutArithmetic = "a9cf20ff-59c8-5762-8ce8-520b700dfeff" [compat] Documenter = "1" diff --git a/docs/make.jl b/docs/make.jl index af14fc8..48e1a3b 100644 --- a/docs/make.jl +++ b/docs/make.jl @@ -8,6 +8,13 @@ Pkg.activate(@__DIR__) using Documenter using DedekindCutArithmetic +using DocumenterCitations + +bib = CitationBibliography( + joinpath(@__DIR__, "src", "refs.bib"); + style = :numeric +) + ############### # CREATE HTML # ############### @@ -15,15 +22,19 @@ using DedekindCutArithmetic makedocs(; modules = [DedekindCutArithmetic], authors = "Luca Ferranti", sitename = "DedekindCutArithmetic.jl", - doctest = false, checkdocs = :exports, + doctest = false, checkdocs = :exports, plugins = [bib], format = Documenter.HTML(; prettyurls = IS_CI, collapselevel = 1, - canonical = "https://lucaferranti.github.io/DedekindCutArithmetic.jl"), + canonical = "https://lucaferranti.github.io/DedekindCutArithmetic.jl", + assets = String["assets/citations.css"] + ), pages = [ "Home" => "index.md", + "Tutorial" => "tutorial.md", "API" => "api.md", "Contributing" => ["90-contributing.md", "91-developer.md"], - "Release notes" => "changelog.md" + "Release notes" => "changelog.md", + "References" => "references.md" ]) ########## diff --git a/docs/src/90-contributing.md b/docs/src/90-contributing.md index c42bb48..d5f683a 100644 --- a/docs/src/90-contributing.md +++ b/docs/src/90-contributing.md @@ -27,7 +27,7 @@ We follow the [ColPrac guide for collaborative practices](https://github.com/Sci If you found an issue that interests you, comment on that issue what your plans are. If the solution to the issue is clear, you can immediately create a pull request. -Otherwise, say what yourfollow proposed solution is and wait for a discussion around it. +Otherwise, say what your proposed solution is and wait for a discussion around it. For small changes (typos, trivial bug fixes) it is ok to open a PR directly even without an associated issue. For non-trivial changes, please open an issue first. diff --git a/docs/src/91-developer.md b/docs/src/91-developer.md index 45d987f..e5291cd 100644 --- a/docs/src/91-developer.md +++ b/docs/src/91-developer.md @@ -3,7 +3,7 @@ !!! note "Contributing guidelines" If you haven't, please read the [Contributing guidelines](90-contributing.md) first. -If you want to make contributions to this package that involves code, then this guide is for you. +If you want to make contributions to this package, then this guide is for you. ## First time clone @@ -12,9 +12,9 @@ If you want to make contributions to this package that involves code, then this If this is the first time you work with this repository, follow the instructions below to clone the repository. -1. Fork this repo -2. Clone your repo (this will create a `git remote` called `origin`) -3. Add this repo as a remote: +1. Fork this repository +2. Clone your fork (this will create a `git remote` called `origin`) +3. Add the original repository as a remote: ```bash git remote add upstream https://github.com/lucaferranti/DedekindCutArithmetic.jl @@ -23,18 +23,21 @@ If this is the first time you work with this repository, follow the instructions This will ensure that you have two remotes in your git: `origin` and `upstream`. You will create branches and push to `origin`, and you will fetch and update your local `main` branch from `upstream`. +!!! warning "Warning" + From now on, these instructions assume you are in the `DedekindCutArithmetic.jl` folder + ## Linting and formatting Install a plugin on your editor to use [EditorConfig](https://editorconfig.org). This will ensure that your editor is configured with important formatting settings. We use [https://pre-commit.com](https://pre-commit.com) to run the linters and formatters. -In particular, the Julia code is formatted using [JuliaFormatter.jl](https://github.com/domluna/JuliaFormatter.jl), so please install it globally first: +In particular, the Julia code is formatted using [JuliaFormatter.jl](https://github.com/domluna/JuliaFormatter.jl), so please install it globally first as follows (the following snippet is copy-pastable into the REPL) ```julia-repl -julia> # Press ] -pkg> activate -pkg> add JuliaFormatter +julia> import Pkg; +pkg> Pkg.activate(); +pkg> Pkg.add("JuliaFormatter") ``` To install `pre-commit`, we recommend using [pipx](https://pipx.pypa.io) as follows: @@ -68,6 +71,12 @@ pkg> activate . pkg> test ``` +Each test file is also stand-alone, hence to run a specific file you can `include` that from the REPL + +```julia-repl +julia> include("test/test-cuts.jl") +``` + ## Working on a new issue We try to keep a linear history in this repo, so it is important to keep your branches up-to-date. @@ -126,13 +135,21 @@ We try to keep a linear history in this repo, so it is important to keep your br ## Building and viewing the documentation locally -To build the documentation locally, simply run +The first time you want to build the documentation locally, you will need to install all needed dependencies. To do so, run + +```bash +julia docs/setup.jl +``` + +This needs to be done the fist time (i.e. if you don't have a `docs/Manifest.toml` file). The setup script needs to be rerun only if some external libraries used in the documentation example change. + +Next, you can build the documentation locally by running ```bash julia docs/liveserver.jl ``` -This will build the documentation and open a preview in your browser. Whenever you make some changes in the documentation files, the preview will also update live. +This will open a preview of the documentation in your browser and watch the documentation source files, meaning the preview will automatically update on every documentation file change. ## Making a new release diff --git a/docs/src/assets/citations.css b/docs/src/assets/citations.css new file mode 100644 index 0000000..53f1937 --- /dev/null +++ b/docs/src/assets/citations.css @@ -0,0 +1,17 @@ +.citation dl { + display: grid; + grid-template-columns: max-content auto; } + .citation dt { + grid-column-start: 1; } + .citation dd { + grid-column-start: 2; + margin-bottom: 0.75em; } + .citation ul { + padding: 0 0 2.25em 0; + margin: 0; + list-style: none !important;} + .citation ul li { + text-indent: -2.25em; + margin: 0.33em 0.5em 0.5em 2.25em;} + .citation ol li { + padding-left:0.75em;} diff --git a/docs/src/index.md b/docs/src/index.md index f71496b..28ef430 100644 --- a/docs/src/index.md +++ b/docs/src/index.md @@ -6,11 +6,11 @@ CurrentModule = DedekindCutArithmetic A Julia library for exact real arithmetic using [Dedekind cuts](https://en.wikipedia.org/wiki/Dedekind_cut) and [Abstract Stone Duality](https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=02c685856371aac16ce81bf7467ffc4d533d48ff). Heavily inspired by the [Marshall](https://github.com/andrejbauer/marshall) programming language. -## Installation +## 💾 Installation -1. If you haven't already, install Julia. The easiest way is to install [Juliaup](https://github.com/JuliaLang/juliaup#installation). This allows to easily install and manage julia versions. +1. If you haven't already, install Julia. The easiest way is to install [Juliaup](https://github.com/JuliaLang/juliaup#installation). This allows to easily install and manage Julia versions. -2. Open the terminal and start a julia session by typing `julia`. +2. Open the terminal and start a Julia session by typing `julia`. 3. Install the library by typing @@ -26,9 +26,9 @@ A Julia library for exact real arithmetic using [Dedekind cuts](https://en.wikip 5. That's it, have fun! -## Quickstart example +## 🌱 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. +The following snippet shows how to define the square root 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 on the value. ```julia using DedekindCutArithmetic @@ -54,7 +54,7 @@ refine!(fmax) # evaluate to 53 bits of precision by default # [0.24999999999999992, 0.25000000000000006] ``` -## Contributing +## 🤝 Contributing Contributions are welcome! Here is a small decision tree with useful links. More details in the [contributor's guide](https://lucaferranti.github.io/DedekindCutArithmetic.jl/dev/90-contributing). @@ -62,7 +62,7 @@ Contributions are welcome! Here is a small decision tree with useful links. More - If you find a bug or want to suggest a new feature, [open an issue](https://github.com/lucaferranti/DedekindCutArithmetic.jl/issues). -- 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](https://lucaferranti.github.io/DedekindCutArithmetic.jl/dev/90-contributing). +- 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 [developer's guide](https://lucaferranti.github.io/DedekindCutArithmetic.jl/dev/91-developer). ## Copyright diff --git a/docs/src/references.md b/docs/src/references.md new file mode 100644 index 0000000..78f29bc --- /dev/null +++ b/docs/src/references.md @@ -0,0 +1,4 @@ +# References + +```@bibliography +``` diff --git a/docs/src/refs.bib b/docs/src/refs.bib new file mode 100644 index 0000000..e0a99ad --- /dev/null +++ b/docs/src/refs.bib @@ -0,0 +1,27 @@ +@article{bauer2009dedekind, + title={The Dedekind reals in abstract Stone duality}, + author={Bauer, Andrej and Taylor, Paul}, + journal={Mathematical structures in computer science}, + volume={19}, + number={4}, + pages={757--838}, + year={2009}, + publisher={Cambridge University Press} +} + +@inproceedings{bauer2008efficient, + title={Efficient computation with Dedekind reals}, + author={Bauer, Andrej}, + booktitle={Fifth International Conference on Computability and Complexity in Analysis,(Eds. V Brattka, R Dillhage, T Grubba, A Klutch), Hagen, Germany}, + year={2008}, + organization={Citeseer} +} + +@misc{marshall, + author = {Bauer, Andrej}, + title = {Marshall}, + year = {2012}, + publisher = {GitHub}, + journal = {GitHub repository}, + url = {https://github.com/andrejbauer/marshall}, +} diff --git a/docs/src/tutorial.md b/docs/src/tutorial.md new file mode 100644 index 0000000..4cfcb64 --- /dev/null +++ b/docs/src/tutorial.md @@ -0,0 +1,194 @@ +# Basic Tutorial + +This tutorial will guide you through the basic functionalities of `DedekindCutArithmetic.jl`. These examples assume you have loaded the library with + +```@repl tutorial1 +using DedekindCutArithmetic +``` + +## Motivation: What is exact real arithmetic? + +Whenever doing computations, we need to face the problem of rounding errors. Standard techniques to cope with it are + +- *floating point arithmetic*: use 64 bits or 32 bits to approximate real numbers. This is what happens by default when you type `0.1` in the julia REPL. It is the fastest of the options, but also loses accuracy the fastest. +- *arbitrary precision floating point arithmetic*: Set an arbitrary (within machine memory limits) precision *a priori* and do all computations using that precision. In Julia, this is achieved using `BigFloat`, which uses the C library MPFR under the hood. By default, it uses 256 bits of precision. This allows more accurate computations, but rounding error will still accumulate and for big enough inputs or long enough computations a significant loss of accuracy may still occur. +- *interval arithmetic*: Use intervals instead of numbers and perform all operations so that the resulting interval contains the true result. This will give a rigorous bound of the error. However, for several factors (directed rounding, dependency problem, wrapping effect) the width of the interval may grow too big and give an uninformative result. + +An alternative approach is *exact real arithmetic*, which sets a target precision and outputs the final result with that precision. The main difference from e.g. MPFR, is that here the precision is dynamic and is increased during computation. Everything has a tradeoff of course, and exact real arithmetic can be slower than MPFR or interval arithmetic, especially for long complex computations. + +The following snippets gives a motivation example for exact real arithmetic. Obviously, ``(1 + a) - a`` should alwyas be ``1``. However, we get a complete wrong answer both with 64 and 256 bits of precision. With interval arithmetic, we get an interval containing the correct answer, but too wide to be informative. With exact real arithmetic we get a sharp bound on the correct value. + +```@repl tutorial1 +a_float = sqrt(2.0^520/3) +res_float = (1 + a_float) - a_float + +a_mpfr = sqrt(big(2)^520/3) +res_mpfr = (1 + a_mpfr) - a_mpfr + +using IntervalArithmetic + +a_interval = sqrt(interval(big(2)^520//3)) +res_interval = (interval(1) + a_interval) - a_interval + +a_era = sqrt(RationalCauchyCut(big(2)^520//3)) +res_era = (1 + a_era) - a_era +``` + +There are different approaches to exact real arithmetic. This library builds on the theoretical framework based on Dedekind cuts and Abstract stone duality, proposed in [bauer2008efficient, bauer2009dedekind](@cite) and first implemented in [marshall](@cite). Next, the basic functionalities of this library are presented. + +## Dyadic numbers + +The fundamental building block of our arithmetic is *dyadic numbers*, that is, a number in the form ``\frac{m}{e^{-k}}`` with ``m\in\mathbb{Z},e\in\mathbb{N}``. We will denote the set of dyadic reals as ``\mathbb{D}``. + +These can be built in the libary using [`DyadicReal`](@ref) + +Dyadic reals are closed under addition, subtraction and multiplication. + +```@repl tutorial1 +d1 = DyadicReal(1, 2) # represents 1 ⋅ 2⁻² +d2 = DyadicReal(2) +d1 + d2 +d1 - d2 +d1 * d2 +``` + +!!! warning "Warning" + Division is currently not supported + +## Dyadic interval + +There is plenty of real numbers which are not dyadic, for example ``0.1, \sqrt{2},\pi`` and so on so forth. What we will want to do, we will want a [`DyadicInterval`](@ref) ``[a, b]`` with ``a,b`` dyadic reals, which bounds the value we want to approximate. These intervals can be manipulated using interval arithmetic. + +```@repl tutorial1 +i1 = DyadicInterval(1, 2) +i2 = DyadicInterval(DyadicReal(1, 1), DyadicReal(1, 2)) + +i1 + i2 +i1 - i2 +i1 * i2 +``` + +An important thing to notice is that our library relies on *Kaucher interval arithmetic*, which allows generalized intervals ``[a, b]`` with ``a > b``. + +```@repl tutorial1 +i = DyadicInterval(3, 1) +``` + +!!! warning "Warning" + Division is currently not supported + +## Defining cuts + +We finally get to the main data structure of the library: [`DedekindCut`](@ref). The intuitive idea of a dedekind cut to define a real number ``x`` is the following + +1. Find a set ``L\subset \mathbb{D}`` so that each element in ``L`` is strictly smaller than ``x`` +2. Find a set ``U \subset \mathbb{D}`` so that each element in ``U`` is strictly bigger than ``x``. +3. To get better and better approximations of ``x``, keep increasing the upper bound of ``L`` and decreasing the lower bound of ``U``, this will give a dyadic interval that shrinks around ``x``. + +### Baby example + +Let us first see a very trivial example, to get a taste of how to build dedekind cuts in practice in the library. Suppose we want to define the number ``2`` as a Dedekind cut. This is of course dummy, since that is a dyadic number and we could simply do `DyadicReal(2)` to get the exact value. + +To define a cut, we need to find an expression for the lower set and upper set. In this case, we simply have + +- **Lower set**: ``\{x \in \mathbb{D}: x < 2\}`` +- **Upper set**: ``\{x \in \mathbb{D}: x > 2\}`` + +Dedekind cuts can be built with the [`@cut`](@ref) macro and the syntax is the + +```julia +@cut var_name ∈ domain, lower_set_expression, upper_set_expression +``` + +If we have no idea where the the number we are defining lies on the real line, we can use ``\mathbb{R}`` for the domain. Alternatively, if we know that it lies in an interval ``[a, b]``, we can restrict the domain to that interval. This will often lead to faster approximations. Let's see this in practice + +```@repl tutorial1 +my2 = @cut x ∈ ℝ, x < 2, x > 2; +``` + +By default, this performs a *lazy* computation, that is, nothing has actually been computed so far. We can now get an arbitrary good approximation of ``\sqrt{2}`` using [`refine!`](@ref) function. + +```@repl tutorial1 +refine!(my2) # uses 53 bits of precision by default +``` + +The number can be queried at different precisions using the `precision` keyword. Refining to a precision `k` will produce a dyadic interval with width smaller than ``2^{-k}``. + +```@repl tutorial1 +refine!(my2; precision=80) +``` + +It is worth mentioning that for printing, the expression is evaluated to 53 bits of precision (that is, same of a 64-bits float), hence the following in the REPL is not entirely lazy. To have a lazy computation in the REPL, suppress the output with `;` + +```@repl tutorial1 +@cut x ∈ [0, 3], x < 2, x > 2 +``` + +!!! warning "Warning" + Unbounded intervals are not really supported, infinity is replaced by `big(typemax(Int))` during macro expansion. + +### Square root as Dedekind cut + +Let's see an example, suppose we want to define ``\sqrt{a}`` for arbitrary dyadic ``a``. We need to find a suitable expression for ``L`` and ``U``. + +- **Lower set**: Since ``\sqrt{a}`` is positive, then all negative ``x`` will be smaller than ``\sqrt{a}`` and hence belong to ``L``. For positive ``x``, we have ``x < \sqrt{a} \leftrightarrow x \cdot x < a``. This gives an expression for the lower set + +```math +L = \{x \in \mathbb{D} : x < 0 \lor x \cdot x < 0\} +``` + +- **Upper set**: Similarly, for a number to possibly be greater than ``sqrt{a}``, it will need to be positive. Furthermore for positive ``x`` we have ``x > \sqrt{a} \leftrightarrow x \cdot x > a``, giving the expression + +```math +L = \{x \in \mathbb{D} : x > 0 \land x \cdot x > 0\} +``` + +In the library, this can be implemented using the [`@cut`](@ref) macro. We can now define a function that computes the square root of a number using dedekind cuts. + +```@repl tutorial1 +my_sqrt(a) = @cut x ∈ ℝ, (x < 0) ∨ (x * x < a), (x > 0) ∧ (x * x > a) +``` + +We can now use it to compute the ``\sqrt{2}`` to an arbitrary precision + +```@repl tutorial1 +sqrt2 = my_sqrt(2); +isqrt2 = refine!(sqrt2; precision=80) +``` + +and verify that the desired accuracy is achieved + +```@repl tutorial1 +width(isqrt2) +width(isqrt2) < DyadicReal(1, 80) +``` + +## Cuts with quantifiers + +So far we have seen how to define numbers whose cuts can be expressed using propositional logic. We can however do better. Namely, we can use first-order logic, i.e. quantifiers like ``\forall`` and ``\exists`` to define more elaborated cuts. + +Let us now see how to define the maximum of a function with domain ``[0, 1]``. Again, we need to define the lower and upper set. + +**Lower set**: if ``a \in L``, it is smaller than the maximum, i.e. there will be an element in the domain of the function for which ``f(x) > a``, this gives us the expression + +```math +L = \{a \in \mathbb{D} : \exists x \in [0, 1] : f(x) > a\} +``` + +**Upper set**: if ``a \in U``, it is greater than the maximum, which means it is also greater than ``f(x)`` for every ``x`` in the domain, this gives us + +```math +U = \{a \in \mathbb{D} : \forall x \in [0, 1] : f(x) < a\} +``` + +The `@cut` macro supports parsing quantifiers with a very similar syntax + +```@repl tutorial1 +my_max(f::Function) = @cut a ∈ ℝ, ∃(x ∈ [0, 1] : f(x) > a), ∀(x ∈ [0, 1] : f(x) < a) +``` + +we can now use that to compute the maximum of ``f(x) = x(1 - x)``, which should be ``\frac{1}{4}`` + +```@repl tutorial1 +my_max(x -> x * (1 - x)) +``` From ca289bf4e43e4367edce43d1b17e1bb0eb2c615a Mon Sep 17 00:00:00 2001 From: lucaferranti Date: Fri, 25 Oct 2024 11:17:55 +0300 Subject: [PATCH 2/3] try fix link issue --- .lychee.toml | 1 + 1 file changed, 1 insertion(+) diff --git a/.lychee.toml b/.lychee.toml index bc896cf..612e3af 100644 --- a/.lychee.toml +++ b/.lychee.toml @@ -1,5 +1,6 @@ exclude = [ "@ref", + "@cite", "^https://github.com/.*/releases/tag/v.*$", "^https://doi.org/FIXME$", "^https://lucaferranti.github.io/DedekindCutArithmetic.jl/stable$", From dcdfb0338424c015fc376d9a9784fa4894a1e92e Mon Sep 17 00:00:00 2001 From: lucaferranti Date: Fri, 25 Oct 2024 11:34:40 +0300 Subject: [PATCH 3/3] reference tutorial in readme --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 59036c6..ae7e552 100644 --- a/README.md +++ b/README.md @@ -66,6 +66,8 @@ refine!(fmax) # evaluate to 53 bits of precision by default - [**STABLE**][stabledoc-url]: Documentation of the latest release - [**DEV**][devdoc-url]: Documentation of the in-development version on main +A good starting point is the [beginner tutorial](https://lucaferranti.github.io/DedekindCutArithmetic.jl/dev/tutorial/) + ## 🤝 Contributing Contributions are welcome! Here is a small decision tree with useful links. More details in the [contributor's guide](https://lucaferranti.github.io/DedekindCutArithmetic.jl/dev/90-contributing).