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.)
|
| In our denotational semantics of FPF, the semantics of
| each syntactic function will be such as to transform
| inputs in !DTN! to outputs which are again in !DTN!.
| We pause briefly to note what kind of function
| constitutes such a transformation.
|
| 3. Definitions. Let X, Y be sets. A 'partial function' from X to Y is
| specified by providing a subset A of X and a function mapping each
| element of A to a unique element of Y. We say X is the 'domain',
| Y is the 'codomain', and A is the 'domain of definition'.
|
| (Other authors use "domain" for our "domain of definition".
| Our terminology follows the conventions of category theory
| as discussed in the next chapter; see Definition 2.1.1.)
|
| [A shorter name for "domain of definition" is "corange".]
|
| Our most common notation will be to assign a symbolic
| name such as 'f' to a partial function. We write
|
| f
| "let X ---> Y be a partial function"
|
| to mean f is a partial function from X to Y.
| We may also write f : X -> Y in place of
|
| f
| X ---> Y
|
| In either case, we use f(x) for the value assigned by f to
| each x in its domain of definition, which we denote by DD(f).
| If x is in X but x is not in DD(f) we say "f(x) is undefined".
|
| 4. The set of all partial functions from X to Y will be
| written Pfn(X, Y). The "partial" in partial function
| means "partially defined". Paradoxically, an important
| special case of a partial function f : X -> Y occurs
| when DD(f) = X. This is just a function from X to Y.
| For emphasis, we call such f a 'total function' from
| X to Y.
|
| 5. We relate this to program semantics in general before returning to !DTN!.
| Let X be an input set and let Y be an output set. A given algorithm
| with input x in X may fail to terminate. Let A be the subset of X
| consisting of those x for which the algorithm terminates if x is
| the input. The denotational semantics of the algorithm is the
| partial function f : X -> Y with DD(f) = A, and where f(x) is
| the output at termination when x is the input. (In 1.4.5
| below we will consider a computation environment in which
| (5) requires modification.
|
| 6. The set of all total functions from X to Y will be written Tot(X, Y).
|
| Manes & Arbib, AAPS, pages 13-14.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤