Equality in Lazy Computation Systems

unofficial copies [PDF], [PS]

by Douglas J. Howe

Proceedings of Fourth IEEE Symposium on Logic in Computer Science, pp. 198-203, 1989.


In this paper we introduce a general class of lazy computation systems and define a natural program equivalence for them. We prove that if an extensionality condition holds of each of the operators of a computation system, then the equivalence relation is a congruence, so that the usual kinds of equality reasoning are valid for it. This condition is a simple syntactic one, and is easy to verify for the various lazy computation systems we have considered so far. We also give conditions under which the equivalence coincides with observational congruence. These results have some important consequences for type theories like those of Martin Lof and Nuprl.