An Algebraic Machine for Imperative Programs (Abstract)

J. Heering

(Joint work with Jan Bergstra, T.B. Dinesh, and John Field)

CWI, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands, e-mail: jan@cwi.nl

(Abstract available as P9504-3.ps.gz)

Abstract

In [Fie92] Field introduced PIM, an algebraic machine for the analysis, transformation, and optimization of imperative programs. For these purposes the algebraic framework is particularly attractive since it provides a uniform setting for modelling the standard dynamic semantics of a language (implemented as a confluent term rewriting system) as well as arbitrary semantics preserving program transformation and partial evaluation (using equations of the complete logic).

Whereas the standard semantics involves only rewriting of PIM ground terms, program transformation and partial evaluation amount to rewriting of PIM terms containing (meta)variables. The appropriate notion of completeness in this setting is not the well-known completeness of equational logic, but omega-completeness [Hee86,BH94] of the specification of PIM. Making an algebraic specification omega-complete usually requires hard work (if it is possible at all), and PIM is no exception.