A Mathematical Theory of Correct Computation

Source abstract

In 1970, Dana Scott proposed his highly influential “mathematical theory of computation” to define the relationship between the text of a program and what the program computes (or denotes)—the “semantics” of the program. Scott used a complete lattice based on the “information ordering”, with the bottom element representing undefined—a program failing to terminate normally, thus producing no information. The top element, however, was unused. Hence most subsequent applications of denotational semantics have used mathematical structures that avoid top elements. We suggest that the information ordering is relevant not only to semanticists but also to working programmers as a basis for determining if a program component or a computation is correct according to their intentions. We also suggest that a return to the use of complete lattices is called for, to broaden formal semantics and allow it to encompass programmer intentions. That is because often those intentions permit more than one runtime behaviour for a given input. In this paper we explore the connections between the information ordering, correctness of computations and programs, and debugging. We present a general theory and describe several instances where the intention for what our logic/functional code computes plus what it actually computes can be described by elements in a complete lattice. For correct code, the information order relates (1) what is intended and what is computed, (2) successive states of a computation, and (3) the left and right sides of program component definitions. For bugs, the information order is violated. The technical results are a reasonably straightforward extension to previous denotational semantics work, but the scheme aligns much better with practical programming and software tools. The theory extends both the theoretical basis and practical flexibility of declarative debugging and reasoning about partial correctness and gives an attractive mathematical framework that encompasses our intentions, our programs and what they compute.