ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 25
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 1. An Introduction to Denotational Semantics
|
| 1.5. A Preview of Partially Additive Semantics (cont.)
|
| We turn to some properties of sum, beginning with the following one.
|
| 15. Proposition. (Distributive Law of Composition over Sums in Mfn).
| Let f be in Mfn(W, X), let (g_i : i in I) be a family in Mfn(X, Y),
| and let h be in Mfn(Y, Z). Then:
|
| 1. (Sum g_i)f = Sum(g_i f) in Mfn(W, Y).
|
| 2. h(Sum g_i) = Sum(h g_i) in Mfn(X, Z).
|
| Proof.
|
| 1. y in ((Sum g_i)f)(w)
|
| <=> there exists x in f(w) with y in (Sum g_i)(x)
|
| <=> there exists x in X, i in I, with x in f(w) and y in g_i (x)
|
| <=> there exists i in I with y in (g_i f)(w)
|
| <=> y in (Sum(g_i f))(w).
|
| 2. z in (h(Sum g_i))(x)
|
| <=> there exists y in (Sum g_i)(x) with z in h(y)
|
| <=> there exists i in I, y in g_i (x), with z in h(y)
|
| <=> there exists i in I with z in (h g_i)(x)
|
| <=> z in (Sum(h g_i))(x).
|
| þ
|
| 16. Corollary. (Distributive Law of Composition over Sums in Pfn).
| Let f be in Pfn(W, X), let (g_i : i in I) be a summable family
| in Pfn(X, Y), and let h be in Pfn(Y, Z). Then (g_i f : i in I)
| and (h g_i : i in I) are summable, and:
|
| 1. (Sum g_i)f = Sum(g_i f) in Pfn(W, Y).
|
| 2. h(Sum g_i) = Sum(h g_i) in Pfn(X, Z).
|
| Proof.
|
| 1. If w in DD(g_i f) |^| DD(g_j f) then f(w) in DD(g_i) |^| DD(g_j), so i = j.
|
| 2. If x in DD(h g_i) |^| DD(h g_j) then x in DD(g_i) |^| DD(g_j), so i = j.
|
| Then equality of the sums follows from (15) in view (12). þ
|
| Proposition 15 and Corollary 16 ae valid when I is empty, yielding the following:
|
| 17. For f in SC(X, Y) and for all sets W, Z we have the commutative diagram:
|
| 0
| W o---------->o X
| \ |\
| \ | \
| \ | \
| \ | \
| \ f | \
| 0 \ | \ 0
| \ | \
| \ | \
| \ | \
| \ | \
| vv v
| Y o---------->o Z
| 0
|
| where the four 0's are the appropriate empty sums of (14).
| It follows that any composition f_n ... f_1 is 0
| if any of the f_i is 0.
|
| Manes & Arbib, AAPS, pages 30-31.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤