Bean: Backward Error Analysis

This is the artifact for Bean, a prototype implementation of the type system and floating-point backward error analysis tool described in the paper Bean: A Language for Backward Error Analysis. It implements the algorithm given in Section 5.1.

The examples given in Section 4 can be found under examples/. The benchmarks from Section 5.2 can be found under benchmarks/.

The type checker is based on the implementation due to Arthur Azevedo de Amorim and co-authors [1].

[1] Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, and Justin Hsu. 2014. Really Natural Linear Indexed Type Checking. In Proceedings of the 26nd 2014 International Symposium on Implementation and Application of Functional Languages (IFL '14). Association for Computing Machinery, New York, NY, USA, Article 5, 1–12. https://doi.org/10.1145/2746325.2746335

Getting started

Bean can be built manually or using the provided Docker image.

Build with Docker

If you have Docker, in the bean directory, run

docker build -t bean .

After the Docker image builds, you can enter a TTY with

docker run -it --rm bean

Build manually

This manual build has been tested on macOS 15.4. First, get opam >= 2.3 here. You need ocaml >= 5.1 plus dune >= 3.17 and menhir >= 20240715. Install them with

opam install [package]

or, in the bean directory, you can obtain everything with

opam install --deps-only .

Build Bean via dune:

dune build

Running a Bean program

Type check an example with the following command:

dune exec -- bean examples/InnerProduct.be

• Turn on debug output with the flag --debug or -d.
• Disable unicode printing with the flag --disable-unicode.
• Set unit roundoff to 2^(-n) with the flag --unit-roundoff <n> or -u <n>. Without this flag, we give the backward error bounds in terms of ε, where ε = u / (1 - u) and u is unit roundoff.

For example, run the InnerProduct Bean program with IEEE 754 double precision arithmetic as follows:

dune exec -- bean examples/InnerProduct.be -u 53

The program looks like this:

{(u : (dnum, dnum))}
{(v : (num, num))}
/*
    Computes the inner product of two vectors in R^2.
*/
dlet (u1, u2) = u;
let (v1, v2) = v;
let x = dmul u1 v1;
let y = dmul u2 v2;
add x y

Bean programs start with two lists of input variables: those that are discrete followed by those that are linear. The sole discrete input to InnerProduct is u : (dnum, dnum) while the sole linear input is v : (num, num). In a nutshell, this means that u and v are real vectors in ℝ²; however, v may have backward error while u may not.

The output is:

[General] Type of the program: ℝ
[General] Inferred linear context:
          v :[2.22e-16] (ℝ ⊗ ℝ)
Execution time: 0.000878s

The return type of InnerProduct is ℝ. The inferred context tells us that our input vector v has a backward error bound of 2.22e-16.

This means that there exists a vector