Combinator Graph Reduction:A Congruence and its Applications

Abstract

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.