A simple calculus for program transformation (inclusive of induction) (Q578898)

A basic purpose of transformation systems is the application of `correctness-preserving rules' in order to derive from given programs new, `equivalent' ones. An important aspect here is the usage of induction principles, without which transformation systems would have too limited power. The paper presents a formal system of `transformation rules' that incorporates induction. This system is a kind of `Gentzen-style calculus', impoverished, however, to a degree that just meets the needs of program transformation. Thus we achieve a basis for the design of transformation systems, which is both simple and sound.