Symbolic functional evaluation

Abstract

Symbolic functional evaluation (SFE) is the extension of an algorithm for executing functional programs to evaluate expressions in higher-order logic. SFE carries out the logical transformations of expand- ing de_nitions, beta-reduction, and simpli_cation of built-in constants in the presence of quanti_ers and uninterpreted constants. We illustrate the use of symbolic functional evaluation as a “universal translator” for link- ing notations embedded in higher-order logic directly with automated analysis without using a theorem prover. SFE includes general crite- ria for when to stop evaluation of arguments to uninterpreted functions based on the type of analysis to be performed. SFE allows both a novice user and a theorem-proving expert to work on exactly the same speci_- cation. SFE could also be implemented in a theorem prover such as HOL as a powerful evaluation tactic for large expressions.