		Search-engine friendly clone of the ACL2 documentation.

Df

Support for floating-point operations

ACL2 supports computation that uses floating-point operations. The basic arithmetic operations (+, -, *, and /) in Common Lisp can be much faster when applied to floating-point numbers than to rational numbers. Moreover, the floating-point operations include transcendental operations such as the sine function.

All floating-point computations performed by Common Lisp for ACL2 use double-floats, that is, double-precision floating-point numbers. Computation with other precisions (including single-precision) is not supported by ACL2.

Note: ACL2 novices are advised to skip this topic and program with ordinary ACL2 rationals rather than taking advantage of ACL2 support for floating-point operations. The syntactic restrictions described below are somewhat like those for single-threaded objects, known as stobjs, so although familiarity with stobjs is not assumed, that familiarity may be helpful for understanding ACL2 support for floating-point computations. (But for expressions denoting floating-point computations, unlike those involving stobjs, there is no restriction to single instances and there are no destructive operations.)

This topic is organized as follows. The Introduction may suffice for those eager to start playing with ACL2's version of floating-point operations. The second section presents challenges for supporting floating-point operations in ACL2, and the third section outlines how ACL2 addresses those challenges. A key enabler for ACL2 support of floating-point operations is how it restricts their use syntactically, and this is discussed in Section 4. Section 5 discusses guards. Section 6 documents the built-in ACL2 functions and macros that involve floating-point operations. Section 7 makes some remarks on performance. Finally, Section 8 covers more aspects of ACL2 support for floating-point operations by presenting highlights of a substantial file of relevant examples: the community-book, books/demos/floating-point-input.lsp. We conclude in Section 9 with remarks for system programmers.

This topic is written for ACL2 users. Implementation-level remarks for developers may be found in a comment in the ACL2 sources entitled “Essay on Support for Floating-point (double-float, df) Operations in ACL2”.

Section 1: Introduction

ACL2 differs from Common Lisp by imposing syntactic restrictions on expressions that represent floating-point computations, to ensure that these computations respect the ACL2 axioms. Those expressions are called df expressions, or dfs for short. ACL2 may also say that such an expression “returns a result of shape :DF”.

With those restrictions, ACL2 supports computations with double-precision floating-point numbers without adding a floating-point data type to the logic. Rather, ACL2 logically treats df expressions as returning rational numbers that are representable by floating-point numbers. For example, there is no floating-point number 1.5 in the ACL2 logic; rather, the Common Lisp value 1.5 represents the rational number 3/2, which is an ACL2 object, and the df expression (to-df 3/2) is provably equal to the constant 3/2 in the logic, even though evaluation of (to-df 3/2) in Common Lisp returns the double-float 1.5. Discussion below further explains dfs in ACL2, but for starters let's consider the following example.

(defun f1 (x)
  (declare (type double-float x))
  (df- x))

ACL2 admits this definition so that f1 is a guard-verified function. The operation df- is essentially just the negative operation (-), except that df- is to be applied only to df expressions; this is enforced based on the double-float type declaration. Let's look at what happens when we trace f1; discussion follows. In the following example, f1 is applied to the df expression (to-df 3/2); the expression (f1 3/2) would be illegal for top-level evaluation because, as noted above, f1 expects a df expression,

ACL2 !>(trace$ f1 to-df)
((F1) (TO-DF))
ACL2 !>(f1 (to-df 3/2))
1> (ACL2_*1*_ACL2::TO-DF 3/2)
<1 (ACL2_*1*_ACL2::TO-DF 3/2)
1> (ACL2_*1*_ACL2::F1 3/2)
  2> (F1 1.5)
  <2 (F1 -1.5)
<1 (ACL2_*1*_ACL2::F1 -3/2)
#d-1.5
ACL2 !>

Initially, the function to-df is applied to 3/2. The result is logically still 3/2, not 1.5, because the executable-counterpart for to-df returns an ACL2 value, not a Common Lisp value. (See evaluation for background on executable-counterparts and corresponding raw Lisp functions.) Then 3/2 is passed to the executable-counterpart for f1. The guard of f1 holds on 3/2 (we'll discuss guards later), so evaluation passes from the executable-counterpart for f1 to the raw Lisp function for f1 after converting 3/2 to a Common Lisp double-precision floating-point number, 1.5. Then df-, which is essentially just - in raw Lisp, is applied to obtain -1.5, which is returned by raw-Lisp f1. Then the executable-counterpart for f1 converts -1.5 to the corresponding ACL2 object, the rational -3/2, which is ultimately returned to the top-level loop.

Remark. The astute reader may have noticed that the executable-counterpart for to-df did not call the raw Lisp function for to-df. That is because to-df is actually a macro in raw Lisp.

Section 2: Challenges for supporting floating-point operations in ACL2

In this section we motivate ACL2 restrictions pertaining to floating-point numbers, which are addressed in the section after this one.

We start with examples that show why ACL2 cannot allow some common operations to be applied to floating-point numbers. We illustrate using computations in raw Lisp; this is relevant since, as noted above, raw-Lisp computation supports evaluation of guard-verified code.

Problem #1: Addition isn't associative on floating-point numbers.

We see that immediately with the following raw Lisp examples.

? (+ 0.1 (+ 0.2 0.3))
0.6
? (+ (+ 0.1 0.2) 0.3)
0.6000000000000001
?

Yet ACL2 has the following axiom.

Definition: associativity-of-+

(defaxiom associativity-of-+
  (equal (+ (+ x y) z) (+ x (+ y z))))

So we can't simply apply + to floating-point numbers in ACL2, because guard-verified code leads to raw Lisp computations that would violate this axiom.

Problem #2: Functions EQUAL and = are logically the same in ACL2 but not in raw Lisp.

The following succeeds.

(thm (equal (equal x y)
            (= x y)))

Yet the following log shows that raw Lisp can violate that property if we allow double-floats. (In Common Lisp, = compares numeric values while EQUAL distinguishes between rationals and floats and even between floating-point numbers 0.0 and -0.0.)

? (equal 1 1.0)
NIL
? (= 1 1.0)
T
? (equal 0.0 (- 0.0))
NIL
? (= 0.0 (- 0.0))
T
?

Section 3: How the challenges are addressed

The following three principles guide support for floating-point computations in ACL2.

(A) Treat floating-point values as rationals.
(B) Put syntactic limitations on floating-point operations.
(C) Use partial-encapsulate to axiomatize floating-point operations while supporting evaluation.

Let's look at these in turn.

(A) Treat floating-point values as rationals.

The ACL2 logic does not include floating-point numbers. Rather, certain rational numbers can be represented by double-precision floating-point numbers, known as double-floats, during computations. We can say that a double-float represents a corresponding rational number. Certain expressions denote such representable rational numbers. Those are called df expressions and we say more about them in our discussion of (B), below.

The predicate dfp recognizes those rational numbers that have a floating-point representation. We do not review floating-point numbers here, other than to note that a floating-point number is equal to a binary significand between 1 and 2 times 2 to a power, such as as 1.01100 * 2^30. For example, 1/4 is representable but 1/3 is not.

ACL2 !>(dfp 1/4) ; represented by the double-float, 0.25d0
T
ACL2 !>(dfp 1/3) ; not represented by a double-float
NIL
ACL2 !>

ACL2 provides #d notation (see sharp-d-reader) as a way to read floating-point notation as a representable rational, illustrated as follows.

ACL2 !>#d0.25
1/4
ACL2 !>#d3.5
7/2
ACL2 !>#d3.1
6980579422424269/2251799813685248
ACL2 !>:q

Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
? (= 3.1 6980579422424269/2251799813685248)
T
?

Although ACL2 simulates floating-point values with rationals, we see below how raw Lisp computation can actually use floating-point arithmetic on double-precision floating-point numbers.

(B) Put syntactic limitations on floating-point operations.

Here we briefly discuss syntactic restrictions based on the notion mentioned above of df expression, or df for short. A more complete discussion is in the section below on Syntactic Restrictions. With those restrictions, ACL2 supports computations with double-precision floating-point numbers without adding a floating-point data type to the logic. Informally, a df expression is one that computes in raw Lisp to a double-float.

Let us return to the following example. It uses df-, which is the negative operation on dfs; that is, (df- x) is analogous to (- x), but df- operates on a df and returns a df.

ACL2 !>(defun f1 (x)
         (declare (type double-float x))
         (df- x))

Since F1 is non-recursive, its admission is trivial.  We observe that
the type of F1 is described by the theorem (RATIONALP (F1 X)).  We
used the :type-prescription rule BINARY-DF+.

(F1 :DF) => :DF.

Computing the guard conjecture for F1....

The guard conjecture for F1 is trivial to prove.  F1 is compliant with
Common Lisp.

Summary
Form:  ( DEFUN F1 ...)
Rules: ((:TYPE-PRESCRIPTION BINARY-DF+))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 F1
ACL2 !>

Notice the signature shown above for f1:

(F1 :DF) => :DF

This means that the input of f1 must be a df expression and f1 returns a df expression. ACL2 determines that the input must be a df by virtue of the declaration, (type double-float x). Calls of f1 are determined to be dfs because the body of f1, (df- x), is a df. One can say that ACL2 engages in a limited form of strong typing to identify certain inputs and outputs of a function symbol as dfs. Those familiar with stobjs may notice some similarity to the syntactic restrictions on stobjs.

The following example illustrates the requirement that the input of f1 be a df.

ACL2 !>(f1 3)


ACL2 Error [Translate] in TOP-LEVEL:  The form 3 represents an ordinary
object, but it is being used where a form representing a :DF was expected.
See :DOC df.  Note:  this error occurred in the context (F1 3).

ACL2 !>

That error can be avoided by converting the input (a rational constant) to a suitable df using the primitive, to-df (discussed later).

ACL2 !>(f1 (to-df 3))
#d-3.0
ACL2 !>

Notice that the result is displayed using #d notation. But remember that there are no actual floating-point objects in ACL2; f1 returns a rational logically, namely -3. However, since the input expression is a df, ACL2 prints the evaluation result using #d notation. (This is analogous to the special printing of <state> when the ACL2 state is returned, and similarly for user-defined stobjs.) To see that the logical value returned is truly 3, note that the following event is admitted by ACL2: (thm (equal (f1 (to-df 3)) -3)).

The tracking of dfs avoids Problem #1 above, that addition isn't associative on floating-point numbers. That's because ACL2 does not allow + to be applied to a df, as illustrated by the following example, which complains that the + operation is being supplied a df, namely the call of f1. The notion “a result of shape :DF” is synonymous with “df”.

ACL2 !>(+ 5 (f1 (to-df 3)))


ACL2 Error [Translate] in TOP-LEVEL:  It is illegal to invoke F1 here
because of a signature mismatch.  This function call returns a result
of shape :DF where a result of shape * is required.  Note:  this error
occurred in the context (F1 (TO-DF 3)).

ACL2 !>

There is however an operation df+ that can be applied to :DF expressions.

ACL2 !>(df+ (to-df 5) (f1 (to-df 3)))
#d2.0
ACL2 !>

In fact df+ automatically converts its arguments satisfying dfp to be dfs, so the following is also legal since 5 is converted to (to-df 5).

ACL2 !>(df+ 5 (f1 (to-df 3)))
#d2.0
ACL2 !>

But df+ is not associative; the following fails, as it should.

(thm ; FAILS!
 (implies (and (dfp x) (dfp y) (dfp z))
          (equal (df+ (df+ x y) z)
                 (df+ x (df+ y z)))))

We return now to Problem #2, that the functions EQUAL and = are logically the same in ACL2 but not in raw Lisp, as seen by evaluation in raw Lisp, where (equal 1 1.0) evaluates to nil but (= 1 1.0) evaluates to t. This problem is avoided by our syntactic tracking of df expressions. The following example shows that equal cannot be called on a df expression.

ACL2 !>(equal 1 (to-df 1))


ACL2 Error [Translate] in TOP-LEVEL:  It is illegal to invoke TO-DF
here because of a signature mismatch.  This function call returns a
result of shape :DF where a result of shape * is required.  Note:
this error occurred in the context (TO-DF 1).

ACL2 !>

One cannot directly test equality of a non-df expression with a df expression, but one can compare equality of two df expressions, as the following example illustrates. (This example also illustrates that addition is commutative on dfs; we will return elsewhere to this point.)

ACL2 !>(df= (df+ #d1.2 #d3.4) (df+ #d3.4 #d1.2))
T
ACL2 !>

(C) Use partial-encapsulate to axiomatize floating-point operations while supporting evaluation.

Next we consider how ACL2 introduces the df primitives, that is, built-in functions and macros that take or return a df. Their calls may be executed by calling corresponding Common Lisp functions. But axiomatizing these primitives presents a challenge since the Common Lisp language doesn't quite tie down the values returned by floating-point operations. Here is a relevant quote from the Common Lisp HyperSpec about the presence of a raw Lisp “feature”, :ieee-floating-point.

If present, indicates that the implementation purports to conform to the requirements of IEEE Standard for Binary Floating-Point Arithmetic.

ACL2 checks at build time that this feature is present. However, that IEEE standard specifies results of operations with respect to a rounding mode. Probably most or all Common Lisp implementations use round to nearest even as their rounding mode, but this is not guaranteed. We work around this problem to some extent by introducing a constrained rounding function, df-round, and using it to define the rational function primitives: addition (df+), subtraction (df-), multiplication (df*), and division (df/). Transcendental functions, such as the sine function, are not as straightforward to define in terms of rounding. Although the sine function, for example, might be defined by rounding a sufficiently large Taylor approximation, transcendental functions are constrained with minimal axioms (at least for now); for example, the sine function is implemented by the constrained function, df-sin. Over time some of those constraints may be strengthened, or they may even be replaced by definitions in terms of df-round.

Even though the df primitives are constrained (except for the rational primitive functions, which are defined in terms of the constrained function df-round), ACL2 can evaluate their calls, even during proofs. This is arranged by introducing them with partial-encapsulate, which allows some of the constraints to be implicit; see partial-encapsulate. The implicit constraints are based on computation; for example, when ACL2 admits the event (thm (equal (df-sin 0) 0)), an implicit constraint guarantees (equal (df-sin 0) 0). There are also explicit constraints, which for example allow ACL2 to prove (dfp (df-sin x)). We do not explain further here, but the interested reader is welcome to examine relevant comments in the ACL2 source code, for example in the partial-encapsulate event that introduces df-round in ACL2 source file float-a.lisp.

ACL2 arranges for the host Lisp to evaluate calls of df primitives in guard-verified) and :program-mode code. For example, such evaluation of a df-sin call leads to a call of sin in Common Lisp. The following log illustrates this point and is discussed below.

ACL2 !>(defun f2 (x)
         (declare (type double-float x))
         (df-sin x))

Since F2 is non-recursive, its admission is trivial.  We observe that
the type of F2 is described by the theorem (RATIONALP (F2 X)).  We
used the :type-prescription rule RATIONALP-DF-SIN-FN.

(F2 :DF) => :DF.

Computing the guard conjecture for F2....

The guard conjecture for F2 is trivial to prove.  F2 is compliant with
Common Lisp.

Summary
Form:  ( DEFUN F2 ...)
Rules: ((:TYPE-PRESCRIPTION RATIONALP-DF-SIN-FN))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
 F2
ACL2 !>(trace$ f2)
 ((F2))
ACL2 !>(trace! (sin :native t))

TTAG NOTE: Adding ttag :TRACE! from the top level loop.
ACL2 !>(f2 (df/ (df-pi) 2))
1> (ACL2_*1*_ACL2::F2 884279719003555/562949953421312)
  2> (F2 1.5707963267948966)
    3> (SIN 1.5707963267948966)
    <3 (SIN 1.0)
  <2 (F2 1.0)
<1 (ACL2_*1*_ACL2::F2 1)
#d1.0
ACL2 !>

We see at “1>” that evaluation arranged to pass a (representable) rational number (roughly, π/2) to the executable-counterpart for f2 (again, for relevant background see evaluation). But at “2>”, where evaluation was passed to the raw Lisp function for f2, that rational value was converted to the corresponding double-float value, which raw Lisp evaluation passed to the Common Lisp function sin, at “3>”. Common Lisp then returned 1.0 for the raw Lisp applications of sin and f2, so that finally, the executable-counterpart for f2 returned the rational number, 1. That value was displayed using #d notation because a call of f2 is a df.

Since rounding (to nearest even, in particular) is not tied down by the Common Lisp language, different host Lisp implementations may give different results. This leads us to the following point of emphasis.

When a collection of books is certified (see certify-book), the same environment — in particular the Lisp implementation and operating system — should be used for all of these books, even those included during certification.

Otherwise there is a soundness issue. One might prove, say, (equal (df-sin 1) A) and (equal (df-sin 1) B) for distinct (but close by) numeric values A and B in two different books, certified with ACL2 executables built on different Lisps, and then include those two books to prove a contradiction.

Section 4: Syntactic Restrictions

We now present more details on the syntactic restrictions pertaining to df expressions (dfs). Our discussion is still informal but it should suffice for the successful use of dfs in ACL2. (Optional technical note for those familiar with ACL2 source function translate11: a df is an expression whose translation is made with stobjs-out equal to (:DF), and the arguments of a function call are those in a :DF position with respect to that function symbol's stobjs-in.)

These syntactic restrictions are not applied in theorem and non-executable contexts, in particular not within defthm, thm, and defun-nx events and not within a call of non-exec. Below we focus on restrictions for a defun event, including its body, guard, and measure; but these restrictions also apply to defmacro events, defconst events, and top-level evaluation.

Certain variables may be specified as dfs at the top level in the case of defun events but not in other cases. For a defun event, the declared dfs consist of all variables vi listed either in a declare form (type double-float v1 ... vk) or an xargs declaration :dfs (v1 ... vk). If k is 1 then one may write :dfs v1 to abbreviate :dfs (v1). These declared dfs are the known df variables at the top level of the user-supplied body, guard, and measure of f. The rules below indicate, for a set V of known df variables, when an expression is a df with respect to V; and these rules also speak to legality of certain expressions.

Before presenting those rules, we extend the notion of a df expression (again, df for short) to that of a df{i} expression (df{i} for short). Such an expression is one that returns multiple values when the ith value is to be considered a df. For example, the expression (mv (to-df x) (df- y) 17) is a df{0} expression and a df{1} expression but not a df{2} expression. Note that an expression that returns a single value might or might not be a df expression, but it is never a df{i} expression for any i; and similarly, an expression that returns multiple values maybe a df{i} expression for various i but it is never a df expression.

Here are the rules promised above. They are not complete; for example, they do not cover stobj-let expressions. But those and other cases should present no surprises in practice. Let u be a user-supplied term (that is, an untranslated term; see term).

If u is a variable, then u is a df with respect to V if and only if it is in V.
If u is a constant symbol then it is not a df (with respect to any set).
If u is a lambda expression, then u is a df with respect to V if and only if the corresponding let expression is a df with respect to V.
If u is a macro call (m t1 ... tn), then u is a df with respect to V if and only if the single-step macroexpansion of u is a df with respect to V.
Suppose u is the term (f t1 ... tn) where f is a function symbol. It is required that ti is a df with respect to V if and only if the ith formal of f is a declared df of f. An exception to that requirement is when f is dfp, in which case the only restriction on t1 is that it is not a stobj name. If f returns a single value then u is a df (respectively, df{i}) with respect to V if and only if the body of f is a df (respectively, df{i}) with respect to V.
Consider (let ((x1 e1) ... (xk ek)) dcl1 ... dclm body). The rules apply to each ei with respect to V, but for body the rules apply with respect to the following new set of known dfs. First, remove all xi from V except when xi is declared as a df in one of the dcli with a double-float type declaration. For any xi not so declared, ACL2 guesses whether or not ei is a df with respect to V. If the guess is “yes” then add xi as a known df, and if the guess is “no” then do not add it. Otherwise, the guess fails to yield an answer, in which case ACL2 can try both ways: first it attempts to treat (technically, translate) ei as a non-df and, if that fails, it treats ei as a df. (However, the guess almost always works; in particular, for a function call it just looks up the function's signature, except for a recursive call of a function being defined.)
For (mv-let (x1 ... xk) mv-expr dcl1 ... dclm body), the rules apply to mv-expr and to body, but for body the known dfs are modified as follows. ACL2 attempts to determine those i ≤ k for which mv-expr is a df{i} expression. (Optional technical note for those familiar with ACL2 source function translate11: ACL2 attempts to determine suitable stobjs-out for translation of mv-expr.) Then to obtain the known dfs for body, each xi is initially removed from V except for those declared in some dcli as having type double-float, and then those xi for which mv-expr is a df{i} expression are added back as known dfs for translation of body.

Note that ACL2 features that naturally traffic in ordinary ACL2 values may disallow uses of df expressions (much as they disallow uses of stobjs). Here are a few examples.

A table guard must return an ordinary value, not a df.
A clause-processor must return an ordinary value (and perhaps stobjs in the multiple-values case; see clause-processor).
A theory expression, as well as the argument of defconst, defpkg, syntaxp, or bind-free, must return an ordinary value, not a df.

Section 5: Guards

When a defun event defines a function, the guard for that function asserts that dfp holds for each declared df. Here's an example

(defun df-10/x (x)
  (declare (xargs :guard (not (df= 0 x))
                  :dfs x))
  (df/ 10 x))

The generated guard is (and (dfp x) (not (df= 0 x))). Note that (dfp x) precedes (not (df= 0 x)): the conjuncts generated from the :dfs always precede those that come from :guard specifications.

Instead of specifying declared dfs using :dfs xargs, a better approach (see Section 7: Remarks on performance) is to use double-float type declarations. Here's a variant of the example above that uses this approach; it too is admitted by ACL2.

(defun df-10/x (x)
  (declare (xargs :guard (not (df= 0 x)))
           (type double-float x))
  (df/ 10 x))

Technical remark (feel free to skip it). There is a subtlety here. Unlike :dfs specifications, any type declarations are conjoined with :guard specifications in the order of appearance of each. (This is a general aspect of ACL2, not specific to double-float types.) So in the example above, the guard is essentially (and (not (df= 0 x)) (dfp x)). It may be surprising that (df= 0 x) can itself be guard-verified without the assumption of (dfp x). The reason is that ACL2 figures out that x is a declared df, and deduces that since this is legal code, we know that (dfp x) is true.

Section 6: Df primitives

This section documents the df primitives, which (again) are those built-in functions and macros that take or return a df. A small number of related built-ins are also documented here. These are divided here into the following groups.

Recognizers and conversion functions
Basic arithmetic operations
Other operations

In each case, we display a function's signature (as in the example of f2 above) and describe its functionality. You can of course use :pe to see its logical definition.

But first we discuss a class of convenient macros.

Corresponding df-friendly macros

Before we document the df primitive functions, we describe corresponding macros that automatically convert certain constants to df expressions by using a to-df wrapper. We call such a macro the “corresponding df-friendly macro” for the given function. Below, we show how that works for binary-df+ and its corresponding df-friendly macro, df+. The same relationship holds for other df primitive functions and their corresponding df-friendly macros.

Consider the following examples of adding two dfs with the function binary-df+.

ACL2 !>(binary-df+ (to-df 3) (to-df 1/2))
#d3.5
ACL2 !>(let ((x (to-df 3))) (binary-df+ x (to-df 1/2)))
#d3.5
ACL2 !>

The arguments to binary-df+ must be dfs, so it is illegal to remove any call of to-df above. For example, all of the following cause errors.

(binary-df+ 3 1/2) ; 3 and 1/2 are not dfs
(let ((x (to-df 3))) (binary-df+ x 1/2)) ; 1/2 is not a df
(let ((x 3)) (binary-df+ x (to-df 1/2))) ; x is not a df

However, binary-df+ has a corresponding df-friendly macro, df+. That macro expands to a call of binary-df with a call of to-df wrapped around every constant numeric argument that satisfies dfp. The following calls show expansions of df+ calls that correspond to calls from the first two examples above.

ACL2 !>:trans1 (df+ 3 1/2)
 (BINARY-DF+ (TO-DF 3) (TO-DF 1/2))
ACL2 !>:trans1 (df+ x 1/2)
 (BINARY-DF+ X (TO-DF 1/2))
ACL2 !>

So, evaluation succeeds for those two uses of df+ in place of binary-df+.

ACL2 !>(df+ 3 1/2)
#d3.5
ACL2 !>(let ((x (to-df 3))) (df+ x 1/2))
#d3.5
ACL2 !>

The third example still fails, however, since df+ only wraps to-df around constants.

ACL2 !>(let ((x 3)) (df+ x (to-df 1/2)))


ACL2 Error [Translate] in TOP-LEVEL:  The form X represents an ordinary
object, but it is being used where a form representing a :DF was expected.
See :DOC df.  Note:  this error occurred in the context
(BINARY-DF+ X (TO-DF 1/2)).

ACL2 !>

Note that a constant value is only supplied a to-df wrapper when it satisfies dfp, that is, it is a representable rational, as illustrated by the following example.

ACL2 !>:trans1 (df+ 1/3 1/4)
 (BINARY-DF+ 1/3 (TO-DF 1/4))
ACL2 !>

The focus above has been on numeric constants, but symbolic constants that start and end with the ‘*’ character, like *c*, are treated somewhat similarly. Such an argument of a df-friendly macro is given a to-df wrapper as well as an assertion that dfp holds. Suppose for example that we submit the following two events.

(defconst *good* 1/4) ; 1/4 satisfies dfp.
(defconst *bad* 1/3)  ; 1/3 does not satisfy dfp.

Here is how those arguments are treated when supplied to a df-friendly macro.

ACL2 !>:trans1 (df+ *good* *bad*)
 (BINARY-DF+ (LET ((C *GOOD*))
               (ASSERT$ (DFP C) (TO-DF C)))
             (LET ((C *BAD*))
               (ASSERT$ (DFP C) (TO-DF C))))
ACL2 !>

Indeed, evaluation of (df+ *good* *bad*) results in an assertion failure.

HARD ACL2 ERROR in ASSERT$:  Assertion failed:
(ASSERT$ (DFP C) (TO-DF C))

But logically, assert$ returns its second argument, so ACL2 can prove the following.

(equal (df+ *good* *bad*)
       (binary-df+ *good* (to-df *bad*)))

Recognizers and conversion functions

(from-df :DF) => *
Converts a df to a numerically equivalent ordinary value.

(to-df *) => :DF
Converts an ordinary value to a nearby df. This is the identity on any rational that is representable by a floating-point number.

(to-dfp *) => *
This is logically the same as to-df, but it returns an ordinary value rather than a df.

(dfp {* or :DF}) => *
Recognizes rationals that can be represented by Lisp double-floats; so, always true when applied to a df. The logical definition of (dfp x) is (and (rationalp x) (= (to-df x) x)).

(df-round *) => *
Constrained, non-executable rounding function, which converts a rational to a nearby value that satisfies dfp. It is used in the definitions of the basic arithmetic operations.

(df-string :DF) => *
Produces the floating-point representation, as a string, of the given df value. Examples:

ACL2 !>(df-string (to-df 1/4))
"0.25"
ACL2 !>(df-string (to-df 1/3))
"0.3333333333333333"
ACL2 !>

(df-rationalize-fn :DF) => *
Calls the Common Lisp function, rationalize, which the Common Lisp HyperSpec says “returns a rational that approximates the float to the accuracy of the underlying floating-point representation.” The idea is to produce a “pretty” rational that approximates the given df, as illustrated by the following example.

ACL2 !>(from-df (to-df 1/10))
3602879701896397/36028797018963968
ACL2 !>(df-rationalize (to-df 1/10))
1/10
ACL2 !>

(rize *) => *
This is a variant of df-rationalize that operates on rationals instead of dfs, as shown by the following extension of the example just above.

ACL2 !>(rize 3602879701896397/36028797018963968)
1/10
ACL2 !>

Basic arithmetic operations

(binary-df+ :df :df) => :df
Adds the two given dfs.
Corresponding df-friendly macro: (df+ x y )

(binary-df* :df :df) => :df
Multiplies the two given dfs.
Corresponding df-friendly macro: (df* x y )

NOTE: Both df+ and df* are binary, unlike + and *. An immediate issue is that the failure of associativity could cause a divergence with the logical expansion into a right-associated sum or product, for example in raw Lisp as follows.

? (+ .1 .2 .3)
0.6000000000000001
? (+ .1 (+ .2 .3))
0.6
?

(binary-df/ :df :df) => :df
Divides the two given dfs, where the second should be non-zero.
Corresponding df-friendly macro: (df/ x y )

(unary-df- :df) => :df
Takes the negative of the given df.
Corresponding df-friendly macro: (df- x)

(unary-df/ :df) => :df
Takes the reciprocal of the given non-zero df.
Corresponding df-friendly macro: (df/ x)

Also provided is a binary version of the macro df-. The expansion of (df- term1 term2) is essentially (df+ term1 (df- term2)).

These functions are all defined by applying df-round to the exact mathematical result. Here are their definitions in the ACL2 logic.

Function: binary-df+

(defun binary-df+ (x y)
  (declare (xargs :guard (and (dfp x) (dfp y))))
  (df-round (+ x y)))

Function: binary-df*

(defun binary-df* (x y)
  (declare (xargs :guard (and (dfp x) (dfp y))))
  (df-round (* x y)))

Function: binary-df/

(defun binary-df/ (x y)
  (declare (xargs :guard (and (dfp x) (dfp y) (not (= y 0)))))
  (df-round (/ x y)))

Function: unary-df-

(defun unary-df- (x)
  (declare (xargs :guard (dfp x)))
  (df-round (- x)))

Function: unary-df/

(defun unary-df/ (x)
  (declare (xargs :guard (and (dfp x) (not (= x 0)))))
  (df-round (/ x)))

We include the following as a basic arithmetic operation (though some may argue with that classification).

(df-abs-fn :df) => :df
Return the absolute value of the df input, as a df.
Corresponding df-friendly macro: (df-abs x)

Other operations

These are listed alphabetically. They include the square root function and common transcendental functions. The first two are logarithm functions.

(binary-df-log :df :df) => :df
Takes the log, where the first argument is the base.
Corresponding df-friendly macro: (df-log x y)

(unary-df-log :df) => :df
Takes the natural log (log base e) of the given df.
Corresponding df-friendly macro: (df-log x)

The following zero-ary functions return floating-point constants.

(df-pi) => :df
Returns a df approximation to π.
The constant *df-pi* is defined to be the corresponding rational:
(defconst *df-pi* (from-df (df-pi))).

(df0) => :df
Returns a df logically equal to 0.

(df1) => :df
Returns a df logically equal to 1.

(df-minus-1) => :df
Returns a df logically equal to -1.

The remaining functions are listed in alphabetic order. Each has a name of the form df-NAME-fn where NAME is the name of a corresponding Common Lisp function. Each takes a df argument except for expt, which takes two df arguments, and each returns a df argument. The guards require not only dfp of each argument but the extra conditions as shown below. Each has a corresponding df-friendly macro, df-NAME.

(df-acos-fn x) ; guard extra: (df<= (df-abs-fn x) 1)

(df-acosh-fn x)

(df-asin-fn x)

(df-asinh-fn x)

(df-atan-fn x)

(df-atanh-fn x) ; guard extra: (df< (df-abs x) 1)

(df-cos-fn x)

(df-cosh-fn x)

(df-exp-fn x)

(df-expt-fn x y) ; guard extra: (or (df< 0 x) (and (df= 0 x) (df< 0 y)))

(df-sin-fn x)

(df-sinh-fn x)

(df-sqrt-fn x) ; guard extra: (df<= 0 x)

(df-tan-fn x) ; guard extra: (not (df= (df-cos-fn x) 0))

(df-tanh-fn x) ; guard extra: (not (df= (df-cosh-fn x) 0))

Section 7: Remarks on performance

This section covers just a few aspects of performance pertaining to the use of dfs. Those who use dfs and can provide useful performance tips are welcomed to extend this section.

Inlining of df primitives

Suppose we start ACL2 and then submit the following forms, which define g1 in raw Lisp and provide its assembly code.

(defun g1 (x y) (declare (type double-float x y)) (df< x y))
(disassemble 'g1)

If we repeat this experiment in a new ACL2 session except that we replace df< with <, we get the same assembly code (at least, when using ACL2 built on CCL or on SBCL as of this writing). This is good; it shows that there is no performance penalty for using df<. To understand why, first observe that macroexpansion replaces df< by df<-fn; then observe that the ACL2 sources include a declaim form that declares df<-fn to be inline. All the df primitive functions are similarly declared inline except for to-df, which we discuss next. Of course, these inlined raw Lisp functions (and macro) cannot generally be traced.

To-df is a macro in raw Lisp

Although to-df is a function in the ACL2 logic, it is implemented as a macro in raw Lisp. To see how that benefits performance, consider the following definition.

(defun add3 (x) (declare (type double-float x)) (df+ 3 x))

We can see the translation of that df+ call as follows.

ACL2 !>(body 'add3 nil (w state))
(BINARY-DF+ (TO-DF '3) X)
ACL2 !>

Since binary-df+ is inlined in raw Lisp (see above), its call above essentially equivalent in raw lisp to (+ (TO-DF '3) X). But it would be unfortunate to call to-df at runtime, even if to-df were an inlined function.

However, to-df is a macro that expands away its call on a rational argument or quoted rational argument.

? (macroexpand-1 '(TO-DF '3))
3.0
T
?

A key performance tip is that a defun form should declare dfs with a type declaration rather than an xargs :dfs declaration. Here are examples.

Type declarations are probably preferred

This observation is not really specific to the use of dfs. Common Lisp compilers can sometimes take advantage of type declarations, but they never take advantage of xargs declarations (because those are ignored by the compiler). So just as one may get better performance with a declaration (type (integer 0 *) x) than with (xargs :guard (natp x)), one may get better performance with (declare (type double-float x)) than with (xargs :dfs x).

Section 8: More examples

This section, which forms the remainder of this topic, is a synopsis of community-books file books/demos/floating-point-input.lsp. It may be useful to skip this section and instead read that file; or one could consult that file when an example given below needs more explanation, since other examples in that file may be clarifying. Comments in that file may suffice to explain what is going on, but if not, then corresponding output file books/demos/floating-point-log.txt (generated by the run-script utility) may be worth a look.

Here are the contents of that file (quoting from a comment near its top).

;;; TABLE OF CONTENTS
;;; -----------------
;;; "Floats" as rationals
;;; Overflow and underflow
;;; An assertion macro
;;; Df-rationalize and rize
;;; More on dfp & to-df (recognizer & generator for representables)
;;; Fun with pi
;;; No support for complex floats
;;; Examples with defined functions
;;; Examples focused on ec-call
;;; We can't prove much
;;; Df stobj fields
;;; Arrays of double-floats
;;; DO loop$ expressions
;;; FOR loop$ expressions
;;; Stobj-let (nested stobjs)
;;; Using apply$ with dfs, including efficiency issues
;;; Encapsulate and signatures
;;; Memoization
;;; Miscellany
;;; Check consistency with values produced in raw Lisp

We now hit some highlights of each of those sections that may not have been adequately covered above. See books/demos/floating-point-input.lsp for more details, e.g., the use of either E or D as an exponent marker.

;;; "Floats" as rationals

(assert-event
; 31/10 is not representable, but every #d number that is read without
; error is representable -- hence the equality below is false.
 (not (equal #d3.1 31/10)))

(assert-event (equal #d1d50 #d1.0E50)) ; Both are the same rational.

; The following are not quite equal because the latter is not representable.
(assert-event (not (equal #d1d50 (expt 10 50))))

(assert-event
 (let ((x (to-df #d.1))
       (y (to-df #d.2))
       (z (to-df #d.3)))
   (not (df= (df+ (df+ x y) z)
             (df+ x (df+ y z))))))

;;; Overflow and underflow

#d1E310 ; Lisp error (overflow)

#d1E-500 ; 0 (underflow)
(to-df #d1E-500) ; #d0.0 (underflow)

;;; An assertion macro

This section just defines a macro, a-e, which checks that its input is true in two ways: by direct evaluation and by proof.

;;; Df-rationalize and rize

(thm (equal (to-df 1/3) ; Rational representation is on next line.
            6004799503160661/18014398509481984))

(df-rationalize
 (to-df 1/3)) ; result is 1/3

(rize 1/3) ; 1/3; equivalent to (df-rationalize (to-df 1/3)) above

;;; More on dfp & to-df (recognizer & generator for representables)

(a-e (equal (dfp 1/4) t)) ; 1/4 is representable
(a-e (equal (dfp 1/3) nil)) ; 1/3 is not representable
(a-e ; to-df maps a rational to one that's representable
 (equal (dfp (to-df 1/3)) t))
(thm (equal (to-df 'abc) 0)) ; default guard-violating behavior

;;; Fun with pi

(defconst *2pi*
; See also df-2pi.  This is a rational approximation to 2*pi.  Note
; that *df-pi* is already defined as a rational approximation to pi.
; Both *df-pi* and *2pi* are ordinary objects, not dfs; defconst
; always creates an ordinary object.
  (* 2 *df-pi*))

; Signature shows return of :DF in the following.
(defun-inline df-2pi ()
; See also *2pi*.  Here, however, we return a :df (which is a
; double-float in raw Lisp) rather than an ordinary object.  Note that
; since (df-pi) is representable, multiplying it by 2 produces a
; representable rational as well (since that multiplication keeps the
; mantissa and simply doubles the small exponent).
  (df* 2 (df-pi)))

(a-e
; This holds since *df-pi* = (df-pi) and (df-2pi) is just the exact
; product by 2 of (df-pi), as noted above.
 (equal *2pi* (from-df (df-2pi))))

(df-sin (df-2pi)) ; very near 0, but not 0 (floating-point sin is not exact)

;;; No support for complex floats

(to-df #c(0 1)) ; guard violation (expects a rational)

;;; Examples with defined functions

This section of books/demos/floating-point-input.lsp has several examples that are worth reading if you have difficulties defining functions that traffic in dfs. In particular, it shows how to use THE (see the) with a double-float type-spec to assist ACL2 with its syntax checking.

;;; Examples focused on ec-call

The example below shows the need to add a :dfs argument to ec-call when the call returns a df. See this section in books/demos/floating-point-input.lsp for additional discussion and examples.

(defun f6 (x)
  (declare (xargs :guard (rationalp x)))
  (ec-call (unary-df- (to-df x))
           :dfs-in '(t)
           :dfs-out '(t)))

;;; We can't prove much

This section of books/demos/floating-point-input.lsp gives some examples of what can be proved about df operations and what cannot be proved.

;;; Df stobj fields

(defstobj st1
  (accum :type double-float :initially 0))

(assert-event (df= (accum st1) 0))

(update-accum (to-df 3) st1)

(assert-event (df= (accum st1) 3))

;;; Arrays of double-floats

(defstobj st3
; Here is an array of double-floats.  The implementation will, as
; usual, take into account the array element type (here, double-float)
; when reading or writing the array, by generating suitable type
; declarations.
; NOTE: It may be that code runs faster (but using more space) if the raw Lisp
; array is declared to have elements of type t instead of type double-float.
; Such a change might be considered in the future.
  (ar :type (array double-float (8)) :initially 0))

(defun load-ar (i max lst st3)
; Update the ar field of st3 with the values in lst, starting at position i.
  [[.. elided here; see books/demos/floating-point-input.lsp ..]])

(load-ar 0 8 (list 3 0 *df-pi* 3/4 -2/3 5 -6 7) st3)

(assert-event (and (= (from-df (ari 2 st3)) *df-pi*)
                   (= (from-df (ari 6 st3)) -6)
                   (df= (ari 6 st3) -6)
                   (df< (ari 0 st3) 5)))

(defthm dfp-nth-arp
; a useful lemma
  (implies (and (arp ar)
                (natp i)
                (< i (len ar)))
           (dfp (nth i ar))))

; We can read dfs and update with dfs.
(defun scalar-multiply-ar (i mult st3)
  (declare (xargs :stobjs st3
                  :guard (and (natp i) (<= i 8)))
           (type double-float mult))
  (cond ((zp i) st3)
        (t (let* ((i (1- i))
                  (old (ari i st3))
                  (st3 (update-ari i (df* mult old) st3)))
             (declare (type double-float old))
             (scalar-multiply-ar i mult st3)))))

(defun scalar-multiply-ar-example (st3)
   (declare (xargs :stobjs st3))
   (scalar-multiply-ar 4 (to-df 4) st3))

(load-ar 0 8 (list 3 0 *df-pi* 3/4 -2/3 5 -6 7) st3)

(scalar-multiply-ar-example st3)

(assert-event (and (= (from-df (ari 2 st3)) (* 4 *df-pi*))
                   (= (from-df (ari 6 st3)) -6)
                   (df= (ari 6 st3) -6)
                   (df< (ari 0 st3) 20)))

;;; DO loop$ expressions

This section of books/demos/floating-point-input.lsp continues using the stobj from the preceding section to show how DO loop$ expressions can operate on a stobj array.

;;; FOR loop$ expressions

; The following is illegal, because it is illegal to use a df variable (in this
; case, w) in a FOR loop$ expression.  Use DO loop$ expressions instead in such
; cases, as illustrated in the preceding section.
(let ((w (to-df 7)))
  (loop$ for v from 1 to 3
         sum (from-df (df+ w (to-df v)))))

;;; Stobj-let (nested stobjs)

This section of books/demos/floating-point-input.lsp shows that the stobj-let utility works properly with dfs.

;;; Using apply$ with dfs

; We see in examples below that apply$ works with df arguments.  This may seem
; surprising.  After all, there is a similar prohibition on stobj arguments
; because a stobj cannot be put into a list; wouldn't such a prohibition
; similarly pertain to df arguments, since they too cannot be put into a list?

; However, ACL2 evaluation of apply$ calls takes place by calling *1*
; functions, and these tolerate ordinary rational inputs where dfs are
; expected.  So apply$ accepts rational arguments where dfs are expected,
; provided they satisfy dfp.

(defun f0 (x)
  (declare (xargs :verify-guards nil)
           (type double-float x))
  (df- x))

; This too is redundant (already included above).
(include-book "projects/apply/top" :dir :system)

; "Teach" apply$ about f0:
(defwarrant f0)

; Succeeds, since 1/4 satisfies the guard for f0, (dfp x).
(assert-event (equal (apply$ 'f0 (list 1/4))
                     -1/4))

; Same as above, since the #d quantities are just rationals:
(assert-event (equal (apply$ 'f0 (list #d0.25))
                     #d-0.25))

; Error: guard violation, since (dfp 1/3) is false.
(apply$ 'f0 (list 1/3))

;;; Efficiency issues when using apply$ with dfs</i></p>
[[.. Examples omitted here; see books/demos/floating-point-input.lsp. ..]]

;;; Encapsulate and signatures

(encapsulate
  (((f16 *) => :df :formals (x) :guard (rationalp x)))
  (local (defun f16 (x)
           (declare (ignore x))
           (to-df 0))))

(defstub f19 (:df) => (mv :df :df))

;;; Memoization

; Memoization works fine with dfs; the subtleties when memoizing with stobjs
; don't apply to dfs.

;;; Miscellany

; The following defun-sk is accepted, even though y represents an ordinary
; object, because by default the defun-sk function is non-executable.
(defun-sk f25 (x)
  (declare (xargs :dfs (x)))
  (exists (y) (df< x y)))

;;; Memoize-partial works fine with dfs.

;;; Check consistency with values produced in raw Lisp

; This section has tests to check that ACL2 evaluation with dfs agrees with
; corresponding Common Lisp evaluation on double-floats.

Section 9: Remarks for system programmers

Probably most ACL2 users should skip this section. But those who use ACL2 system utilities (see for example system-utilities and programming-with-state) may find some remarks here to be useful.

The functions translate, translate1, translate-cmp, and translate1-cmp all convert a user-level term to a translated term. Each of these assumes that no free variable of the user-level term is a df. The function translate1-cmp+ has an extra argument, known-dfs, that is a list of free variables that are to be considered to be dfs.

Subtopics

Fp: Floating-point and ACL2