Correctness of fixpoint transformations

AbstractFormal languages, recursive program schemes, program transformations and many other theories in computer science are closely related to systems of equations on various algebraic structures. Transformations on equations usually show important properties of the original problems. A transformation on a system of equations is said correct if it keeps the desired solution unchanged. In this paper correctness of transformations, especially fixpoint transformations, is investigated. Based on general representations of these transformations, necessary and sufficient judging their correctness are given. Applications of the results are illustrated with various examples