Transformations as Proofs

This paper is a companion to [Hen93] which explores in depth the relationship between transformational programming and intuitionistic proofs in a theory of operations and types. Here we concentrate on discussing the extension of the theoretical development to algebraic data types and illustrating the techniques with an example. 2 Introduction and background We are concerned primarily with the task of uncovering the precise mathematical proofs which underlie certain semi-formal arguments. In the area of program development the program transformations [BuD77] are an excellent example of semi-formality, since, as is well known, the calculus of transformations is not, in general, sound 1 , and it is capable of effecting significant shifts in logical complexity by, what superficially appears to be, equational manipulation. In [Hen93] we provided an interpretation of certain transformations over N as derivations within a theory of operations and types (the theory EON of [Bee85]). The mai..