ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 20
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 1. An Introduction to Denotational Semantics
|
| 1.4. Multifunctions (cont.)
|
| We conclude this section by showing that partial functions (and so
| total functions) may be thought of as special cases of multifunctions.
|
| 9. Definition. For each f in Pfn(X, Y) define fˆ in Mfn(X, Y) by:
|
| ( {f(x)}, x in DD(f),
| fˆ(x) = <
| ( Ø, else.
|
| Such fˆ is closely associated to f. For example, f can be completely deduced
| from fˆ because DD(f) = {x in X : fˆ(x) =/= Ø} and for x in DD(f), f(x) is the
| unique element of fˆ(x). A multifunction g has the form fˆ if and only if g(x)
| has at most one element for all x. Furthermore, the compositions of (4) and
| 1.3.7 respect each other as is shown in the next result.
|
| 10. Proposition. Let f be in Pfn(X, Y), g be in Pfn(Y, Z),
| and let gf in Pfn(X, Z) be the composition of 1.3.7.
| Let gˆfˆ in Mfn(X, Z) be the composition of (4).
| Then (gf)ˆ = gˆfˆ.
|
| Proof. (gˆfˆ)(x) = {z : there exists y in fˆ(x) with z in gˆ(y)}
|
| = {z : x in DD(f) and f(x) in DD(g) and z = g(f(x))}
|
| ( {g(f(x))}, x in DD(f) and f(x) in DD(g),
| = <
| ( Ø, else.
|
| = (gf)ˆ(x). þ
|
| The import of (9), (10) is that "partial functions are multifunctions",
| that is, blurring the distinction between f and fˆ is unlikely to be
| imprecise. Usually, one writes fˆ simply as f. Thus, if f is in
| Pfn(X, Y) and g is in Mfn(Y, Z) we would write gf without comment
| for the more precise gfˆ in Mfn(X, Z). One mild warning is in
| order, however, relating to 1.3.3. If a known programming
| statement computes f we would expect to be able to write
| the statement:
|
| if fˆ(x) = Ø then g(x) else h(x)
|
| in, say, Pascal. This would compute h(x) if computation of f(x) halts,
| but would be undefined rather than returning g(x) if f(x) does not halt,
| that is, if x is not in DD(f). In short, fˆ(x) = Ø in 1.3.5 should be
| interpreted not as a returned value but as a nontermination. A similar
| interpretation applies to f(x) = Ø in (5). On the other hand, there are
| circumstances such as the "children" multifunction where Ø is a reasonable
| returned value. In a semantic environment where a possibly nonterminating
| algorithm has the empty set as a possible returned value, multifunctions
| may not provide the correct type of function. See Exercise 2.1.10.
|
| 11. Proposition. (Associative Law for Partial Function Composition).
|
| If f in Pfn(W, X),
|
| g in Pfn(X, Y),
|
| h in Pfn(Y, Z),
|
| then, with respect to the composition of 1.3.7,
|
| h(gf) = (hg)f in Pfn(W, Z).
|
| Proof. Using (6) and (10) we have:
|
| (h(gf))ˆ = hˆ(gf)ˆ = hˆ(gˆfˆ) = (hˆgˆ)fˆ = (hg)ˆfˆ = ((hg)f)ˆ,
|
| so that h(gf) = (hg)f. þ
|
| Manes & Arbib, AAPS, pages 23-24.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤