Skip to main content
PRL Project

Equality in Lazy Computation Systems

by Douglas J. Howe

Proceedings of Fourth IEEE Symposium on Logic in Computer Science

  • unofficial copies PDF, PS

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.

bibTex ref: Howe89

cite link