Herbie uses the FPCore format to specify an input program, and has extensive options for precisely describing its context.
The Herbie web shell takes input in a subset of the math.js syntax. The web shell automatically checks for syntax errors, and provides a graphical user interface for specifying the input domain. The web shell converts the mathematical expression and input ranges into FPCore before sending it to Herbie.
Herbie's command-line and batch-mode tools use FPCore format to describe mathematical expressions. FPCore looks like this:
(FPCore (inputs ...) properties ... expression)
(FPCore name (inputs ...) properties ... expression)
Each input is a variable name, like
used in the expression. Properties are used to specify
additional information about the expression's context.
If name is specified, the function can be referenced in
subsequent FPCore declarations 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:
Herbie also supports the constants
E. The arithmetic operators associate to the left,
- is used for both subtraction and negation.
Herbie links against your computer's
evaluate these functions. So, each function has the same behavior in
Herbie as in your code. You can instead use
racket precision if you
instead want reproducible behavior.
if for conditional expressions:
(if cond if-true if-false)
cond may use:
The comparison functions support chained comparisons with more than two arguments.
Intermediate variables can be defined
(let ([variable value] ...) body)
(let* ([variable value] ...) body)
each variable is bound to its value and can be
used in the body. The difference between
let* is what order the values are
letexpression, 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 looks the same as a
letblock, except the values are evaluated one at a time, and later values can refer to earlier variables.
Unless you have a lot of Lisp experience, you'll probably
let* more intuitive.
Internally, Herbie treats intermediate values only as a notational convenience, and inlines their values before improving the formula's accuracy. Using intermediate variables will therefore not produce a more accurate result or help Herbie run faster.
In some cases, your input program is an approximation of some
more complex mathematical expression. The
“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
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.
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.
:pre property (for “precondition”) describes this
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
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
binary64, but using Racket math functions rather than your computer's
binary64 is assumed. Herbie also has
a plugin system to load additional
Herbie won't produce mixed-precision code unless you allow it to
do so, using the
([prec1 prec2] ...)
prec1, can be rewriten to use precision
prec2, and vice versa.
All conversions are assumed to be bidirectional. For example, if
:herbie-conversions ([binary64 binary32]),
Herbie will be able to add conversions between single- and
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:
([pts err] ...)
([pts err] ...)
Herbie's benchmark suite also uses properties such
:herbie-target for continuous integration, but these
are not officially supported and their use is discouraged.