Programming Research Group Technical Monograph PRG-73

David Lester

April 1989, 136 pages, ISBN 0-902928-55-4

The G-machine is an efficient implementation of lazy functional languages developed by Augustsson and Johnsson. This thesis may be read as a formal mathematical proof that the G-machine is correct with respect to a denotational semantic specification of a simple language. It also has more general implications. A simple lazy functional language is defined both denotationally and operationally; both are defined to handle erroneous results. The operational semantics models combinator graph reduction, and is based on reduction to weak head normal form. The two semantic definitions are shown to be congruent.

Because of error handling the language is not confluent. Complete strictness is shown to be a necessary and sufficient condition for changing lazy function calls to strict ones. As strictness analyses are usually used with confluent languages, methods are discussed to restore this property.

The operational semantic model uses indirection nodes to implement sharing. An alternative, which is without indirection nodes, is shown to be operationally equivalent for terminating programs.

The G-machine is shown to be a representation of the combinator graph reduction operational model. It may be represented by the composition of a small set of combinators which correspond to an abstract machine instruction set. Using a modified form of graph isomorphism, alternative sequences of instructions are shown to be isomorphic, and hence may be used interchangeably.