The Input Format

Herbie's input format is designed for expressing mathematical functions, which Herbie can then search for accurate implementations of. It also allows specifying the distribution that Herbie draws inputs from when evaluating the accuracy of an expression.

General format

The general format of an input expression is:

(herbie-test (inputs ...) "title" expression)

Each input is a variable, like x, or a variable and a distribution, written [x distribution]. The title is any text that describes the expression and the input is the expression to improve the accuracy of.

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

(herbie-test (a b) "hypotenuse" (sqrt (+ (sqr a) (sqr b))))

Supported functions

The full list of supported functions and is as follows:

+, -, *, /, abs
The usual arithmetic functions
- is both negation and subtraction
sqr, sqrt
Squares and square roots
exp, log
Natural exponent and natural log
Exponentiation; raising a value to a power
sin, cos, tan, cotan
The trigonometric functions
asin, acos, atan, atan2
The inverse trigonometric functions
atan2 is the two-argument inverse tangent
sinh, cosh, tanh
The hyperbolic trigonometric functions
expm1, log1p, hypot
Specialized numeric functions, as in math.h

Herbie allows the +, -, *, and / functions to be passed more than two arguments, and all of these functions are taken as left-associative.

Herbie allows conditional expressions using if: (if cond a b) evaluates the conditional cond and returns either a if it is true or b if it is not. Conditionals may use:

=, <, >, <=, >=
The usual comparison operators
and, or, not
The usual logical operators

Intermediate variables can be defined using let*:

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

Each variable is bound to the associated value, in order, with later values allowed to reference prior values. All the defined values are bound in the body. Note that Herbie treats these intermediate values only as a notational convenience, and inlines their values before improving the formula's accuracy.

Herbie also supports the constants PI and E.


Herbie allows each variable to specify the distribution it is drawn from. These distributions can be:

Interpret a random bit pattern as a float
(uniform a b)
A uniform real value between a and b
Both bounds must be numeric constants
Samples a random 32-bit signed integer
Always bind the variable to a constant

Each of these distributions can also be modified:

(< a dist b)
Only values between a and b from dist
Both bounds are optional numeric constants.