ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 19
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 1. An Introduction to Denotational Semantics
|
| 1.4. Multifunctions (cont.)
|
| Multifunctions are suitable input/output functions for the
| following parallel computation scenario which generalizes
| that of 1.3.5.
|
| 5. Let X be an input set and let Y be an output set. Beginning with
| an input x in X, a given algorithm simultaneously initiates a set
| of noninteracting computations. Some of these may not terminate
| and those that do may halt at different times. The denotational
| semantics of the algorithm is the multifunction f in Mfn(X, Y)
| which assigns to x the set f(x) of all outputs in Y resulting
| from some terminating computation initiated by input x.
|
| One might, for example, add atomic multifunctions to the functional programming
| fragment of Section 1.3 and give a multifunction denotational semantics based
| on (5) rather than 1.3.3. See Exercise 3. In such a situation we would need
| a multifunction semantics for the FPF (f_k o ... o f_1). Similarly, in
| attempting a multifunction semantics for Pascal we would need to assign
| a meaning to "begin f_1; ...; f_k end". While the composition operation
| of (4) is the natural candidate, a technical issue is raised. Up to now
| we have viewed the chaining together of, say, three functions in the
| following way:
|
| o---------o o---------o o---------o
| ---->| f |--->| g |--->| h |---->
| o---------o o---------o o---------o
|
| For multifunctions, should this mean h(gf) or (hg)f?
| Fortunately, it makes no difference.
|
| 6. Proposition. (Associative Law for Multifunction Composition).
|
| If f in Mfn(W, X),
|
| g in Mfn(X, Y),
|
| h in Mfn(Y, Z),
|
| then h(gf) = (hg)f in Mfn(W, Z).
|
| Proof. Let z be in (h(gf))(w). Then there exists y in (gf)(w)
| with z in h(y). But then there exists x in f(w) with y in g(x).
| By the definition of hg, z is in (hg)(x) and so z in ((hg)f)(w).
| So far, we have shown that (h(gf))(w) is a subset of ((hg)f)(w)
| for all w in W. To complete the proof, let z be in ((hg)f)(w)
| and show z is in (h(gf))(w). There exists x in f(w) with z in
| (hg)(x). Thus, there exists y in g(x) with z in h(y). By the
| definition of gf, y is in (gf)(w) and then z in (h(gf))(w). þ
|
| Theorem 6 allows us to write the equal multifunctions
| h(gf) and (hg)f simply as hgf. In fact, the proof
| has shown:
|
| 7. (hgf)(w)
|
| = {z in Z : there exists x in f(w) and then y in g(x) with z in h(y)}.
|
| Repeated use of the associative law guarantees that
| parentheses can be avoided for chains of all lengths.
|
| Manes & Arbib, AAPS, pages 22-23.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤