A Precise Characterization of Extended Tail-recursive Definitions

S. Ray

Technical Report TR-08-47, Department of Computer Sciences, University of Texas at Austin, November 2008.

Abstract

Extended tail-recursive definitional equations are definitional equations involving quantification and tail-recursion that can be introduced in the logic of the ACL2 theorem prover. This paper corrects a previous mistake by the author in the characterization of extended tail-recursive definitions, and provides a precise characterization of such definitions.