1 Real Computation🔗ℹ

Rival’s main use case is to evaluate real-number expressions to correctly-rounded floating-point outputs. To do so, you first compile your real-number expression to a "rival machine", and then apply that machine to specific inputs.

1.1 Supported Real-Number Operation🔗ℹ

Rival supports a simple language of real-number expressions containing variables, rational literals, common mathematical functions, and common mathematical constants:

Expressions largely follow the semantics of math.h, not Racket, when it comes to, for example, the order of arguments to atan2 or the naming of the exponential function.

Some inputs are invalid to some operations, such as division by zero, square roots of negative numbers, and similar. For pow, Rival considers (pow 0 x) valid for non-negative x, and (pow x y) invalid for negative x and non-integer y. In general these conventions again follow those in math.h. Colloquially we say that these expressions "throw" on invalid points, though note that internally Rival uses error intervals to soundly track whether an input is invalid or not.

Expressions that mix boolean and real-number operations must type-check in the expected way, and variables must have consistent types. Rival does not perform typechecking; that is a user responsibility, and Rival may return undefined results if passed ill-typed formulas.

The assert and error operators need additional explanation; these control the definition of a "valid" input to an expression. The assert function takes in a boolean input and returns a boolean output. If the input is false, assert throws. Its output is always true. error? has the opposite behavior. This function never throws, and instead returns true if its argument throws and false if it doesn’t.

assert and error can be used to model constructs like preconditions, tests, try/catch blocks, and others.

1.2 Compiling Real Expressions🔗ℹ

To define the floating-point format that Rival is supposed to compute the output in, you provide a "discretization".

A distance of 0 indicates that the two values are equal. A distance of 2 or greater indicates that the two values are far apart. A value of exactly 1 indicates that the two values share a rounding boundary; this triggers special behavior inside Rival to handle double-rounding issues.

Note that (the absolute value of) flonums-between? already returns values that fit these requirements.

Once you have defined an appropriate discretization, you can compile your real expression using rival-compile.

Internally, rival-compile converts the exprs into a simple register machine. rival-compile is fairly slow, so the ideal use case for Rival is to compile a function once and then apply it to multiple points.

If more than one expression is provided as an input to rival-compile, common subexpressions will be identified and eliminated during compilation. This makes Rival ideal for evaluting large families of related expressions, a feature that is heavily used in Herbie. Note that each expression can use a different discretization.

1.3 Evaluating Real Expressions🔗ℹ

Once a real expression has been compiled to a rival-machine?, it can be evaluated at specific input points using rival-apply.

If the point is an invalid input to at least one of the exprs passed to rival-compile, rival-apply raises exn:rival:invalid. If Rival is unable to evaluate at least one of the exprs on the point, rival-apply raises exn:rival:unsamplable.

struct (struct exn:rival exn:fail ())

struct (struct exn:rival:invalid exn:fail (pt))   pt : (vectorof (or/c bigfloat? boolean?))

struct (struct exn:rival:unsamplable exn:fail (pt))   pt : (vectorof (or/c bigfloat? boolean?))

Note that rival-apply will only return a result if it can prove that it has correctly-rounded the output, and it will only throw an exn:rival:invalid exception if it can prove that at least one of the output expressions in the machine throws on the given input. In all other cases

Internally, rival-apply executes the register machine stored in machine repeatedly, at ever-higher bf-precision, until the output intervals are narrow enough that both endpoints convert to outputs distance 0 apart in the requested discretization. The precision is chosen through a fairly-sophisticated process that can execute different operations in different precisions to maximize performance. Caching avoids re-executing instructions whose precision needs haven’t changed. Detailed execution information can be found via racket-profile.

parameter (*rival-max-precision*) → natural? (*rival-max-precision* precision) → void?   precision : natural?  =  10000

parameter (*rival-max-iterations*) → natural? (*rival-max-iterations* iterations) → void?   iterations : natural?  =  5

Sets the maximum precision used by Rival internally and the maximum iterations performed by Rival before raising the exn:rival:unsamplable error. Note that Rival will stop at whichever of *rival-max-precision* or *rival-max-iterations* is hit first. For example, Rival may execute the maximum number of iterations before reaching the maximum precision, or choose to use a precision over the maximum before reaching the maximum number of iterations. The default values are likely sufficient for most use cases.

In other words, if ival-false is returned, there is no point calling rival-apply with any point in the input-range. If ival-maybe is returned, some points in the input-range may raise errors, while others may not, though nothing is guaranteed. If ival-true is returned, an exn:rival:invalid will not be raised for any point in the input-range. However, a exn:rival:unsamplable may still be raised.

The advantage of rival-analyze over rival-apply is that it applies to whole ranges of input points and is much faster.