ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| Algebraic Approaches to Program Semantics
|
| Part 1. Denotational Semantics of Control
|
| Chapter 1. An Introduction to Denotational Semantics
|
|
| 1.3. A Functional Programming Fragment (cont.)
|
| If f in Pfn(X, Y), g in Pfn(Y, Z) arise as in (5) we may
| think of f, g as the computations of subalgorithms which
| can be chained together setting the output of f as the
| input of g to produce a net output in Z from an input
| in X. The formal operation involved is as follows.
|
| 7. Definition. For f in Pfn(X, Y) and g in Pfn(Y, Z)
| their 'composition' gf in Pfn(X, Z) is defined by:
|
| DD(gf) = {x in X : x in DD(f) and f(x) in DD(g)},
|
| (gf)(x) = g(f(x)) for x in DD(gf).
|
| Note that gf is total when f and g are.
|
| The functions studied in first-semester calculus are
| partial functions from the set of reals to itself (e.g.,
| DD(1/x) = {x : x =/= 0}, DD(arcsin x) = {x : -1 =< x =< 1},
| etc.). The "chain rule" refers to the composition of (7),
| being a rule for the derivative of gf. Composition of
| functions is sometimes called "chaining" because the
| output of one function is the input to the next,
| creating a chain of two links. Longer chains
| arise in (12) below.
|
| Manes & Arbib, AAPS, page 14.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤