TANSTAAFL (with partial functions)
Chloe Jones · 1996
. Partial operators and functions are ubiquitous in program specifications, designs and arguments about both. There are several ways to ensure that logics can safely handle partiality. This paper identifies the costs associated with each of a variety of approaches to reasoning about partial functions. 1 The problem Much of classical mathematics focuses on total functions where given some function f , one can write an application of that function to a value in its domain and know that f (x ) denotes a value of a type fixed by the signature of the function. This property is easier to achieve in texts which are concerned with restricted families of functions; for example, a book on number theory would involve natural numbers and a small collection of operators. There are inconveniences such as `division by zero' but, if these are sufficiently limited, they can often be handled by textual comments. When writing specifications of computer systems, one is often faced with many different ty...