The Input Format

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

Math format

The Herbie web shell takes input in standard math syntax. More specifically, it uses 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.

FPCore format

Herbie's command-line and batch-mode tools use FPCore format to describe mathematical expressions. FPCore looks like this:

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

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 FPCore files.

Supported functions

FPCore expressions can use any of the following functions:

+, -, *, /, 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. Use - for both subtraction and negation.

However, how Herbie evaluates these functions, their cost, and what additional functions are available depends on the platform you select.

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 operators support chained comparisons with more than two arguments; for example (< 1 x 10) means 1 < x < 10.

Intermediate variables

Intermediate variables can be defined using let and let*:

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

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

Unless you have a lot of Lisp experience, you'll probably find 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.

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 use the :spec expression to evaluate error, but use body expression as a starting-point for finding more accurate expressions.

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

Platforms can also add additional precisions.