ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 26
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 1. An Introduction to Denotational Semantics
|
| 1.5. A Preview of Partially Additive Semantics (cont.)
|
| A useful result about the existence of sums is the following:
|
| 18. Proposition. Let (f_i : i in I) be a summable family in Pfn(X, Y).
|
| Then:
|
| a. If J c I,
|
| then (f_i : i in J) is summable in Pfn(X, Y).
|
| b. If (g_i : i in I) is a similarly indexed family
| (not necessarily summable) in Pfn(Y, Z),
|
| then (g_i f_i : i in I) is a summable family in Pfn(X, Z).
|
| Proof. That (a) holds is obvious. For (b), if x is in
| DD(g_i f_i) |^| DD(g_j f_j) then x is in DD(f_i) |^| DD(f_j),
| so i = j. þ
|
| In the balance of this section we emphasize the
| use of sums to define programming constructs.
|
| 19. Definition. If A is a subset of X,
| the 'inclusion function' of A is
| inc_A in Pfn(X, X) defined by:
|
| DD(inc_A) = A,
|
| inc_A (x) = x.
|
| Thus, inc_Ø = 0 is the everywhere undefined function X -> X and inc_X = id_X.
| As usual, we consider inc_A in Mfn(X, X) as well, as in 1.4.9-10.
|
| 20. Definition. If p in Pfn(X, X) is an inclusion function (so that
| p = inc_A for A = DD(p)) we say p is a 'guard function', and for f
| in SC(X, Y) we introduce the notation p -> f for fp. The meaning of
| p -> f is "if p is true then execute f else the result is undefined",
| where to say p(x) is true means x in DD(p). Thus p "guards" entry to f.
| Such p -> f is called a 'guarded command'.
|
| Manes & Arbib, AAPS, pages 31-32.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤