ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 24
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 1. An Introduction to Denotational Semantics
|
| 1.5. A Preview of Partially Additive Semantics (cont.)
|
| We next seek a suitable sum operation for partial functions.
| It is easy to see that when each f_i in (9) is a partial function
| (i.e., a multifunction which happens to be a partial function, cf.
| 1.4.9-10) then Sum f_i need not be. In the case of (10), let f, g
| be partial functions and x be such that f(x) and g(x) are defined
| and different. Then the sum f + g maps x to the set {f(x), g(x)}
| and so is not a partial function. To better understand what needs
| to be fixed, imagine the "fanout" in (10),
|
| |
| |
| |
| v
| o-----------------o-----------------o
| | |
| | |
| | |
| v v
|
| as controlled by a test such as "if f is defined go left;
| if g is defined go right". For multifunctions, such a test can
| pass the input down both lines simultaneously. For partial functions,
| we demand that such a test choose 'at most one' alternative and define
| (10) only when DD(f) |^| DD(g) = Ø. We have motivated the definition:
|
| 11. Let X, Y be sets and let (f_i : i in I) be an I-indexed family in
| Pfn(X, Y). Then (f_i : i in I) is 'summable' in Pfn(X, Y) if for
| all i, j in I with i =/= j, DD(f_i) |^| DD(f_j) = Ø. In that case,
| Sum f_i = Sum(f_i : i in I) in Pfn(X. Y) is defined by:
|
| DD(Sum f_i) = |_|^(i,I) DD(f_i)
|
| ( f_j (x), if there exists j with x in DD(f_j),
| (Sum f_i)(x) = <
| ( undefined, else.
|
| Note that we do not require that I be finite.
| The following is an immediate result:
|
| 12. If (f_i : i in I) is summable,
|
| then (Sum f_i)ˆ = Sum(f_iˆ),
|
| where fˆ is defined in 1.4.9 and
| the latter sum is that of (9).
|
| Thus, the Pfn sum, when it exists, specializes the Mfn sum.
|
| In particular, we have for one-element families
|
| 13. Sum(f) = f
|
| and for empty families
|
| 14. Sum Ø = 0
|
| where 0 : A -> B denotes the everywhere undefined
| partial function characterized by DD(0) = Ø. It is
| obvious that we may extend a summable family by adding
| any number of 0's or we may delete any number of 0's which
| are already there without affecting either the summability of
| the family or the value of the sum. It is for this reason that,
| in this context, we prefer the notation 0 instead of the alternate
| notation _|_ introduced in Exercise 1.3.6.
|
| Our operation of sum, then, differs from ordinary numerical addition
| in two fundamental respects:
|
| a. It is not always defined. Indeed, for any f in Pfn(X, Y)
| with DD(f) =/= Ø, f + f is never defined. The "partial" in
| "partially additive" refers to this property -- addition (= sum)
| is only partially defined.
|
| b. There are many infinite families whose sum is defined.
|
| We remark that even finite sums such as (10) cannot be implemented
| in an unrestricted way. It is well known from computability theory
| that given two programs which compute partial functions f, g there is
| no way to decide, in general, if DD(f) |^| DD(g) = Ø, and this makes it
| hard to imagine a suitable approach to compute f + g for arbitrary f, g
| (see Exercise 4 for an unsuccessful attempt). There remains the option
| to restrict the use of sum to "provably disjoint" families, and this will
| in fact be what happens when we give a partially additive semantics for
| iteration in Section 3.3 (see also (27) below).
|
| Manes & Arbib, AAPS, pages 29-30.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤