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 X-expressions are first translated into Turner's combinator code (see [7]) WE choose to use a fired 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 programs arguments can be supplied to produce a new denotation (result) using the same reduction machine.