Title :
Equality in lazy computation systems
Author :
Howe, Douglas J.
Author_Institution :
Dept. of Comput. Sci., Cornell Univ., Ithaca, NY, USA
Abstract :
The author introduces a general class of lazy computation systems and defines a natural program equivalence for them. He proves that if an extensionality condition holds of each of the operators of a computational 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 considered so far. Conditions are given under which the equivalence coincides with observational congruence. These results have important consequences for type theories
Keywords :
data structures; equivalence classes; formal logic; computational system; equality reasoning; equivalence relation; extensionality condition; lazy computation systems; natural program equivalence; observational congruence; syntactic condition; type theories; Computer languages; Computer science; Reasoning about programs;
Conference_Titel :
Logic in Computer Science, 1989. LICS '89, Proceedings., Fourth Annual Symposium on
Conference_Location :
Pacific Grove, CA
Print_ISBN :
0-8186-1954-6
DOI :
10.1109/LICS.1989.39174
