The direct declarative language, with put, discard and composition, was presented as a category in Section 4.3 . Besides its obvious covariant imperative action on states, it has a contravariant action on predicates. We saw that these midconditions f[[(x)\vec]] belong naturally at the semicolons between commands, at each of which there is also an associated list [(x)\vec] of program-variables, namely those which are in scope at that point. But we only defined the contexts (objects of the category) to consist of the typed variables, so now we shall also incorporate the midconditions.
We aim to identify the essential categorical features of the imperative action, where the interpretation of such a context is the set of states of [(x)\vec] which satisfy f[[(x)\vec]], ie the comprehension {[(x)\vec]|f[[(x)\vec]]}. If f[[(x)\vec]] is a family of equations, we already know how to express this subobject directly in category theory, as an equaliser; this will be extended to full first order logic in Section 5.8.
Midconditions were introduced with a view to proving correctness of programs, but they are also used to control (non-)termination. Although we cannot cause non-termination in the programs we build until we introduce recursion or while loops in Section 6.4, the building blocks may themselves be non-terminating if applied indiscriminately. We use conditionals to ensure that they only get called in circumstances where we know that they are defined and produce correct results.
EXAMPLE 5.3.1 In the program for the cubic equation (Example 4.3.4), some of the operations involved are only defined on part of R, or have ambiguous results. We must be clear, for example, that Ö{ } and cos-1 are the inverses of maps (-)2:P® P and cos:H® I, where the subsets P = [0,¥), H = [0,p] and I = [-1,1] of R must also be objects of the category.
If, as in Section 4.3, the meaning of a program is to be a morphism of a category whose objects are simply lists of program-variables, then this morphism must be allowed to be a partial one. We can restore totality by introducing virtual objects, defined by program-variables together with midconditions. In particular, the troublesome primitive operations in the cubic equation program are treated as partial functions (Section 3.3) whose supports are given by known predicates, ie the preconditions which guarantee termination and correctness.
For this approach to be adequate for recursive or while programs, the logic used to define the virtual objects must be strong enough to express the termination or otherwise of the program-fragments which are about to be executed, and in particular stronger than the program itself could verify. This is the case if category S incorporates the predicate calculus, with quantification over N, or is simply assumed to be (like) Set. This chapter adopts the point of view of traditional categorical logic, which aims to describe the category of sets and functions. Our account therefore falls short of a purely syntax-driven construction.
REMARK 5.3.2 Let u:G® D be a terminating (everywhere defined) program, where G = [[(x)\vec]:[(X)\vec]]. The interpretation of its restriction to the subset on which f[[(x)\vec]] holds is of course the composite
|
|
omitted diagram environment
The top map is unique because the right hand one is an inclusion. This square is a pullback iff f is the weakest precondition u*q for which the property is valid (Remark 4.3.7).
In the terminology of Example 3.8.3, we still aim for total correctness; partial correctness is more useful for while programs (Remark 6.4.16) .
REMARK 5.3.3 Notice that we have returned to the more general notion of context developed for the predicate calculus (Definition 1.5.4), which involves both typed variables and logical formulae. Given that the Floyd rules are anyway not fully specified without a statement of the variables involved, with their types, we now see them as a minor variant of our standard notation u:[G,f]® [D,q].
Computationally, G is the physical range of the program-variables. The state is confined to [G,f] only by a ``gentlemen's agreement,'' namely the proof of the preceding program-fragment: the program could be started (such as in a debugging environment) at this intermediate point in any state [(a)\vec] Î [[G]] . Consider, for example, the type of primes (with the usual binary representation of numbers), or the type of codes for programs that terminate. These acquire their meaning by intension, not extension.
The discard commands divide Example 4.3.4 into seven phrases. Each one is interpreted as a bijection, whose inverse is essentially given by the comments. When a set is defined using comprehension in Zermelo type theory, it is commonly understood to be interchangeable with any isomorphic set, defined by some other set-theoretic formula. However, in the case of a program such as this, to dismiss these isomorphisms as mere changes of representation of the same object would trivialise this historic achievement in algebra. So, in a computational intuition this virtual object is more closely related to the ambient G than to any isomorphic [D,q]. There is a rigid division of the context between typed variables and predicates. The axiom of comprehension makes the division permeable, emancipating the subset (Sections 9.2 and 9.5).
Partial morphisms Now we drop the assumption that u:G® D is total on the physical range of the program-variables. We begin by defining partial functions in terms of a given class of total functions in a category S such as Set. Afterwards, we consider how the total functions and virtual objects can be recovered when the possibly non-terminating programs are the raw material.
DEFINITION 5.3.4 A partial function with source X, target Y and support U in a category S is an isomorphism class of diagrams like
omitted diagram environment
The m:U\hookrightarrow X may be required to belong to a class M of supports (Definition 5.2.10). When m is an isomorphism, the function is total.
Definition 3.3.4 defined equality and the extension order (f\sqsubseteq g) on partial functions, exactly analogously to the definitions for subobjects in Section 5.2. They also bear the same relation to the category of spans used in Lemma 4.5.16 as S¯ X @ \SubS(X) did to the slice S¯ X.
PROPOSITION 5.3.5 Composition of partial functions, U;V, defined by pullback, is associative, cf Lemmas 1.6.6 and 4.1.3. (Note that U;V is defined as a subobject, ie as an isomorphism class of such pullbacks, so it is legitimate to say that associativity holds up to equality.)
omitted diagram environment
We write \nearrow [thick] = P(S,M) for the category composed of partial functions.
PROOF: Use Lemma 5.1.2.
omitted diagram environment
The diagram on the right shows that a second pullback also arises; it is used in Exercise 5.53 and Section 6.4. []
REMARK 5.3.6 An alternative view of partial functions starts from the category \nearrow [thick] and tries to recover S and M:
|
Proposition 5.8.7 considers an approach to relations analogous to this one for partial functions. A similar construction using virtual objects applies. Section 6.4 shows how while programs can be interpreted using coequalisers; in this case the virtual objects form a far larger structure than is needed to prove the soundness result.
Conditionals Even when no proof of correctness has been supplied for a program, it is still natural to think of the branches of a conditional as defined only on the virtual subobjects described by the condition or its negation. The word `` if'' is misleading: the test is not a proposition as in implication but a computable function. Failure is not enough to cause execution of the else branch: that only happens when the test has succeeded in producing the second value. This all too common confusion with logic may be avoided by regarding the condition as a question, to which yes and no are possible responses: there may be no answer at all. The two parts are put together in the same way as those of a disjunction (ÚE )-box or a coproduct.
DEFINITION 5.3.7 The conditional declarative language extends the \bnfname programs of Definition 4.3.1 by
|
ASSUMPTION 5.3.8 Without loss of generality, the test c terminates without side-effect. This can be ensured by inserting putz = c before the conditional. The test is then just that of a variable of type 2 (Boolean), ie of a single bit ( b inary dig it). We shall need this in the following account because it only uses the test to select one of the branches, and does not incorporate it into the flow of control.
REMARK 5.3.9 The interpretation of a conditional with test c is defined in terms of the restrictions of the two branches to the virtual objects
|
omitted diagram environment
The conditional is then the mediator [g,f]:G® Q, which is a bijective correspondence so long as the triangles Y® G®Q and N® G® Q commute. This requires the b- and h-rules
omitted eqnarray* environment
The b- and h-rules make G the coproduct Y+N of the virtual objects for the two branches. However, this is not the typical coproduct situation, as ours also has to agree with a pair of pullbacks.
EXAMPLE 5.3.10 In Sections 4.3 and 4.6 we saw how to interpret the individual lines of the cubic equation program (Example 4.3.4). The whole program is the composite along the top of
omitted diagram environment
where the dotted line is a product mediator, and we still have to define the lower map in terms of the conditional. (The numbers refer to the seven phrases into which the discard commands break the program.)
Writing Y,N Ì R2 for the complementary subsets of R2 on which the condition succeeds and fails, the two maps are then as shown.
omitted diagram environment
REMARK 5.3.11 The Floyd rule (Remark 4.3.5) for conditionals is
|
|