Floating point verification in HOL light: The exponential function

1997 ◽  
pp. 246-260 ◽  
Author(s):  
John Harrison
Keyword(s):  
Exponential Function ◽  
Floating Point ◽  
Hol Light

On a Fast, Compact Approximation of the Exponential Function

2000 ◽  
Vol 12 (9) ◽  
pp. 2009-2012 ◽  
Author(s):  
Gavin C. Cawley
Keyword(s):  
Exponential Function ◽  
Floating Point ◽  
Computational Expense ◽  
Point Representation ◽  
Compact Approximation

Recently Schraudolph (1999) described an ingenious, fast, and compact approximation of the exponential function through manipulation of the components of a standard (IEEE-754 (IEEE, 1985)) floating-point representation. This brief note communicates a recoding of this procedure that overcomes some of the limitations of the original macro at little or no additional computational expense.

A Fast, Compact Approximation of the Exponential Function

1999 ◽  
Vol 11 (4) ◽  
pp. 853-862 ◽  
Author(s):  
Nicol N. Schraudolph
Keyword(s):  
Neural Network ◽  
Exponential Function ◽  
Computation Time ◽  
Linear Interpolation ◽  
Lookup Table ◽  
Floating Point ◽  
Exponential Functions ◽  
Point Representation ◽  
Compact Approximation ◽  
Network Simulations

Neural network simulations often spend a large proportion of their time computing exponential functions. Since the exponentiation routines of typical math libraries are rather slow, their replacement with a fast approximation can greatly reduce the overall computation time. This article describes how exponentiation can be approximated by manipulating the components of a standard (IEEE-754) floating-point representation. This models the exponential function as well as a lookup table with linear interpolation, but is significantly faster and more compact.

scholarly journals Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL

2009 ◽  
Vol 53 (4) ◽  
pp. 465-488 ◽  
Author(s):  
B. Akbarpour ◽  
A. T. Abdel-Hamid ◽  
S. Tahar ◽  
J. Harrison
Keyword(s):  
Exponential Function ◽  
Floating Point

scholarly journals A Parameterized Floating-Point Formalizaton in HOL Light

2015 ◽  
Vol 317 ◽  
pp. 101-107 ◽  
Author(s):  
Charles Jacobsen ◽  
Alexey Solovyev ◽  
Ganesh Gopalakrishnan
Keyword(s):  
Floating Point ◽  
Hol Light
Sign in / Sign up

Export Citation Format

Share Document