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

Pasquale Noce 📧

December 1, 2013

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Tail_Recursive_Functions