The derivation of functional equivalents of imperative programs

Denotational semantics is presented as a valuable theoretical tool, having many applications including language design, compiler generation and program analysis. In particular, a method is described for deriving a concise and useful functional representation of a program using a denotational definition of the source language´s semantics. Our aim is to translate a given program into a compact functional representation to facilitate its evaluation on functional hardware. The λ-expressions are first translated into Turner´s combinator code (D. Turner, 1979). We choose to use a fixed set of combinators as the resulting code is more amenable to analysis and there are many inherent advantages such as lazy evaluation and once only evaluation of reducible sub-expressions. Semantic algebras relating to static semantics and the store algebra are “unfrozen” so they can be partially evaluated. The reduction machine that performs the evaluation includes simplification rules that allows a more compact functional representation (denotation) to be reached. If desired, some or all of the program arguments can be supplied to produce a new denotation (result) using the same reduction machine