Another Look at Nested Recursion
Functions specified by nested recursions are difficult to define and
reason about. We present several ameliorative techniques that use
deduction in a classical higher-order logic. First, we discuss how an
apparent circular dependency between the proof of nested termination
conditions and the definition of the specified function can be
avoided. Second, we propose a method that allows the specified function
to be defined in the absence of a termination relation. Finally, we show
how our techniques extend to nested program schemes, where a termination
relation cannot be found until schematic parameters have been filled
in. In each of these techniques, suitable induction theorems are
automatically derived.
paper