ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 16
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 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.)
|
| We now provide the semantics for the basis step
| in the set of functions defined in Table 1.
|
| 11. For each DTN t, !=!t:
| is the total function
| which is constantly t,
| that is,
|
| !=!t: u is t for any DTN u.
|
| To continue our description of the semantics of FPF
| we examine the constructions of the inductive step
| for the functions in Table 1.
|
| 12. If f_1, ..., f_k are functions (k >= 1), (f_k o ... o f_1):
| is the k-fold composition of (7), being essentially the same
| as the pseudo-Pascal f_1; ...; f_k, that is,
|
| (f_k o ... o f_1): t = f_k: (f_k-1: (... (f_2: (f_1: t) ...))).
|
| (Such is defined, of course, only when all the intermediate steps are defined.)
|
| The next construction applies k functions in parallel and combines the results
| in a single list.
|
| 13. If f_1, ..., f_k are functions (k >= 1),
|
| then
|
| DD([f_1, ..., f_k]) = DD(f_1) |^| ... |^| DD(f_k)
|
| and
|
| [f_1, ..., f_k]: t = <f_1: t, ..., f_k: t>.
|
| This construction is a major tool in building lists.
|
| 14. For p, f, g functions,
|
| ( f: t (p: t =/= < >),
| (if p then f else g): t is < g: t (p: t = < >),
| ( undefined (p: t undefined).
|
| Thus, our device for viewing function p as a test is to consider
| p: t false if it is our coding < > for false, true if it is defined
| but not false, and undefined else. The notation above is understood
| to mean that (if p then f else g): t is undefined if p: t = < > but
| g: t is undefined, or if p: t is defined and =/= < > but f: t is
| undefined.
|
| 15. The symbol !a! is the 'apply-to-all operator'. If f is a function,
| (!a!f): is "f applied to all entries in the input list". Specifically,
| an input to (!a!f): must have the form <t_1, ..., t_k> with k >= 1, and
| each t_i in DD(f), and then
|
| (!a!f): <t_1, ..., t_k> = <f: t_1, ..., f: t_k>.
|
| 16. The symbol / is the 'insertion operator'.
|
| If f is a function then (/f): <t_1, t_2, t_3>, for example,
| will be defined as f: <t_1, f: <t_2, t_3>>. Equivalently,
| using infix notation t f u instead of f: <t, u>, we have:
|
| (/f): <t_1, t_2, t_3> = t_1 f (t_2 f t_3).
|
| Similarly,
|
| (/f): <t_1, t_2, t_3, t_4> = t_1 f (t_2 f (t_3 f t_4)).
|
| Thus, / treats f as a function of two variables and
| extends it to a function on any number of variables
| by "inserting" it between the variables.
|
| The formal definition is as follows. The input must
| have the form <t_1, ..., t_k>, (k >= 0), that is, it
| cannot be a numeral. We use induction on k.
|
| (/f): < > = < >,
|
| (/f): <t_1> = t_1,
|
| (/f): <t_1, ..., t_k+1> = f: <t_1, (/f): <t_2, ..., t_k+1>>.
|
| This completes the description of the syntax and semantics of FPF.
| Since the reader may have had very little prior experience with
| functional languages, we will write some FPF functions to
| illustrate some of the concepts. Additional examples
| using recursion will be given in Section 5.1, but
| we shall be able to achieve quite a bit without
| any repetitive constructs. Indeed, it is
| possible to write an FPF function to
| multiply two square matrices and
| this is done in (26) below.
|
| Manes & Arbib, AAPS, pages 15-17.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤