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

pow

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.

Distributions

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

default

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

int

Samples a random 32-bit signed integer

n

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.