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 result 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 the definition of functions so that the constraints on operations such as inversion can be greatly relaxed. The specificational functions that emerge generalize 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 functions as embodied in programming languages. The idea of specificational functions is not new, but accommodating them in all their generality without falling foul of a myriad of anomalies has proved elusive. We investigate the technical problems that have hindered their use, and propose solutions. In particular, we develop a formal axiomatization for reasoning about specificational functions, and we prove its consistency by constructing a model.
INTRODUCTION
The square function on the integers, defined by sqr -
z), is not traditionally
regarded as having a well-defined inverse, because it is neither injective
nor surjective. Suppose, however, we were to broaden our definition of functions
so that the inverse of sqr, call it sqrt, is indeed a function. We might define sqrt
thus:
Permission to make digital/hard copy of all or part of this material without fee is granted
provided that the copies are not made or distributed for profit or commercial advantage, the
ACM copyright/server notice, the title of the publication, and its date appear, and notice is given
that copying is by permission of the Association for Computing Machinery, Inc. (ACM). To copy
otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific
permission and/or a fee.
M. Morris and A. Bunkenburg
We have used above an instance of what we can call a prescriptive expression.
This has the general form (2x:T j P ) and the intuitive meaning some x of type T
satisfying predicate P . If there is no such x, we regard (2x:T jP ) as being equivalent
to the special expression ?, pronounced "bottom". If there are many such x, then
we have no information about which outcome is actually produced. For example,
sqrt 4 may yield 2 or \Gamma2, and we don't know or care which. Indeed, we cannot even
determine its behavior by experiment, because if sqrt 4 yields 2 in the morning, it
may well yield \Gamma2 in the afternoon. Both sqrt 7 and sqrt(\Gamma4) yield ?.
Here is another example: Suppose the type PhoneBook is comprised of all relations
from type Name to type PhoneNumber. Then the following function looks up
a person's phone number in a phone book:
lookUp -
Again, lookUp is not necessarily a function in the traditional sense (because some
people are not listed in phone books, and some have several entries) but we would
like to treat it as such.
For a more elaborate example, consider the function
which takes as arguments a function f and a set s, and selects some element a of
s such that f a is minimized. For example, instantiating T with Z,
yields either 1 or \Gamma1. We can define leastWRT for any type T thus:
To illustrate its use, we make a function to be used by two lovers each of whom
travels from city to city as a computer consultant. The function should yield a city
to which they should both travel if they want to be together as soon as possible. We
assume a type City whose elements are all cities, and a function time:City \Theta City!N
which yields the least traveling time (in minutes, say) between any two cities. The
function is
-his; hers:City ffl leastWRT (-c:City ffl time(his; c) max time(hers; c)) City:
In need not be a so-called "flat" type such as the integers,
but can be a more structured type such as a function type. For example,
specifies the familiar factorial function. For a more elaborate example of the
usefulness of choice over function types, let us specify a program for playing a
one-player game such as Rubik's Cube. We assume a context which provides a set
Cube of all the legitimate states of the game, a set LegalMoves which is a subset
of Cube $ Cube describing the set of legal moves, and a value goal 2 Cube which
describes the goal of the game. A player will be modeled as a function f :Cube!Cube
is the position to which the player moves when in position b:
Players -
Specificational Functions \Delta 3
We eliminate players who get stuck:
GoodPlayers -
Each player has a cost, which is the total number of moves taken to play all possible
games:
cost -
The program we want is
GamePlayer -
cost GoodPlayers:
All of sqrt, lookUp, leastWRT, and GameP layer are examples of functions more
liberally defined; we call them specificational functions.
Although specificational functions are not in general computational, they do play
an important role in specifying computational functions. For example, sqrt might
be presented to a programmer as a specification of a program he should implement,
by which is meant that he should produce a computational function SQRT whose
behavior is consistent with that of sqrt. By "consistent" we mean that when SQRT
is applied to a perfect square x it yields a square root of x (either negative or non-
negative), and otherwise it behaves in any way that the programmer fancies. For
example, the programmer might well design SQRT such that its graph is
We say that SQRT is a refinement of sqrt and write sqrt v SQRT. Roughly
holds of expressions E and F if in all contexts the possible
outcomes of E is a superset of the possible outcomes of F , with the slight twist
that ? is refined by all terms (which is the mathematical way of saying that if
the customer asks for the impossible, he had better be willing to accept whatever
he is given!). Readers not familiar with refinement calculi may feel, with good
cause, that w would be a more appropriate symbol for refinement, but v is what is
traditionally used (it may help to think of v as suggesting increasing information-
content). For example, in the context of applying SQRT to 4, the outcome 2
is among the outcomes of applying sqrt to 4 (2 and \Gamma2), and in the context of
applying SQRT to \Gamma2, the outcome 49 is acceptable because sqrt applied to \Gamma2
yields ?.
A refinement calculus is, in essence, a language with a transitive refinement relation
v, where some of the terms in the language are computational, and the
remainder are available for describing desired behavior. The process of making a
program consists in producing a sequence of language terms, t0 v t1 v ::: v tn,
where t0 is the customer's specification, tn is computational, and each term in the
sequence (except the first) is constructed incrementally from its predecessor. We
say that each term in the sequence is a refinement of its predecessors. Programming
by stepwise refinement [Wirth 1973] is an example of such a process, albeit
a somewhat informal one because the terms of the language are written partly in
informal pseudo-code. The motivation for studying specificational functions is a
desire to use them as part of a refinement calculus that supports the development
of functions, whether in functional or imperative programming.
Unlike stepwise refinement, we have in mind a fully formal mathematical system
in which each refinement is formally provable by deduction from given axioms.
M. Morris and A. Bunkenburg
ff (-x:T ffl E) j (-y:T ffl E[xny]), fresh y
E) j (-x:T ffl F
extensionality
Skolem
Fig. 1. Axiomatic properties of functions
This requires an axiomatization of logic, an axiomatization of base types that the
functions operate on, and an axiomatization of functions themselves. Traditional
functions are typically axiomatized by postulating properties such as those in figure
replaced by F
(subject to the usual caveat of renaming to avoid variable capture), and similarly
for predicates. In j and extensionality, E and F are of functional type T!U . (The
listed properties are not independent of one another, so no one axiomatization
would use all of them).
If we employ such axioms on specificational functions, we fall foul of a myriad of
anomalies, as we shall see shortly. The effect has been to inhibit their deployment
seriously. For example, it is common to restrict choice to flat types only, which rules
out, for example, the specification GamePlayer above. We investigate the technical
problems and propose solutions. In particular, we develop a formal axiomatization
for reasoning about them and show that it sees off the anomalies.
1.1 Outline of rest of paper
The next section will introduce the concepts and notations for equivalence, re-
finement, choice, and "proper" values. The third section explains in detail the
anomalies that occur when functions and choice meet, and suggests ways of avoiding
them. The fourth section axiomatizes these language constructs, and pairs.
The fifth section is the core of the paper. It presents an axiomatization of specificational
functions that avoids the discussed anomalies. The sixth section discusses
logic, and argues for our prefered logic. The seventh section gives a denotational
model of the calculus. Finally, we draw conclusions and review related literature.
1.2 Contributions
-Detailed exposition of six anomalies that occur when functions and choice are
combined.
-Suggestions how these anomalies can be avoided.
-An axiomatization of specificational functions.
-A denotational model.
2. MATHEMATICAL PRELIMINARIES
2.1 Equivalence, choice, and refinement
We presume the availability of a (strong) equality operator j on terms, reserving the
for the weak or computational equality operator found in programming
languages. (Weak equality is further explained below.) We will use "equivalence"
Specificational Functions \Delta 5
as a synonym for strong equality. Equivalence is reflexive, symmetric, transitive,
and a congruence: if replace F in any term without changing
its meaning.
The choice inherent in (2x:T j P ) may be unbounded, as in (2x:Z j true) which
may yield any integer. On the other hand, there may be no x satisfying P , as in
(2x:T jfalse); we introduce the special term ? T as an abbreviation for (2x:T jfalse).
It may seem intuitively reasonable that ? v F should hold for no term F , but
refinement calculi commonly depart from intuition by postulating ? v F for all
terms F . We adopt the latter approach (known as excluding miracles). The calculus
it gives rise to is arguably easier to apply in practice, although the underlying theory
is slightly more complex. This choice is not central to the concerns of this paper,
and nothing of substance in what follows depends on it. Note that (2x:T j true)
differs from ? T in that ? T is refined even by a "non-terminating" expression such
as an application of the recursive function f where f -
x. There is a
bottom for each type, indicated by subscripting, but we nearly always omit the
type, either because it is not significant in the context, or it can be easily inferred.
In refinement calculi, partial operations such as 3=0 are commonly equated with
?, and similarly for nonterminating expressions. It is also customary to use ? as
a "don't care'' term by which the customer indicates that she has no interest in
the outcomes. Although it may be useful in other contexts to distinguish these
various roles for ?, in program derivation they are similar in that they represent
error situations in which the outcome is unpredictable and unconstrained.
When there is precisely one x of type T satisfying predicate P - call it k -
then equivalent to k. One consequence of this is that specificational
functions include traditional total functions. Any finite choice can be expressed
in terms of a binary choice E u F which specifies a choice among terms E and F
(we use the words "term" and "expression" interchangeably). For example, 2 u 3
specifies 2 or 3, without preference; it can be written equivalently as (2x:Z j x j
It should be evident that u is commutative, associative, and idempotent.
It is a standard postulate in refinement calculi that refinement and equivalence are
related by E). It follows that v is reflexive, transitive and
antisymmetric (with respect to j). It also follows that ? is a zero of u.
Readers coming from a background in formal logic might be tempted to view
rough equivalent of Hilbert's ffl operator [Leisenring 1969], but
that would be a mistake. There is little connection between the two. Roughly
speaking, ffl represents choices that have already been made for you and for everyone
now and for all time, whereas 2 represents choices that have yet to be made and
which may be made differently on different occasions. A Hilbert choice from 2 and
3 is always 2 or always 3 - we just don't know which one it is. On the other hand,
2 u 3 is sometimes 2 and sometimes 3. In formal terms, the ffl operator satisfies
the axiom words "if P is true of some x of type
T , then it is true of (fflx:T j P )". This assertion does not hold when ffl is replaced
with 2. For example, letting J abbreviate (fflx:Z j x we have the
truth of J but with K standing for (2x:Z j x
false. The ffl operator is not useful for program refinement, because
it requires that any "looseness" in a specification be resolved by programmers in the
same way at all times and in all places. For example, if a customer asked that some
6 \Delta J. M. Morris and A. Bunkenburg
error message be displayed if a file was unavailable, without stating any preference
as to the wording of the message, it would require every programmer to deliver
exactly the same message. More amusingly, if all choice was Hilbert's choice, then
the diners in a restaurant would each choose the same meal from the menu.
We postulate that the operators of the base types (like on the integers)
are strict (i.e., ? is a zero for them) and distribute over choice. This design decision
properly reflects the fact that our brand of choice allows different resolutions on
different occasions. For example, although (2 u would be equivalent
to 0 according to Hilbert's brand of choice, we admit the possibility that the first
occurrence of (2u3) has outcome 2, while the second has outcome 3, and vice versa.
Hence behaves strictly and distributively,
just
2.2 Propers
The instantiation rule for universal quantification asserts that from the truth of
any term E. But such instantiation rules can
easily lead to inconsistencies in the presence of bottom and choice. For example,
is a theorem of arithmetic, and so we might be tempted to infer that
in contradiction of our earlier conclusion that
similar anomaly arises if we instantiate with ? - we can infer
There are two ways out of this dilemma: Either we modify the standard
laws of arithmetic to take into account bottom and choice, or we modify the rules
of instantiation. The easiest fix is to modify the instantiation rules by forbidding
instantiations with ? or terms involving (an unresolvable) choice; we call such terms
improper and all other terms proper. For example, ? and 2u3 are improper, whereas
are proper (in the final example, we have assumed
that ! distributes over u). Our intention is that every expression should be either
proper or bottom or a choice among propers. The requirement that 8x:T ffl P (and
similarly, only be instantiated with proper terms is a condition on the
underlying logic. In the terminology of [S-ndergaard and Sestoft 1992], we have
opted for strict singular semantics; they list alternate approaches.
Technically, an expression E of type T is proper iff 9x:T ffl E j x. Of course,
to ensure that this is a useful definition, we shall have to axiomatize each type so
that we can infer the truth or otherwise of 9x:T ffl E j x. We postulate that the
common base types Z; Char; Float; ::: are flat, i.e. 8x; y:T ffl
From this we can deduce that for flat types, E u F is proper iff E is proper and
equivalent to F . We also postulate that the constants (such as, in the case of the
integers, 0, 1, \Gamma1, 2, \Gamma2, :::, etc.) are proper. We can now formally deduce that
say, is not proper because 2 is proper and differs from 3. We write proper E
as an abbreviation for 9x:T ffl
Non-flat types (such as function types) are considerably more complex than flat
types, and determining just which expressions should be proper need not be at
all obvious, as we shall see. Because most of us came to know functions through
studying functions on the integers and reals, it is easy to be seduced into accepting
properties of functions that may hold for functions on flat types, but which are not
true in general. This is even more so in the case of specificational functions, and
we advise the reader to think of non-flat types whenever he or she is looking for
Specificational Functions \Delta 7
intuitive understanding. We have ourselves sometimes been misguided by thinking
in terms of flat types only.
For the purpose of examples, we will denote by Two a type which has (at least)
two propers u and v such that u ! v, i.e. u v. Whether such
a type exists, is of course a consequence of our design decisions. However, usually
functional types are non-flat, for example which might both
reasonably be considered proper.
For the remainder of the paper we use lower case letters for proper ex-
pressions, and upper case letters for arbitrary (possibly improper) expressions

3. THE ANOMALIES
In this section, we expose some of the problems that are encountered when a
straightforward axiomatization of functions drawn from figure 1 is used in the presence
of bottom and choice.
3.1 Beta-equivalence and extensionality
For specificational functions, the combination of axioms fi and extensionality leads
to an inconsistency. Consider -x:Z ffl x\Gammax and -x:Z ffl 0. By extensionality, we
conclude that they are equivalent, since 8x:Z ffl x\Gammax j 0. But if now we apply each
function to ? in turn, we can deduce that ? j 0! Similarly, we can deduce that
by applying the two functions to 2 u 3 in turn.
It is not fruitful to attack the anomaly by restricting the extensionality axiom,
because the two functions in question are so simple that we expect them to be
equivalent by extensionality, however restricted. The remedy we shall adopt is to
restrict the fi axiom to proper arguments. Now the anomalies disappear, since
neither ? nor 2 u 3 are proper.
Of course, we are left with the question of assigning a meaning to applications
with improper arguments. We choose to make function application strict and distribute
over choice. In symbols, E G. Now both
example functions yield ? when applied to ?, and 0 when applied to 2 u 3.
We should not forget that function types also accommodate bottom and choice.
For reasons of symmetry, we decide that function application should be strict and
distributive in the function as well as in the argument, i.e.
G. These decisions aren't controversial, since there is no reasonable
alternative, but they do lead to a quandary, as we shall see.
The above is the first of several examples of inconsistencies that arise from naively
applying the traditional laws of functions; ridding ourselves of them requires com-
promise. We choose our compromises to make life as pleasant as possible when
we put our tools to their intended use. If our purposes change, then so might our
compromises. For example, not insisting on strictness would be appropriate if the
target program language is a lazy functional language like e.g. Haskell [Peterson
and Hammond 1997]; such a calculus is explored in [Bunkenburg 1997]. In [Hehner
1993; 1998], the decision as to whether function application distributes over choice
is left open in general; it must be decided individually for every abstraction the
developer writes.
M. Morris and A. Bunkenburg
3.2 Distribution and j
The following inconsistency was discussed but not solved satisfactorily in [Meertens
1986].
Using j, we prove
their equivalence by transforming one into the other (here and elsewhere, we omit
type information to reduce syntactic clutter):
G
F:
Now we can show that 3 u 4 u 5 u 6 j 3 u 6 by applying the higher-order function
to F and G in turn:
assuming F is proper
(1
whereas for G we get:
3 u
We definitely do not want 3 u 4 u 5 u 6 j 3 u 6. (In the calculation, we have
assumed that -x ffl x u 3 is proper. We shall see later on that this is reasonable.)
The j-axiom also leads us to conclude that ? T!U and -x:T ffl ?U are equivalent:
ap. strict
Specificational Functions \Delta 9
But this runs counter to practice in imperative and functional programming
languages. In imperative languages, for example, the body of a function f supplied
as an argument to a procedure proc is not inspected at the point of invoking proc,
but only at the point of invoking f within the body of proc.
We will resolve these dilemmas by restricting the j-axiom to proper functions
only, with ? T!U and such functions as (-x ffl x) u (-x ffl being improper. We will
have much more to say about properness of functions later on.
3.3 Extensionality and distribution
Postulating distribution of application has the consequence that extensional equivalence
of functions breaks down in the presence of higher-order functions. Consider
as before F -
any proof of their
equivalence must lead to a contradiction because -h ffl
them. Previously, we proved them equivalent by j and distribution; now we prove
them equivalent by extensionality:
, extensionality
, u/ap.
We will choose to resolve the inconsistency by having function equivalence require
more than extensionality in general (it will turn out that in the case of proper
functions, extensionality is sufficient). On reflection, this restriction should not be
surprising because unrestricted extensionality identifies the functions ? T!U and
against our wishes.
3.4 Monotonicity and distribution
It is not too difficult to deduce that if function application distributes over u then
function application is monotone with respect to v, that is,
It follows that we can introduce an inconsistency if we can construct a non-monotone
function. Such a function is f : Two!U such that f u
(recall Two has two propers u and v such that u ! v). Assuming a conditional
expression whose first argument is a proposition is available, we can construct f
thus: -x:Two ffl if x j u then 1 else 2.
We shall avoid this anomaly by admitting only -abstractions -x:T ffl E such that
The restriction is not a hindrance in practice because it turns out that all operators
used in programming languages, and just about all those used in specifications
are indeed monotone. The function f above is non-monotone because j is a non-monotone
operator. Trivially, all functions on flat domains are monotone, even if
their bodies employ non-monotone constructs. It is possible to set down reasonable
M. Morris and A. Bunkenburg
syntactic rules for forming -abstractions that guarantee monotonicity (although
some acceptable -abstractions might be ruled out).
It is a little disappointing that when we refine the (monotone) body of a -
abstraction, we retain the obligation to show monotonicity - it is not necessarily
preserved by refinement. For example, if x j uthen 1u2 else 1, which is monotone,
is refined by if x j u then 2 else 1, which is not monotone! Fortunately, such
examples are rare (those we know of rely on the use of the strong j or v operators).
However, there are some theoretical surprises as we shall see later.
3.5 Monotonicity and Skolem
The Skolem axiom, (8x:T ffl9y:U fflP ) ) (9f :T !U ffl8x:T fflP [ynf x]), which promises
the existence of certain functions, seems intuitively reasonable, but in the presence
of the monotonicity requirement on functions, it may be promising the impossible.
Recall again type Two with propers u and v such that u ! v. Let P -
holds. But the
function f promised by the Skolem axiom would have to map u to 1 and v to 2,
and this is not monotone. The essence of the problem is that with the restriction
to monotone functions, the Skolem axiom promises the existence of a monotone
mapping for every possibly non-monotone mapping, and that promise cannot be
kept.
We shall not postulate Skolem as an axiom, but will be able to derive it for
"reasonable" P . For example, if the x in P (x; y) is drawn from a flat type, then
Skolem holds. We will return to this point later.
4. THE AXIOMATIZATION PROCESS
We axiomatize prescriptive and conditional expressions. We also explain our method
for axiomatizing types and their operations, using pair-types as an example. This
will serve as a model for the more complex function types to come.
4.1 Axiomatizing language constructs
Let -E abbreviate E 6j ?. The following postulate captures the intuitive idea of
refinement as described earlier:
(The conjunct (-E ) -F ) is required to distinguish between ? T and (2x:T ffl
true).) From this, and the antisymmetry of v, we can deduce:
It follows that to determine whether a given expression E is refined by another
expression F , or whether E is equivalent to F , all we need to know is whether or
not E and F are bottom, and if not then what propers refine them. So for any
language construct FOO, we need to be able to determine -FOO and FOO v x
(fresh x), and in general our strategy will be to define these by axioms. For a simple
example, see the axiomatization of u in figure 2.
The defining axioms of prescriptive expressions are given in figure 3. (The axiomatization
of prescriptive expressions makes assumptions about the underlying logic.
Specificational Functions \Delta 11
u-(E
Fig. 2. Axioms for u
Fig. 3. Axioms for prescriptive expressions
Different assumptions might be made, but they would give rise to some similar
axiomatization.)
It is possible to axiomatize some language constructs FOO by defining FOO v E
for arbitrary expression E. Then we can determine -FOO by instantiating E with
?, and we can determine FOO v x by instantiating E with x. See, for example,
the axiomatizations of conditional and assertion expressions in figure 4.
The assertion expression has the form P ?\Gamma E; it is equivalent to E if P is true, and
otherwise it is ?. Assertion expressions (called "assumptions" in [Ward 1994], and
discussed e.g. in [M-oller 1989], and increasingly becoming part of specification and
program languages, e.g. Eiffel [Meyer 1992]) serve to annotate expressions with a
little knowledge that can be used in their further refinement. For example, finding a
zero of a function on the integers might be specified as -f :Z!Z ffl (2x:Zjf
we now wish to inform the implementor that the function will only ever be invoked
for monotonically increasing functions, then we can specify
4.2 Axiomatizing types
For each new type that is introduced, we must provide axioms describing its propers.
For the case of pair types, properness seems perfectly straightforward: all proper
pairs are of the form (x; y) for proper constituents x and y, and for every proper x
and y, (x; y) is a proper pair. This is captured in the first two axioms in figure 5.

Figure

5 also gives the axiomatization of operations on pairs. Observe the shape:
there are two axioms to describe each type constructor - here, just pair forma-
tion, and two axioms to describe each type destructor - here, the two projection
functions (we just describe the left projection fst, the right projection snd is simi-
lar). The third axiom states that pair formation is strict in both arguments. The
fourth states that refinement is carried out component-wise; the formulation of the
axiom is slightly cluttered by the need to state that refinement is guaranteed if
either component is ?. Because of the intimate relationship between refinement
and choice, the import of this axiom is that pair-formation distributes over choice
in both arguments. The axioms for fst are obvious. The final axiom in fact implies
that fst distributes over choice.
Fig. 4. Axioms for conditional and assertion expressions
M. Morris and A. Bunkenburg
Fig. 5. Axioms for pair types
5. AXIOMATIZING FUNCTIONS
We axiomatize function types, following the same strategy as for pairs, and keeping
in mind the desired properties of functions collected earlier.
5.1 The core axioms
A partial axiomatization of functions is given in figure 6. Recall that we use lower
case letters for propers, and uppercase letters for arbitrary expressions. Conse-
quently, the lower case variables in figure 6 can be universally quantified over (we
have not done so to minimize syntactic clutter), but not the upper case ones. We
have also omitted types to avoid clutter. For example, the first axiom in full is
The first axiom is just familiar j-equivalence on proper functions and shows that
every proper function can be written as a -abstraction. Taking pair types as our
model, we should expect a companion axiom which determines which -abstractions
are proper. It turns out that a lot can be said without committing to that axiom,
and so we postpone further consideration of it for a moment.
The second group of axioms defines -abstraction. Axiom - ensures that our
desire to distinguish ? and -x:T ffl ? is met. Axiom -v implies our desired property
of extensional equivalence for proper functions.
The remaining axioms define the single function destructor, viz. application, in
effect asserting that function application is strict and distributive, and that application
can be reduced to substitution. The essential interplay between abstraction
and application is captured in axiom fij (there is nothing corresponding to axiom
fij in pair types). Axiom ap.- states the three ways by which function application
yields ?: either the function is ?, or the argument is ?, or the application
is normal but yields ?. Observe in both ap:- and ap.v that function application
determined by considering all applications e f where e and f are proper
refinements of E and F , respectively.
Even though we have not yet fixed what abstractions are proper, the axioms of
figure 6 imply a large body of desired theorems, including those listed in figure
7. In particular, function application is strict, distributive, and monotone on
either side. For proper functions, refinement and equivalence are extensional. A -
abstraction can be refined by refining its body (assuming monotonicity is preserved).
The bound variable in an abstraction can be renamed (this is assuming that the
logic gives renaming of universally quantified variables). Finally, moving choice out
of an abstraction is a refinement, not an equivalence as might be expected. To
see this, observe that -x:Z ffl if even x then 2 else 3 refines -x:Z ffl 2 u 3, whereas
Specificational Functions \Delta 13
E)
E) v f,(8x
fij (-x ffl E) y j E[xny]
Fig. 6. Core axiomatization of functions
ap.mon.
ap.mon. G v H
mon. E) v (-x ffl F )
-ff (-x ffl E) j (-y ffl E[xny]) x not in the free variables of E
E) u (-x ffl F )
Fig. 7. Some theorems which follow from the axioms of figure 6
has as refinements only itself, -x:Z ffl 2 and -x:Z ffl 3.
To illustrate the axioms, we prove -mon. from the axioms and then deduce -=u:
E) v (-x ffl F )
E) E)
, axioms -v
transitive
We deduce:
E) u (-x ffl F )
, u is greatest lower bound with respect to v
E) -x ffl E
, -mon.
E) -
which is a property of choice.
The axioms of figure 6 resolve all the anomalies of section 3. For example, recall
functions F -
We used the putative
equivalence of these functions in Section 3 to construct difficulties with both j
and extensionality. Although they remain extensionally equal, they are no longer
equivalent:
14 \Delta J. M. Morris and A. Bunkenburg
, (2)
, -F , -G, arbitrary f
, G; u v
- the final line does not in general hold, which can be seen by instantiating f
with -x ffl if even x then x else 3.
5.2 Proper functions
We must now address the question "What functions are proper?". First, we definitely
expect traditional functions to be proper, i.e. those abstractions -x:T ffl E
for which E is proper for all (proper) x.
Second, we have already ruled that ? T!U is not proper.
Third, consider those abstractions -x:T ffl E for which E is ? for some or all values
of x and proper for the remaining values of x, i.e. the traditional partial functions.
Assume for a moment that we deem these to be improper, and consider the extreme
example Because -x:T ffl ? is improper and not ?, it must be equivalent
to the choice over its proper refinements. But that is impossible, because by our
assumption all proper functions have proper outcomes. We conclude that we must
include the partial functions among the propers.
Finally, we are left with the question of whether functions such as -x ffl 2 u 3
whose bodies contain an unresolvable choice, are to be considered proper. There
seem to be two reasonable views. The liberal view is to accept all abstractions as
proper. The conservative one is to regard -x ffl 2 u 3 as improper, in which case it is
equivalent to the choice over the (infinite) collection of proper functions that refine
it, i.e. all functions whose application to any argument is equivalent to either 2 or
3 (but not 2 u 3), including -x ffl 2, -x ffl 3, -x ffl if even x then 2 else 3 and many
others. According to this view, an abstraction is proper iff its body is proper or
bottom.
The liberal view can be adopted by postulating the axiom
-prop: proper(-x:T ffl E)
(Incidentally, axiom - can be erased from figure 6 in the presence of this axiom
since it follows therefrom, assuming the underlying logic ensures 8x:T ffl -x.) It has
the disadvantage that the proper functions include rather exotic elements which we
will frequently have to exclude explicitly, cluttering up our specifications. On the
other hand, the liberal view is often convenient calculationally. In particular, we
can tell by appearance whether a function F is proper or not, and hence whether
F can be the subject of an instantiation, and whether fij applies when F is the
argument of a higher order function.
The conservative view is embodied in the axiom
E) , (8x:T ffl -E ) proper E)
Specificational Functions \Delta 15
It states, in effect, that the proper functions are the partial functions of mathe-
matics. However, in calculations it may be hard to prove that a given abstraction
is proper, or that there exists a proper function satisfying some property. For in-
stance, to show that -x ffl E has a proper refinement, i.e. 9f ffl (-x ffl E) v f , we have
to show 9f ffl 8x ffl E v f x. But it is not enough to exhibit a mapping from x to y x
such that 8x ffl E v y x - we must find a monotone mapping.
Although the liberal and conservative views seem roughly equally attractive on
the surface, the conservative view has to be rejected because of a subtle anomaly.
Consider function G -
else 1. This would seem to
have two refinements (other than itself), i.e. G 1
and G 2
else 1. However, G 2
has to be rejected because
it is not monotone. We can now conclude with the help of law (2) that G j G 1
, in
contradiction of our assumption that G 1
is proper while G is not! It seems that the
only reasonable escape is to include G among the propers. Now (2) implies G 6j G 1
because G has G itself as a proper refinement, whereas G 1
does not. The root
cause of this anomaly is that certain seemingly natural refinements of functions are
lost to the monotonicity requirement. Although this is true of both the liberal and
conservative views, it is not significant in the former view because the "parent"
function is retained among the proper refinements and so no information is lost.
In conclusion, specificational functions are axiomatized by figure 6, with axiom
- replaced by -prop.
5.3 Total functions
Function types bring a new subtlety to the notion of properness. Up to this point,
we have had the property that if E is proper then it has no refinements other than
itself, but this no longer holds once function types are introduced. For example,
although both functions are proper. Let us say
that an expression E (of type T , say) is total and satisfies total E, iff it has no
refinements other than itself, i.e. iff x. For example, -x:Z ffl 2
is total, but not -x:Z ffl x-0 ?\Gamma 2. On flat types (and pair types derived from flat
types), totality and properness are identical. On function types, however, totality
is stronger than properness, and in fact specializes to the usual sense of the word.
Totality is obviously an important concept. We can use it to rescue the Skolem
axiom which we have shown cannot hold for specificational functions in general.
We can prove
There still remains an irritation, however: although Skolem promises the existence
of a function f satisfying a property P , it is not guaranteed that all the
refinements of f also satisfy P . For that, we should restrict ourselves to predicates
that are monotone in y in the sense y v y 0
x. This condition is automatically satisfied when the type of y is flat.
5.4 Recursive functions
Recursively defined functions have the form -f :T !U ffl -x:T ffl E where E is of type
U and may contain free occurrence of f . This notation allows us to write a recursive
function without naming it. More usually, recursive functions are simultaneously
M. Morris and A. Bunkenburg
unfold (-f ffl -x ffl E) j -x ffl E[fn-f ffl -x ffl E]
prefix -x ffl E[fnF E) v F
Fig. 8. Axioms for recursive functions
described and named by writing f -
may occur in E. The
body of the recursive function must be monotone in f to ensure that
the fixpoint exists (more details of this are given in the section on denotational
semantics below). We axiomatize recursion in the standard way as a fixpoint, and
the least prefixpoint with respect to refinement; see figure 8 (again, types have been
omitted).
In program development, -abstractions are refined to recursive functions by recursive
refinement. Suppose we set out to implement the specification -x ffl E via
recursion. Our modus operandi is to proceed through a series of refinements beginning
with E and ending with a term of the form F [-x ffl E] where -x ffl E appears
within F. Along the path, we will have transmuted non-algorithmic notation into
algorithmic substitutes. We can now almost conclude that -f ffl -x ffl F [f ] is the
recursive function we were after, i.e. (-x ffl E) v (-f ffl -x ffl F [f ]). We say "almost"
because we have not ensured that the recursion is well-founded, or in programming
terms, that invocations of the recursive function terminate. As every programmer
knows (although not necessarily in formal terms), to ensure termination of a recursive
function, the argument of each recursive call must be less that the "incoming"
arguments with respect to some well-ordering. This added requirement is captured
in the formal statement of the recursion introduction theorem below:
Theorem -fun. If E v F [fn-y ffl y!x ?\Gamma E[xny]] for all x then (-x ffl E) v
is a well-order on the source type of f .
Proof. To begin:
E) v (-f ffl -x ffl F )
, axm unfold
E) v (-x ffl F [fn-f ffl -x ffl F ])
We prove 8x:T ffl E v F [fn-f ffl -x ffl F ] by well-founded induction
where here P [x] -
arbitrary x of type
Specificational Functions \Delta 17
( assumption of the theorem, and v transitive
mon. in expression variable f
, axm unfold
, thm -ff
, thm -mon.
5.5 Example
We construct a small program to decompose a natural number into the sum of two
squares. The starting specification is
ss -
We proceed in the standard way for such problems by choosing a finite search
space containing an i and j such that (assuming there is such an
and then repeatedly testing the pairs it contains. If the candidate (i; j) we test
are done, and if not we reduce the search space by removing
(and any other pairs we can eliminate at the same time). We choose as our
search space all the (i; j)'s such that lo - lo and hi are some
naturals, initially 0 and b
nc, respectively. In summary,
ss v -n:N ffl ss 1
(0;
\Xip
where
ss 1
lo
Let E denote the body of ss 1
. It is not difficult to conclude the following facts
about E:
lo
lo
lo
Using elementary properties of if ::: then ::: else ::: we infer
else if lo 2
else ss 1
For a termination argument, observe first that -E implies lo - hi. Second,
observe that in comparison with E, which is ss 1
(lo; hi), the absolute difference
of the two arguments of ss 1
is less by 1, and similarly for ss 1
M. Morris and A. Bunkenburg
1). Practitioners will recognize the ingredients for the well-founded ordering to
show termination when -E holds; we omit the details. When -E does not hold,
termination is not an issue. Hence, we have shown ss1 v f where
else if lo 2
else
6. BOOLEANS AND PROPOSITIONS
Naturally, every refinement calculus will have the booleans as a given basic type
(which will be a flat type). Although it is common to define the boolean connectives
as strict and distributive (see, for example [Larsen and Hansen 1996]), or as left-to-
right evaluating (see, for example, [Partsch 1990]), these turn out to be seriously
unattractive. Many of the familiar laws of boolean algebra break down, with the
result that the booleans become awkward to handle calculationally. It turns out,
however, that the boolean connectives can be extended to accommodate bottom
and choice in quite a different way such that almost all the familiar laws of boolean
algebra continue to hold (the main loss is the law of the excluded middle). This is
described in [Morris and Bunkenburg 1998a; 1998b].
Actually, because the language of a refinement calculus is used to make specifications
(which are a superset of programs), the operations in every type will be about
as rich as mathematics can provide. In particular, in specificational languages the
boolean type includes arbitrary universal and existential quantifications, even over
infinite domains. Again, it turns out that the quantifiers can be suitably extended
to allow for bottom and choice while retaining just about all the laws of predicate
calculus (the only loss is that instantiation can only be carried out with proper
terms). See [Morris and Bunkenburg 1998b] for the details, including a Hilbert-style
axiomatic presentation.
We have made few assumptions about the logic with which we reason about
specifications, and so our theory is pretty much independent of the choice. Our
own choice is unusual. Because we have had to construct a comprehensive axiomatization
of the booleans including quantifiers, we have elected to avoid duplicated
effort by adopting the same logic for reasoning about specifications. In short, we
do not distinguish between propositions and booleans. This means, for example,
that even something as exotic as E v F or E j F is a boolean expression (and
hence a specification). There are advantages and disadvantages. One disadvantage
is that refinement and equivalence are the primary sources of non-monotonicity in
-abstractions. An advantage is that it facilitates the smooth transition of specifications
to programs, because propositions can migrate effortlessly into specifica-
tions/programs, as often they want to when we formally extract programs from
specifications. See [Morris and Bunkenburg 1998b] for an example of this.
7. MODEL THEORY
In this section, we provide a denotational semantics for the language constructs we
have given. The purpose is to ensure consistency of the calculus and to underpin
our understanding of it, particularly recursion. The model is parameterized by
models of base types and a logic.
Specificational Functions \Delta 19
T \Theta U [T ] \Theta [U
Fig. 9. Interpretations of the types
The grammar of the types is type
given base types Each type is interpreted by a complete partial order
element that none of the [T ] contain. For each T , we extend the partial order
The usual way of giving semantics to a functional programming language is to
interpret every expression of type T as an element of [T ] ? . However, this approach
does not accommodate choice.
We can accommodate choice by interpreting every expression E as the subset
of [T ] ? that intuitively contains interpretations of all the possible outcomes of E.
To model recursion and refinement, we need an order on these sets. The order
appropriate for a 'total correctness' calculus (i.e. one in which E u? j ?) such as
this one is the "Smyth" order (v 0 ) (see [Plotkin 1976; Smyth 1978]), defined by
where A and B are subsets of [T ] ? . Inconveniently, (v 0
) is not antisymmetric. We
make it antisymmetric by restricting it to upclosed sets only.
The upclosure of a subset S of a partial order (P; -) is written S" - , defined by
pg. To avoid double subscripts, we abbreviate S" -T by
. Conveniently, for upclosed sets, (v 0
is identical with ('). Therefore, we
will interpret every expression of type T as an upclosed subset of [T
meaning to recursion and refinement using (').
For every type T , we denote by P [T ] the set fS
g, that is, the
upclosed subsets of [T ] ? . We abbreviate P [T
For each base type B i , a set [B i ] is given, and it will be ordered simply by equality.
Pair types are interpreted as the product of the constituent types. The function
type T!U is interpreted by the functions f from [T ] to P 1
[U ] that are monotone
in the sense that t - T u . The interpretation of base type Z, and the
interpretations of pair- and function-types, are collected in figure 9, where - 0
and
denote the left and right projections from pairs to their constituents.
Construction of a universal domain D, which is a superset of [T ] for every type
T , is clerical, using the definitions in figure 9. Readers familiar with models of the
untyped -calculus will note that we do not require D since we are dealing
with a typed language.
An environment ae is a mapping from each variable of type T to an element of
[T ]. In addition, it maps each recursion-dummy f of type T!U to an element of
Expressions are interpreted by induction on their structure. Every expression E
of type T is interpreted in environment ae by the set [E]ae, which is an element of
J. M. Morris and A. Bunkenburg
proposition interpretation in ae
Fig. 10. Interpretation of refinement and equivalence
expression X of type its interpretation [X]ae
if P then E else F if [P
c f[c]g
where ap(e; f)-= if
rec. dummy f ae f
where
Fig. 11. Interpretation of the expressions
For each constant c of base type T , we are given an element [c] of [T ]. For every
operator symbol f of the base types we are given a "matching" function [f ]. By
"matching" we mean that if the argument types of f are T its result
type is U , then [f ] is a function in [T 0
We don't give a model for the logic. Rather we assume that every proposition
P is interpreted in environment ae as some element [P ]ae. We assume that tt is the
interpretation of some theorem of the logic, and that ff is the interpretation of some
anti-theorem of the logic. With two-valued logic, the domain of propositions would
be ftt; ffg, the interpretations of true and false. We give interpretations for the
propositions

Figure

11 gives the semantics of the typed expressions. It can easily be verified
that for every expression E of type T , its interpretation [E]ae is a set upclosed with
respect to - T .
The recursive function -f ffl -x ffl E is interpreted by the fixpoint of the functional
F as defined. F acts on P [T !U ] which is a complete lattice under the order '. By
the language restriction that -x ffl E must be refinement-monotone in f , we ensure
that F is '-monotone, and therefore the generalized limit theorem ([Hitchcock and
Park 1972; Nelson 1989]) ensures that a least fixpoint exists. The mathematics of
this construction do not exclude cases where -F is the empty set, or where -F is
Specificational Functions \Delta 21
a set containing functions that map some arguments to the empty set. One should
choose the specification language in such a way that this cannot happen, and in
fact -F is an element of P 1
Finally, we give some examples. The three expressions 2, 2 u 3, and ?Z are
interpreted as f2g, f2; 3g and f?; 0; ::g. The abstraction -x:Z ffl 2 is
interpreted as the singleton set containing the function that maps every element
of [Z] to f2g. The abstraction -x:Z ffl 2 u 3 is interpreted as the set containing all
those functions mapping each element of [Z] to a non-empty subset of f2; 3g.
8. CONCLUSION AND RELATED WORK
Specificational functions are made by combining regular functions with choice and
bottom, taking special care to accommodate higher-order functions. We have shown
examples of their usefulness both in making specifications, and in extracting computational
functions from those specifications. The technical difficulties that stand
in the way of establishing a consistent set of laws for reasoning about them are well
known, and have led to severe restrictions on their use in the past (see the commentary
on related work below). We have picked our way around these difficulties
to arrive at an axiomatic treatment which does not fall foul of the anomalies. The
key elements in our approach are:
(1) a richer notion of equivalence than extensionality, based on refinement;
(2) a restriction on quantifications to range over proper elements only, where properness
is carefully defined for each type; and
(3) the imposition of a monotonicity requirement on functions.
Clearly, some compromises have to be made, but we believe that practicioners could
comfortably live with the compromises we have arrived at.
The two standard ways of combining functions and choice are to move to set-valued
functions or to generalize functions to binary relations. Here we reject
moving to set-valued functions, because in calculations it leads to frequent packing
and unpacking of values in to and out of sets even though often the set is just a
singleton set. The relational approach lends itself well to calculation (see e.g. [Bird
and de Moor 1997; Brink and Schmidt 1996]). However, we would like to stick
with functions because they capture better the directional nature of programs as
input-to-output mappings. This decision means we don't lose the direct connection
to current program languages which have functions, not relations.
Munich CIP is a development method based on a wide-spectrum language CIP-L;
a comprehensive account of it is given in [Partsch 1990]. CIP-L has similar concepts
to our choice, equivalence ("strong equality"), refinement ("descendancy"), bottom
and properness. Functions are defined as (possibly recursive) abstractions. How-
ever, there are severe limitations placed on functions in CIP-L. Most importantly,
choice and quantification over functions is forbidden. It is not clear to us how this
restriction is enforced. In this paper, bodies of -abstractions must be monotone
in the bound variable. In CIP-L that is automatic, since every language construct
is monotone anyway. All -abstractions are considered proper. The main transformation
rules are ff, fiv (called "unfold"), and our theorem E[xnF
-F , but no concise axiomatization is given in [Partsch 1990] and so it is not clear
which "rules" are axioms and which theorems.
22 \Delta J. M. Morris and A. Bunkenburg
Calculation with functions is dealt with in the thesis [Hoogerwoord 1989]. The
language has underdetermined "where" clauses that specify a value by asserting a
property it enjoys. This is closely related to Hilbert's ffl, and so refinement is pretty
much impossible.
Norvell and Hehner present a refinement calculus for expressions in [Norvell and
Hehner 1993], by giving an incomplete list of axioms for a language similar to the
one discussed here. The main differences lie in the treatment of termination and the
properness of functions. Their calculus does not have a term bottom representing
non-termination, and it is therefore a partial correctness calculus. For termination
of recursive programs they annotate the expressions with abstract execution times.
It is not clear how refinement and timing relate. An abstraction -x ffl E is a proper
function (in their terminology "an element") iff E is proper for all x. Since the
language has no bottom, that implies that only traditional functions are elements.
It seems their intention to have flat types only, which would avoid the anomalies of
our subsections 3.4 and 5.2. However, we believe their system is inconsistent, since
there are -abstractions that are non-miraculous refinements of proper functions
which implies that function types are non-flat.
In closely related work ([Hehner 1993; 1998]), a half-and-half approach to distributivity
of functions over choice in their arguments is described. They distinguish
between those occurrences of the parameter in the body of the function for which
distribution is appropriate, and those for which direct substitution of the argument
is appropriate. These occurrences can be syntactically decided, and of course are
fixed for each function. Therefore, some -abstractions do distribute over choice in
their arguments, and others don't. However, this approach seems to impose a host
of trivial concerns on the programmer. It is not clear whether there are sufficient
compensating gains.
Ward's thesis ([Ward 1994]) presents a functional specification and programming
language, defined by a semantics that models demonic and angelic choice. However,
the language is not given a proof theory, and there is no suggestion that the given
refinement laws are sufficient in practice. New refinement laws can be generated
by proving candidates sound using the semantics. All abstractions are proper;
therefore function types are non-flat, and the inconsistency described in subsection
3.4 occurs, but is not addressed.
The language of VDM includes "loose let-expressions" of the form
let x:T be s.t. P in E:
Its intended meaning is: E with x bound to an arbitrary value satisfying P . How-
ever, its axiomatization has proved elusive, and [Bicarregui et al. 1994] suggest the
approach taken by [Larsen and Hansen 1996].
Larsen and Hansen [Larsen and Hansen 1996] present a denotational semantics
for a functional language with under-determinism. The type language is extended
by comprehension-types of the form fE j x:T ffl Pg, and the expression language
is extended by choice T , under-deterministically selecting an element of the type
T . However, which element is chosen depends on the whole environment, even on
those variables that don't occur in T . The proof system is based on generalized
type inference, with propositions of the rather than equivalence and
refinement relations. Indeed, it is hard to see how equivalence and refinement would
Specificational Functions \Delta 23
fit in. Larsen and Hansen consider those lambda-abstractions proper that map
propers to bottom or propers. Therefore the anomalies of subsections 3.4 5.2 could
be reproduced, if strong operators such as j were added to the language.
Previous work by one of the present authors ([Morris 1997]) gives weakest-
condition semantics to an expression language with choice and bottom. The style
of semantics fits the weakest-precondition semantics of the imperative refinement
calculus. However, no axioms or logic is given, and issues pertaining to functions
are not addressed.

ACKNOWLEDGMENT

We thank David Watt and Richard Botting for reviewing drafts of this paper.



--R


Proof in VDM: A practioner's guide.
Algebra of Programming.
Relational Methods in Computer Science.
Supplemental Volume
Expression Refinement.
Avoiding the undefined by underspecification.
A practical theory of programming.
Unified algebra.
Induction Rules and Termination Proofs.
The design of functional programs: a calculational approach.

Semantics of under-determined expressions
Mathematical Logic and Hilbert's ffl-symbol


Eiffel: The Language.


E3: A logic for reasoning equationally in the presence of partiality.
Undefinedness and nondeterminacy in program proofs.
A generalization of Dijkstra's calculus.

Specification and Transformation of Programs.

A Powerdomain Construction.
Power domains.

A refinement calculus for nondeterministic expressions.
Systematic Programming

--TR
The/Munich Project CIP
A generalization of Dijkstra''s calculus
Specification and transformation of programs: a formal approach to software development
Eiffel: the language
Non-determinism in functional languages
A practical theory of programming
Proof in VDM
Algebra of programming
Non-deterministic expressions and predicate transformers
Relational methods in computer science
Systematic Programming
Applicative Assertions
Logical Specifications for Functional Programs

--CTR
J. M. Morris , A. Bunkenburg, A source of inconsistency in theories of nondeterministic functions, Science of Computer Programming, v.43 n.1, p.77-89, April 2002
Joseph M. Morris , Malcolm Tyrrell, Terms with unbounded demonic and angelic nondeterminacy, Science of Computer Programming, v.65 n.2, p.159-172, March, 2007
function;refinement calculus;nondeterminacy;logic;expression