Algebraic identities for program calculation

Abstract

To calculate a program means to derive it from a suitable specification by a process of equational reasoning. We describe a number of basic algebraic identities that turn out to be extremely useful in this task. These identities express relationships between the higher-order functions commonly encountered in functional programming. The idea of program calculation is illustrated with two non-trivial examples.