The Input Format

Herbie uses the FPCore input format to specify mathematical expressions, which Herbie searches for accurate implementations of.

General format

FPCore format looks like this:

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

Each input is a variable, like x, which can be used in the expression, whose accuracy Herbie will try to improve. Properties are described below.

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))))

We recommend the .fpcore file extension for Herbie input files.

Supported functions

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

+, -, *, /, fabs

The usual arithmetic functions
(where - is both negation and subtraction)

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.

Herbie links against libm to ensure that every function has the same behavior in Herbie as in your code. However, on Windows platforms some functions are not available in the system libm. In these cases Herbie will use a fallback implementation and print a warning; turning off the the precision:fallback option disables those functions instead.

Conditionals

FPCore uses if for conditional expressions:

(if cond if-true if-false)

The conditional cond may use:

==, !=, <, >, <=, >=

The usual comparison operators

and, or, not

The usual logical operators

TRUE, FALSE

The two boolean values

The comparison functions can take any number of arguments and implement chained comparisons.

Intermediate variables

Intermediate variables can be defined using let:

(let ([variable value] ...) body)

In a let expression, all the values are evaluated first, and then are bound to their variables in the body. This means that the value of one variable can't refer to another variable in the same let block; nest let constructs if you want to do that.

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.

Preconditions

By default, the arguments to formulas are assumed to be arbitrary floating-point numbers. However, in many cases only a range of argument values are possible. In Herbie, you can describe valid arguments with the :pre property (for “precondition”).

Preconditions comparison and boolean operators, just like conditional statements. Herbie is particularly efficient when when the precondition is an and of ranges for each variable, such as:

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

More complex preconditions do work, but may cause the “Cannot sample enough valid points” error if it is too hard to find points that satisfy the precondition.

Precisions

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

By default, binary64 is assumed. Herbie also has a plugin system to load additional precisions.

Complex Numbers^β

Herbie includes experimental support for complex numbers; however, this support is currently limited to a few basic operations.

All input parameters to an FPCore are real numbers; complex numbers must be constructed with complex. The functions re, im, and conj are available on complex numbers, along with the arithmetic operators, exp, log, pow, and sqrt. Complex and real operations use the same syntax, but cannot be mixed: (+ (complex 1 2) 1) is not valid. Herbie reports type errors in such situations.

Complex operations use the Racket implementation, so results may differ (slightly) from complex numbers in some other language, especially for non-finite complex numbers. Unfortunately, complex number arithmetic is not as standardized as float-point arithmetic.

In the future, we hope to support complex-number arguments and fully support all complex-number operations.

Miscellaneous Properties

Herbie uses the :name property to name FPCores in its UI. Its value ought to be a string.

Herbie's out uses custom FPCore properties to provide additional information about the Herbie improvement process:

: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 computed average error of the input program, evaluated on pts points. Multiple entries correspond to multiple training or test sets.

:herbie-error-output
([pts err] ...)

The computed average error of the output program, like above.

Herbie's passes through :name, :pre, and :precision properties to its outputs.

The benchmark suite uses other properties (such as :herbie-target) for testing, but these are not supported and their use is discouraged.