Abstract: | In this paper I present an automatic technique for transforming a program by changing the data types in that program to ones which are more appropriate for the task. Programs are synthesised by providing modified synthesis theorems in the proofs-as-programs paradigm. the transformation can be verified in the logic of type theory.
Transformations are motivated by the presence of subexpressions in the synthesised program. A library of data type changes is maintained, indexed by the motivating subexpressions. These transformations are extended from the motivating expressions to cover as much of the program as possible.
I describe the general pattern of the revised synthesis proof, and show how such a proof can be guided by difference matching followed by rippling.
|