• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
        • Simplify-defun
        • Isodata
        • Tailrec
        • Schemalg
        • Restrict
        • Expdata
        • Casesplit
        • Simplify-term
        • Simplify-defun-sk
        • Parteval
        • Solve
        • Wrap-output
        • Propagate-iso
        • Simplify
        • Finite-difference
          • Drop-irrelevant-params
          • Copy-function
          • Lift-iso
          • Rename-params
          • Utilities
          • Simplify-term-programmatic
          • Simplify-defun-sk-programmatic
          • Simplify-defun-programmatic
          • Simplify-defun+
          • Common-options
          • Common-concepts
        • Zfc
        • Acre
        • Milawa
        • Smtlink
        • Abnf
        • Vwsim
        • Isar
        • Wp-gen
        • Dimacs-reader
        • Pfcs
        • Legacy-defrstobj
        • Proof-checker-array
        • Soft
        • C
        • Farray
        • Rp-rewriter
        • Instant-runoff-voting
        • Imp-language
        • Sidekick
        • Leftist-trees
        • Java
        • Taspi
        • Bitcoin
        • Riscv
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Bigmems
        • Builtins
        • Execloader
        • Aleo
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Apt

    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:

    1. 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.
    2. 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).
    3. 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.
    4. Prove that F$1(x,v) is equivalent to F$1-pre(x,v) assuming v = T(x).
    5. Build a wrapper function that calls F$1 with thv V parameter initialized to T(x), thus establishing the invariant.
    6. Prove that the wrapper function is equal to the original F.