Support for floating-point operations

ACL2 supports computation that uses floating-point operations. The
basic arithmetic operations (

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,

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

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

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

ACL2 admits this definition so that

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 *executable-counterpart* for

Remark. The astute reader may have noticed that the executable-counterpart
for

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: **

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

So we can't simply apply

**Problem #2**: Functions

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,

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

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

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

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

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 :DF) => :DF

This means that the input of

The following example illustrates the requirement that the input of

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,

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

Notice that the result is displayed using

The tracking of dfs avoids Problem #1 above, that addition isn't
associative on floating-point numbers. That's because ACL2 does not allow

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

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

In fact

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

But

(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

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”,

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 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,

Even though the df primitives are constrained (except for the rational
primitive functions, which are defined in terms of the constrained function
`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

ACL2 arranges for the host Lisp to evaluate calls of df primitives in guard-verified) and

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 “

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 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,

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

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
*declared dfs* consist of all variables `declare` form `xargs`
declaration *known df variables* at the top level of the user-supplied body, guard,
and measure of

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

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 *untranslated* term; see term).

- If
u is a variable, thenu is a df with respect toV if and only if it is inV . - If
u is a constant symbol then it is not a df (with respect to any set). - If
u is a`lambda`expression, thenu is a df with respect toV if and only if the corresponding`let`expression is a df with respect toV . - If
u is a macro call(m t1 ... tn) , thenu is a df with respect toV if and only if the single-step macroexpansion ofu is a df with respect toV . - Suppose
u is the term(f t1 ... tn) wheref is a function symbol. It is required thatti is a df with respect toV if and only if thei th formal off is a declared df off . An exception to that requirement is whenf isdfp , in which case the only restriction ont1 is that it is not a stobj name. Iff returns a single value thenu is a df (respectively, df{i}) with respect toV if and only if the body off is a df (respectively, df{i}) with respect toV . - Consider
(let ((x1 e1) ... (xk ek)) dcl1 ... dclm body) . The rules apply to eachei with respect toV , but forbody the rules apply with respect to the following new set of known dfs. First, remove allxi fromV except whenxi is declared as a df in one of thedcli with adouble-float type declaration. For anyxi not so declared, ACL2 guesses whether or notei is a df with respect toV . If the guess is “yes” then addxi 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 treatsei 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 tomv-expr and tobody , but forbody the known dfs are modified as follows. ACL2 attempts to determine those i ≤ k for whichmv-expr is a df{i} expression. (Optional technical note for those familiar with ACL2 source functiontranslate11 : ACL2 attempts to determine suitable stobjs-out for translation ofmv-expr .) Then to obtain the known dfs forbody , eachxi is initially removed fromV except for those declared in somedcli as having typedouble-float , and then thosexi for whichmv-expr is a df{i} expression are added back as known dfs for translation ofbody .

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.

When a `defun` event defines a function, the guard for that
function asserts that

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

The generated guard is

Instead of specifying declared dfs using `xargs`, a better
approach (see Section 7: Remarks on performance) is to use `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

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
`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

Consider the following examples of adding two dfs with the function

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+ 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,

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

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

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

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 ‘

(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

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__

Converts a df to a numerically equivalent ordinary value.

Converts an ordinary value to a nearby df. This is the identity on any
rational that is representable by a floating-point number.

This is logically the same as

Recognizes rationals that can be represented by Lisp double-floats; so, always
true when applied to a df. The logical definition of

Constrained, non-executable rounding function, which converts a rational to a
nearby value that satisfies

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 !>

Calls the Common Lisp function,

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

This is a variant of

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

__Basic arithmetic operations__

Adds the two given dfs.

Corresponding df-friendly macro:

Multiplies the two given dfs.

Corresponding df-friendly macro:

NOTE: Both

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

Divides the two given dfs, where the second should be non-zero.

Corresponding df-friendly macro:

Takes the negative of the given df.

Corresponding df-friendly macro:

Takes the reciprocal of the given non-zero df.

Corresponding df-friendly macro:

Also provided is a binary version of the macro

These functions are all defined by applying

**Function: **

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

**Function: **

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

**Function: **

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

**Function: **

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

**Function: **

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

Return the absolute value of the df input, as a df.

Corresponding df-friendly macro:

__Other operations__

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

Takes the log, where the first argument is the base.

Corresponding df-friendly macro:

Takes the natural log (log base

Corresponding df-friendly macro:

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

Returns a df approximation to π.

The constant

Returns a df logically equal to 0.

Returns a df logically equal to 1.

Returns a df logically equal to -1.

The remaining functions are listed in alphabetic order. Each has a name of
the form

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 the submit the following forms, which defines

(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

`To-df`__ is a macro in raw Lisp__

Although

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

We can see the translation of that

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

Since

However,

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

A key performance tip is that a

__Type declarations are probably preferred__

This observation is not really specific to the use of dfs. Common Lisp
compilers can sometimes take advantage of

This section, which forms the remainder of this topic, is a synopsis of
community-books file

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

*;;; "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 useTHE (see the) with adouble-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 toec-callwhen the call returns a df. See this section inbooks/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 howDO 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 thestobj-letutility 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.

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

- Fp
- Floating-point and ACL2