Operationally-Based Theories of Program Equivalence

Introduction This article describes some mathematical methods for verifying properties of programs in higher-order, functional languages. We focus on methods for reasoning about equivalence of expressions. Such methods are often based upon a denotational semantics of the programming language in question, using the mathematical theory of domains (Scott 1982; Plotkin 1981a). Here I will describe some methods which are based upon operational semantics (Plotkin 1981b). These operationally-based techniques have several attractive features. For example, there is relatively little mathematical overhead involved in developing the basic theory—in contrast with that needed to develop the existence and properties of recursively defined domains, the sine qua non of denotational semantics. On the other hand, domain theory provides an extremely powerful tool for analysing recursive program constructs. I believe that any serious attempt to develop a useful theory for verification of program properties has to involve both operational and denotational techniques. Highlights The main purpose of this article is to advertise the usefulness, for proving equivalences between functional programs, of co-inductive techniques more familiar in the context of concurrency theory (de Roever 1978; Park 1981; Milner 1989). They were imported into the world of lambda calculus and functional programming by several people: see Dybjer and Sander (1989); Abramsky (1990); Howe (1989, Howe (1996); Egidi, Honsell, and della Rocca (1992); and Gordon 1994.