The Input Format

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

General format

FPCore format looks like this:

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

(FPCore name (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.

Supported functions

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.

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 implement chained comparisons with more than two arguments.

Intermediate variables

Intermediate variables can be defined using let and let*:

(let ([variable value] ...) 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.

Preconditions

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.

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.

Conversions

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.

For example, to let Herbie introduce single-precision code when :precision is set to binary64 or vice versa, specify :herbie-conversions ((binary64 binary32))

Specifications

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.

Miscellaneous Properties

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 error 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.