Correctness Proofs of Transformation Schemas

Schema-based logic program transformation has proven to be an eective technique for the optimiza-tion of programs. Some transformation schemas were given in [3]; they pre-compile some widely used transformation techniques from an input program schema that abstracts a particular family of programs into an output program schema that abstracts another family of programs. This report presents the correctness proofs of these transformation schemas, based on a correctness de nition of transformation schemas. A transformation schema is correct i the templates of its input and output program schemas are equivalent wrt the specication of the top-level relation dened in these program schemas, under the applicability conditions of this transformation schema.