Floating-point Support in ACL2
Matt Kaufmann, 11/14/2023
In collaboration with J Moore

------------------------------

**Notes**

This work isn't part of ACL2 yet.

- Awaiting release approval for work done after
  October 5 (not the subject of this talk)
- Some details remain to be worked out.

------------------------------

Outline:

MOTIVATION (but is it needed?)
TWO BIG PROBLEMS
THE SOLUTION IN A NUTSHELL (3 key aspects)
MORE EXAMPLES

------------------------------

MOTIVATION (but is it needed?):

Floating-point computations are widely used.

They are much faster than computations with rationals.

------------------------------

TWO BIG PROBLEMS
(illustrated with CCL logs):

Note: we'll deal entirely with double-precision
floating-point numbers.  ACL2 executes the following in
Common Lisp.

(setq *read-default-float-format* 'double-float)

.....

Problem #1: Addition isn't associative.

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

Yet ACL2 has the following.

ACL2 !>:pe Associativity-of-+
       -8212  (DEFAXIOM ASSOCIATIVITY-OF-+
                (EQUAL (+ (+ X Y) Z) (+ X (+ Y Z))))
ACL2 !>

We can't just run + on floating-point numbers in ACL2!

.....

Problem #2:

EQUAL and = are logically the same in ACL2;
the following succeeds:

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

Yet raw Lisp can violate that property if we allow
double-floats:

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

------------------------------

THE SOLUTION IN A NUTSHELL (3 key aspects):

(A) Treat floating-point values as rationals.

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

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

..........

(A) Treat floating-point values as rationals.

- So, no new data type.  The ACL2 logic's notion of a
  floating-point number is representable rational:

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

- The new #d reader reads in floating-point notation as
  a representable rational.

  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
  ? 

- Raw Lisp computations will use floating-point
  arithmetic on double-float objects; see below.

..........

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

- Example:

  (DEFUN F1 (X)
    (DECLARE (TYPE DOUBLE-FLOAT X))
    (DF- X))

  has signature:
  (F1 :DF) => :DF

- Avoids Problem #1,
    associativity of +,
  since + must not be applied to :DF values (there is a
  df+ operation for that).

- Avoids Problem #2,
    EQUAL vs. =,
  since these are only applied to ordinary objects;
  it's df= that's to be applied to :DF values.

..........

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

- See :DOC partial-encapsulate.

- Example 1:

  - DF-SIN is explicitly constrained to return a DFP.

  - We want implicit constraints such as
    (DF-SIN 0) = 0
    -- justified by (= (sin 0.0) 0.0) in Common Lisp.

  - So, the implicit constraints are equalities
    (DF-SIN r1) = r2
    where
    r1 is represented by double-float f1,
    r2 is represented by double-float f2,
    and in the host Common Lisp,
    (sin f1) computes to f2.

  - Signature:
    (TO-DF :DF) => :DF

- Example 2:

  - TO-DF converts any rational to nearby :DF.

  - Signature:
    (TO-DF *) => :DF

  - For example:

    ACL2 !>(to-df 1/3) ; 1/3 does not satisfy dfp
    #d0.3333333333333333
    ACL2 !>#d0.3333333333333333
    6004799503160661/18014398509481984
    ACL2 !>

------------------------------

MORE EXAMPLES

..........

Example with sin(pi/6):

ACL2 !>(df-sin (df/ (df-pi) 6)) ; 6 is (to-df 6)
#d0.49999999999999994
ACL2 !>(df- 1/2 ; (to-df 1/2)
            (df-sin (df/ (df-pi) 6)))
#d5.551115123125783E-17
ACL2 !>

..........

Computation with df operations can take place during
proofs (thanks to the use of partial-encapsulate).

; Succeeds:
(thm (equal (df-sin 0)
            (df+ -3 3)))

..........

Recall that associativity fails:

ACL2 !>(df= (df+ #d.1 (df+ #d.2 #d.3))
            (df+ (df+ #d.1 #d.2) #d.3))
NIL
ACL2 !>

Thus we're glad that the proof fails for the following
event.

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

..........

Definitions and stobjs:

(defstobj st
  (ar :type (array double-float (8)) :initially 0))

(defun load-ar (i max lst st)
  (declare (xargs :stobjs st
                  :guard (and (rational-listp lst)
                              (natp i)
                              (= (+ i (length lst)) (ar-length st))
                              (integerp max)
                              (<= i max)
                              (<= max (ar-length st)))
                  :measure (nfix (- (ar-length st) i))))
  (if (mbt (and (natp i) (integerp max) (<= i max)
                (<= max (ar-length st))
                (rational-listp lst)))
      (if (< i max)
          (let ((st (update-ari i (to-df (car lst)) st)))
            (load-ar (1+ i) max (cdr lst) st))
        st)
    st))

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

(assert-event (df= (ari 2 st) *pi*))

..........