Specificational functions

Mathematics supplies us with various operators for creating functions from relations, sets, known functions, and so on. Function inversion is a simple example. These operations are useful in specifying programs. However, many of them have strong constraints on their arguments to ensure that the resu lt is indeed a function. For example, only functions that are bijective may be inverted. This is a serious impediment to their use in specifications, because at best it limits the specifier's expressive power, and at worst it imposes strong proof obligations on the programmer. We propose to loosen t he definition of functions so that the constraints on operations such as in version can be greatly relaxed. The specificational functions that emerge g eneralize traditional functions in that their application to some arguments may yield no good outcome, while for other arguments their application may yield any of several outcomes unpredictably. While these functions are not in general algorithmic, they can serve as specifications of traditional fu nctions as embodied in programming languages. The idea of specificational f unctions is not new, but accommodating them in all their generality without falling foul of a myriad of anomalies has proved elusive. We investigate t he technical problems that have hindered their use, and propose solutions. In particular, we develop a formal axiomatization for reasoning about speci ficational functions, and we prove its consistency by constructing a model.