Rewriting techniques for analysing termination and complexity bounds of Safe programs

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 and stack memory consumption during the evaluation of an expression f(e1,..., en) depends on the number of calls to f. Ensuring termination of Safe programs (or of particular function calls) is therefore essential to implement these analysis. Furthermore, being able to give bounds to the number of recursive calls required by a terminating initial call becomes essential in computing space bounds. In this paper, we first investigate how to analyze termination of Safe programs by using stan-dard term rewriting techniques. First, we transform a Safe program into a term rewriting system. We provide a correct and complete transforma-tion for that purpose, i.e., termination of the original Safe program P is completely characterized as (innermost) termination of the transformed TRS RP. Then, termination can be automatically analysed by means of existing tools such as AProVE, mu-term, or TTT. We provide explicit bounds for the number of calls which are issued during the evaluation of an expression as above. We also investigate how to use proofs of termi-nation which combine the dependency pairs approach with polynomial interpretations to obtain such numeric bounds