Total correctness by local improvement in program transformation

Abstract

The goal of program transformation is to improve efficiency while preserving meaning. This paper presents a condition for the total correctness of transformations on recursive programs, which deals with higher-order functional languages (both strict and non-strict) including lazy data structures. The main technical results is an improvement theorem which says that if the local transformation step are guided by certain optimization concerns, then correctness of the transformation follows.