Type-changing rewriting and semantics-preserving transformation

We have identified a class of whole-program transformations that are regular in structure and require changing the types of terms throughout a program while simultaneously preserving the initial semantics after transformation. This class of transformations cannot be safely performed with typical term rewriting techniques, which do not allow for changing the types of terms.In this paper, we present a formalization of type-and-transform systems, an automated approach to the whole-program transformation of terms of one type to terms of a different, isomorphic type using type-changing rewrite rules. A type-and-transform system defines typing and semantics relations between all corresponding source and target subprograms such that a complete transformation guarantees that the whole programs have equivalent types and semantics. We describe the type-and-transform system for the lambda calculus with let-polymorphism and general recursion, including several examples from the literature and properties of the system.