Implementing an Automatic Differentiator in ACL2

Peter Reid
(University of Oklahoma)
Ruben Gamboa
(University of Wyoming)

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.

In David Hardin and Julien Schmaltz: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2011), Austin, Texas, USA, November 3-4, 2011, Electronic Proceedings in Theoretical Computer Science 70, pp. 61–69.
Published: 20th October 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.70.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org