Equality in lazy computation systems. (English) Zbl 0716.68065

Logic in computer science, Proc. 4th Annual Symp., Pacific Grove/CA (USA) 1989, 198-203 (1989).
Summary: [For the entire collection see Zbl 0713.00018.]
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-Löf and Nuprl.


68Q60 Specification and verification (program logics, model checking, etc.)
68N15 Theory of programming languages
03F35 Second- and higher-order arithmetic and fragments
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
03B40 Combinatory logic and lambda calculus


Zbl 0713.00018