Termination Checking: Comparing Structural Recursion and Sized Types by Examples

Termination is an important property for programs and is necessary for formal proofs to make sense. In order to make sure that a program using recursion is terminating, one can use a termination checker that will use some strategy to verify the termination of a given program. Two very common strategies are structural recursion that makes an analysis on the structure of terms and sized types that use size annotation in the types. In this paper, we compare the two approaches to identify their strengths and limitations and to see how one can proceed to prove termination using each of the strategies. This analysis is done on different examples: a series of functions on the natural numbers and a mergesort algorithm. We also discuss the use of each of the approaches in the cases of proofs.