An Intensional Semantics for Elementary Program Transformations
Martin C. Henson · Journal of Logic and Computation · 1995
This paper is a contribution to the formal study and analysis of vernacular forms of program derivation. Specifically, in this paper, our vernacular derivations are elementary program transformations over the natural numbers. We provide an intensional semantics for these transformations within the derivations of the elementary theory of operations and numbers, ɛON. This semantics is intensional in the sense that the computational content of a derivation associated with a transformation is equal, up to the intensional equality underlying the theory ɛON, to the computational content of the transformation itself. The interpretation enables us to underwrite the correctness of the program transformations and, further, provides an analysis of correctness by classifying, via schema, the operations available by these transformations.