A General Method for the Proof of Theorems on Tail-recursive Functions

Pasquale Noce 📧

December 1, 2013

Abstract

Tail-recursive function definitions are sometimes more straightforward than alternatives, but proving theorems on them may be roundabout because of the peculiar form of the resulting recursion induction rules.

This paper describes a proof method that provides a general solution to this problem by means of suitable invariants over inductive sets, and illustrates the application of such method by examining two case studies.

License

BSD License

Topics

Session Tail_Recursive_Functions