Herbie uses the FPCore format to specify an input program, and has extensive options for precisely describing its context.

FPCore format looks like this:

(FPCore (inputs ...)properties ...expression)

(FPCorename(inputs ...)properties ...expression)

Each `input` is a variable name, like `x`

,
used in the `expression`. Properties are used to specify
additional information about the `expression`'s context.
As of version 1.5, Herbie supports named functions.
If `name` is specified, the function can be inlined
within any subsequent FPCore in the file.

The expression is written in prefix form, with every function call
parenthesized, as in Lisp. For example, the formula for the
hypotenuse of a triangle with legs *a* and *b* is:

(FPCore (a b) (sqrt (+ (* a a) (* b b))))

The semicolon (`;`) character introduces a line comment.
We recommend the `.fpcore`

file extension for Herbie input files.

Herbie supports all functions from math.h with floating-point-only inputs and outputs. The best supported functions include:

`+`

,`-`

,`*`

,`/`

,`fabs`

- The usual arithmetic functions
`sqrt`

,`cbrt`

- Square and cube roots
`pow`

,`exp`

,`log`

- Various exponentiations and logarithms
`sin`

,`cos`

,`tan`

- The trigonometric functions
`asin`

,`acos`

,`atan`

,`atan2`

- The inverse trigonometric functions
`sinh`

,`cosh`

,`tanh`

- The hyperbolic functions
`asinh`

,`acosh`

,`atanh`

- The inverse hyperbolic functions
`fma`

,`expm1`

,`log1p`

,`hypot`

- Specialized numeric functions

Herbie also supports the constants `PI`

and `E`

. The arithmetic operators associate to the left,
and `-`

is used for both subtraction and negation.

Herbie links against your computer's `libm`

to
evaluate these functions. So, each function has the same behavior in
Herbie as in your code.

On Windows, the Bessel functions are not available in the
system `libm`

, so Herbie will use a fallback
implementation and print a warning. Turn off the
the `precision:fallback` option
to disable those functions instead.

FPCore uses `if`

for conditional expressions:

(ifcondif-trueif-false)

The conditional

may use:
`cond`

`==`

,`!=`

,`<`

,`>`

,`<=`

,`>=`

- The usual comparison operators
`and`

,`or`

,`not`

- The usual logical operators
`TRUE`

,`FALSE`

- The two boolean values

The comparison functions implement chained comparisons with more than two arguments.

Intermediate variables can be defined
using `let`

and `let*`

:

(let ([variablevalue]...)body)

In both `let`

and `let*`

,
each `variable` is bound to its `value` and can be
used in the `body`. The difference between `let`

and `let*`

is what order the values are
evaluated in:

`let`

expressions- In a
`let`

expression, all the values are evaluated in parallel, before they are bound to their variables. This means that later values can't refer to earlier variables in the same`let`

block. `let*`

expressions- A
`let*`

block looks the same as a`let`

block, except the values are evaluated one at a time, and later values can refer to earlier variables.

Note that Herbie treats intermediate values only as a notational convenience, and inlines their values before improving the formula's accuracy. Using intermediate variables will not help Herbie improve a formula's accuracy or speed up its run-time.

By default, the arguments to formulas are assumed to be
arbitrarily large or small floating-point numbers. However, in most
programs a smaller range of argument values is possible.
The `:pre`

property (for “precondition”) describes this
smaller range.

Preconditions use comparison and boolean operators, just like conditional statements:

(FPCore (x) :pre (< 1 x 10) (/ 1 (- x 1)))

Herbie is particularly efficient when when the precondition is
an `and`

of ranges for each variable, but more complex
preconditions also work.

Herbie supports both single- and double-precision values; you can
specify the precision with the `:precision`

property:

`binary32`

- Single-precision IEEE-754 floating point
`binary64`

- Double-precision IEEE-754 floating point
`racket`

- Like
`binary64`

, but using Racket math functions rather than your computer's`libm`

.

By default, `binary64`

is assumed. Herbie also has
a plugin system to load additional
precisions.

Herbie supports conversions between different precisions.
All conversions are assumed to be bi-directional. You can
specify conversions with the `:herbie-conversions`

property.

`:herbie-conversions`

([`prec1``prec2`] ...)- If an expression is computed with precision
`prec1`

, Herbie is allowed to rewrite all (or some) of the expression so it is computed with precision`prec2`

and vice versa.

For example, to let Herbie introduce single-precision
code when `:precision`

is set to `binary64`

or vice versa,
specify `:herbie-conversions ((binary64 binary32))`

In some cases, your input program is an approximation of some
more complex mathematical expression. The `:spec`

(for
“specification”) lets you specify the more complex ideal case.
Herbie will then try to modify the input program to make it more
accurately evaluate the specification.

For example, suppose you want to evaluate `sin(1/x)`

via a series expansion. Write:

(FPCore (x) :spec (sin (/ 1 x)) (+ (/ 1 x) (/ 1 (* 6 (pow x 3)))))

Herbie will only use the `:spec`

expression to
evaluate error, not to search for accurate expressions.

Herbie uses the `:name`

property to name FPCores in
its UI. Its value ought to be a string.

Herbie's output provide additional information in custom properties:

`:herbie-status`

`status``status`describes whether Herbie worked: it is one of`success`

,`timeout`

,`error`

, or`crash`

.`:herbie-time`

`ms`- The time, in milliseconds, used by Herbie to find a more accurate formula.
`:herbie-error-input`

([`pts``err`] ...)- The average
`err`or of the input program at`pts`points. Multiple entries correspond to Herbie's training and test sets. `:herbie-error-output`

([`pts``err`] ...)- The computed average error of the output program, similar to
`:herbie-error-input`

.

Herbie's benchmark suite also uses properties such
as `:herbie-target`

for continuous integration, but these
are not supported and their use is discouraged.