Termination and complexity bounds for SAFE programs

Authors

Salvador Lucas and Ricardo Peña

Abstract

Safe is a first-order eager functional language with facilities for programmer-controlled destruction and copying of data structures and is intended for compile-time analysis of memory consumption. In Safe, heap memory consumption depends on the length of recursive calls chains. Ensuring termination of Safe programs (or of particular function calls) is therefore essential to implement these features. Furthermore, being able to giving bounds to the chain length required by such terminating calls becomes essential in computing space bounds. In this paper, we investigate how to analyze termination of Safe programs by using standard term rewriting techniques, i.e., by transforming Safe programs into term rewriting systems whose termination can be automatically analyzed by means of existing tools. Furthermore, we investigate how to use proofs of termination which combine the dependency pairs approach together with polynomial interpretations to obtain suitable bounds to the length of chains of recursive calls in Safe programs.