Implementing an Automatic Differentiator in ACL2

Details Implementing an Automatic Differentiator in ACL2 Implementing an Automatic Differentiator in ACL2

2011-10-21

arxiv.org/abs/1110.4674v1

EPTCS 70, 2011, pp. 61-69

Computer Science

Symbolic Computation

In Proceedings ACL2 2011, arXiv:1110.4473

Scientific paper

10.4204/EPTCS.70.5

The foundational theory of differentiation was developed as part of the original release of ACL2(r). In work reported at the last ACL2 Workshop, we presented theorems justifying the usual differentiation rules, including the chain rule and the derivative of inverse functions. However, the process of applying these theorems to formalize the derivative of a particular function is completely manual. More recently, we developed a macro and supporting functions that can automate this process. This macro uses the ACL2 table facility to keep track of functions and their derivatives, and it also interacts with the macro that introduces inverse functions in ACL2(r), so that their derivatives can also be automated. In this paper, we present the implementation of this macro and related functions.

Affiliated with

Also associated with

No associations

Rating

Implementing an Automatic Differentiator in ACL2 does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Implementing an Automatic Differentiator in ACL2, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Implementing an Automatic Differentiator in ACL2 will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-84690