Size invariant and ranking function synthesis in a functional language

Abstract

Size analysis is concerned with the compile-time determination of upper bounds to the size of program variables, including the size of the results returned by functions. It is useful in many situations and also as a prior step to facilitate other analyses, such as termination proofs. Ranking function synthesis is one way of proving termination of loops or of recursive definitions. We present a result in automatic inference of size invariants, and of ranking functions proving termination of functional programs, by adapting linear techniques developed for other languages. The results are accurate and allow us to solve some problems left open in previous works on automatic inference of safe memory bounds.