Equality in lazy computation systems. (English) Zbl 0716.68065

Howe, Douglas J.

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.

MSC:

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

Keywords:

program equivalence in lazy languages; lazy computation systems; type theories

Citations:

Zbl 0713.00018

Software:

Nuprl