Abstract
In this paper, we describe recent improvements to the theory of differentiation that is formalized in ACL2(r). First, we show how the normal rules for the differentiation of composite functions can be introduced in ACL2(r). More important, we show how the application of these rules can be largely automated, so that ACL2(r) can automatically define the derivative of a function that is built from functions whose derivatives are already known. Second, we show a formalization in ACL2(r) of the derivatives of familiar functions from calculus, such as the exponential, logarithmic, power, and trigonometric functions. These results serve as the starting point for the automatic differentiation tool described above. Third, we describe how users can add new functions and their derivatives, to improve the capabilities of the automatic differentiator. In particular, we show how to introduce the derivative of the hyperbolic trigonometric functions. Finally, we give some brief highlights concerning the implementation details of the automatic differentiator.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Community portal for automatic differentiation, http://www.autodiff.org
Corliss, G., Griewank, A., Bischof, C., Carle, A., Hovland, P.: ADIFOR: Generating derivative codes from fortran programs. Scientific Programming (1) (1991)
Roh, L., Bischof, C., Mauer-oats, A.: ADIC: An extensible automatic differentiation tool for ANSI-C 27, 1427–1456 (1997)
Hovland, P.D., Bischof, C.H., Norris, B.: On the implementation of automatic differentiation tools. Higher Order Symbol. Comput. 21, 311–331 (2008)
Corliss, G., Faure, C., Griewank, A., Hascoet, L., Naumann, U. (eds.): Automatic Differentiation of Algorithms: From Simulation to Optimization. CIS. Springer, Heidelberg (2001); Selected papers from the AD2000 conference, Nice, France (June 2000)
Gamboa, R.: Continuity and differentiability in ACL2. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds.) Computer-Aided Reasoning: ACL2 Case Studies, ch. 18. Kluwer Academic Press, Dordrecht (2000)
Gamboa, R., Cowles, J.: The chain rule and friends in ACL2(r). In: Proceedings of the Eighth International Workshop of the ACL2 Theorem Prover and its Applications, ACL2 2009 (2009)
Gamboa, R., Kaufmann, M.: Nonstandard analysis in ACL2. Journal of Automated Reasoning 27(4), 323–351 (2001)
Griewank, A., Walthe, A.: Evaluating Derivatives: Principles and Techniques of Algorithmic Differentiation. Other Titles in Applied Mathematics. SIAM, Philadelphia (2008)
Kaufmann, M.: Modular proof: The fundamental theorem of calculus. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds.) Computer-Aided Reasoning: ACL2 Case Studies, ch. 6, Kluwer Academic Press, Dordrecht (2000)
Pearlmutter, A.B., Siskind, J.M.: Reverse-mode AD in a functional framework: Lambda the ultimate backpropagator. ACM Trans. Program. Lang. Syst. 30, 7:1–7:36 (2008)
Tadjouddine, E.M.: On formal certification of AD transformations. In: Barth, T.J., et al. (eds.) MFCS 1978. LNCSE, vol. 64, pp. 23–33. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Reid, P., Gamboa, R. (2011). Automatic Differentiation in ACL2. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds) Interactive Theorem Proving. ITP 2011. Lecture Notes in Computer Science, vol 6898. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22863-6_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-22863-6_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22862-9
Online ISBN: 978-3-642-22863-6
eBook Packages: Computer ScienceComputer Science (R0)