		Search-engine friendly clone of the ACL2 documentation.

Finite-difference

This transformation performs finite-differencing, aka incrementalization.

Usage

(finite-difference fn
                   term-to-replace
                   rules
                   [:skip-termination bool]     ;; Default: nil
                   [:verify-guards t/nil/auto]  ;; Default: :auto
                   [:guard-hints hints/:auto]   ;; Default: :auto
                   [:new-param-name name]       ;; Default: nil
                   [:expand-lets bool]          ;; Default: t
                   [:extra-rules rules]         ;; Default: nil
                   [:theorem-name name]         ;; Default: nil
                   [:build-wrapper bool]        ;; Default: t
                   [:theorem-disabled bool]     ;; Default: nil
                   [:function-disabled bool]    ;; Default: nil
                   [:new-name sym]              ;; New name to use for the function (if :auto, the transformation generates a name), Default: :auto
                   [:check-guard bool]          ;; Default: nil, whether to check the claimed relationship in the body of the function (may be needed for termination)
                   [:show-only bool]            ;; Default: nil
                   )

Detailed Description

Consider a function, F(x) [assume F is unary for this discussion], whose body includes some term, T(x), over the parameter x. It may be the case that T could be calculated incrementally (that is, we can use the current value of T(X) to compute the value of T(x) that will be needed on the next iteration, after x is updated). This may be cheaper than calculating T(x) each time.

The transformation does the following:

Build a function version of F(x), call it F$1-pre(x,v), that has an additional parameter (call it v) which is always equal to T(x). All recursive calls must be changed pass the updated value of the new V parameter. F$1-pre will compute this for each call by replacing x in T(x) with the actual value of x passed to the recursive call. This establishes the invariant v=T(x) on the recursive calls.
Prove that F$1-pre(x) is equivalent to F$1(x,v). Note that F$1-pre ignores its v parameter (but F$1, built below, will not).
Build F$1 by simplifying the body of F$1-pre, in two ways: 1) Simply use the new v parameter instead of computing T(x). 2) Simplify the update of v passed to each recursive call, using distributed laws provided by the user, to express it in terms of T(x) = v. This is the key incrementalization step.
Prove that F$1(x,v) is equivalent to F$1-pre(x,v) assuming v = T(x).
Build a wrapper function that calls F$1 with thv V parameter initialized to T(x), thus establishing the invariant.
Prove that the wrapper function is equal to the original F.