diff --git a/README.md b/README.md index 28541e4..90bc9db 100644 --- a/README.md +++ b/README.md @@ -13,9 +13,9 @@ A Julia library for exact real arithmetic using [Dedekind cuts](https://en.wikip ## 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 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 simply typing `julia` +2. Open the terminal and start a julia session by typing `julia`. 3. Install the library by typing @@ -33,7 +33,7 @@ A Julia library for exact real arithmetic using [Dedekind cuts](https://en.wikip ## Quickstart example -The following snippet shows how to define the maximum of a function $f: [0, 1] \rightarrow \mathbb{R}$ using Dedekind cuts and how to use it to actually compute the maximum of a given function. +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. ```julia using DedekindCutArithmetic @@ -41,12 +41,14 @@ 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) -sqrt2 = my_sqrt(2); # lazy computation, however it is evaluated to 53 bits precision when printing +# lazy computation, however it is automatically evaluated to 53 bits of precision if printed in the REPL. +sqrt2 = my_sqrt(2); -refine!(sqrt2; precision=80) # evaluate to 80 bits precision +# 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 +# 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) @@ -60,7 +62,7 @@ refine!(fmax) # evaluate to 53 bits of precision by default ## Documentation - [**STABLE**][stabledoc-url]: Documentation of the latest release -- [**DEV**][devdoc-url]: Documentation of the version on main +- [**DEV**][devdoc-url]: Documentation of the in-development version on main ## Contributing diff --git a/docs/make.jl b/docs/make.jl index cd3c4f6..bbebd4e 100644 --- a/docs/make.jl +++ b/docs/make.jl @@ -21,7 +21,6 @@ makedocs(; canonical = "https://lucaferranti.github.io/DedekindCutArithmetic.jl"), pages = [ "Home" => "index.md", - "Tutorial" => "tutorial.md", "API" => "api.md", "Contributing" => ["90-contributing.md", "91-developer.md"] ]) diff --git a/docs/src/90-contributing.md b/docs/src/90-contributing.md index 87c9d88..c42bb48 100644 --- a/docs/src/90-contributing.md +++ b/docs/src/90-contributing.md @@ -15,7 +15,7 @@ All interactions should folow the [Code of Conduct](https://github.com/lucaferra If you need help using `DedekindCutArithmetic.jl`, you can use the [helpdesk](https://github.com/lucaferranti/DedekindCutArithmetic.jl/discussions/categories/helpdesk) category to ask for help. This is preferable over issues, which are meant for bugs and feature requests, because discussions do not get closed once fixed and remain browsable for others. -There is also a [show and tell](https://github.com/lucaferranti/DedekindCutArithmetic.jl/discussions/categories/show-and-tell) category to share with the world your work using DedekindCutArithmetic.jl. If your work involves a new application of `DedekindCutArithmetic.jl` and you also want it featured in the Applications section in the documentation, let us know (in the element chat or in an issue). You will get help with the workflow and setup, but you are expected to do the writing 😃 . +There is also a [show and tell](https://github.com/lucaferranti/DedekindCutArithmetic.jl/discussions/categories/show-and-tell) category to share with the world your work using DedekindCutArithmetic.jl. If your work involves a new application of `DedekindCutArithmetic.jl` and you also want it featured in the Applications section in the documentation, let us know. You will get help with the workflow and setup, but you are expected to do the writing 😃 . ## Opening issues diff --git a/docs/src/index.md b/docs/src/index.md index 73fb8a1..f71496b 100644 --- a/docs/src/index.md +++ b/docs/src/index.md @@ -2,6 +2,68 @@ CurrentModule = DedekindCutArithmetic ``` -# DedekindCutArithmetic +# DedekindCutArithmetic.jl -Documentation for [DedekindCutArithmetic](https://github.com/lucaferranti/DedekindCutArithmetic.jl). +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 + +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 + + ```julia + using Pkg; Pkg.add("DedekindCutArithmetic") + ``` + +4. The package can now be loaded (in the interactive REPL or in a script file) with the command + + ```julia + 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. + +```julia +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] +``` + +## 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). + +- There is a [discussion section](https://github.com/lucaferranti/DedekindCutArithmetic.jl/discussions) on GitHub. You can use the [helpdesk](https://github.com/lucaferranti/DedekindCutArithmetic.jl/discussions/categories/helpdesk) category to ask for help on how to use the software or the [show and tell](https://github.com/lucaferranti/DedekindCutArithmetic.jl/discussions/categories/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](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). + +## Copyright + +- Copyright (c) 2024 [Luca Ferranti](https://github.com/lucaferranti), released under MIT license diff --git a/docs/src/tutorial.md b/docs/src/tutorial.md deleted file mode 100644 index e69de29..0000000 diff --git a/src/interval.jl b/src/interval.jl index 143ce18..dd83164 100644 --- a/src/interval.jl +++ b/src/interval.jl @@ -122,7 +122,7 @@ Base.:>=(i1::AbstractDyadic, i2::AbstractDyadic) = low(i1) >= high(i2) ######### """ -Given precision `p` and interval `i``, compute a precision which is better than `p` and +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 diff --git a/test/test-cuts.jl b/test/test-cuts.jl index 1281655..03351d0 100644 --- a/test/test-cuts.jl +++ b/test/test-cuts.jl @@ -43,4 +43,4 @@ end @test ifmax == fmax.mpa @test BigFloat(width(fmax)) <= 0x1p-53 @test low(fmax) < 1 // 4 < high(fmax) -end \ No newline at end of file +end diff --git a/test/test-interval.jl b/test/test-interval.jl index 4f365f3..eb0a4f5 100644 --- a/test/test-interval.jl +++ b/test/test-interval.jl @@ -49,4 +49,4 @@ end @test !(DyadicInterval(0, 2) < DyadicInterval(1, 3)) @test !(DyadicInterval(1, 3) > DyadicInterval(0, 2)) -end \ No newline at end of file +end