ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 17
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 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 begin by introducing "abbreviations" which amount to "subprograms".
|
| 17. We introduce the symbol =_abb.
|
| If f is a syntactic function then
|
| x =_abb f,
|
| read "x is an abbreviation for f", is an
| informal declaration that any occurrence
| of x may be literally replaced by the
| string f.
|
| We begin with some abbreviations which produce
| functions to manipulate lists and matrices.
|
| 18. For any function f and n >= 0,
|
| f^n is the abbreviation defined by
|
| f^0 =_abb id,
|
| f^1 =_abb f,
|
| f^n =_abb (f o ... o f), (n times for n > 1).
|
| For i >= 1 we have the following abbreviations:
|
| 19. pr_i =_abb (head o tail^(i-1)), the 'i^th projection function'.
|
| 20. col_i =_abb (!a!pr_i), the 'i^th column function'.
|
| 21. transp_n =_abb [col_1, ..., col_n], the 'n-column transpose function'.
|
| Thus, transp_3 is an abbreviation for the FPF function:
|
| [(!a!(head o id)), (!a!(head o tail)), (!a!(head o tail o tail))].
|
| The reader may easily check that pr_i: <t_1, ..., t_n> is t_i for i =< n
| but undefined for i > n, so that pr_i selects the i^th entry of a list,
| that col_i returns the i^th column of a matrix:
|
| col_i: <<a_11, ..., a_1n>, ..., <a_m1, ..., a_mn>>
|
| ( <a_1i, ..., a_mi>, (i =< n),
| = <
| ( undefined, (i > n),
|
| and that
|
| transp_n: <<a_11, ..., a_1n>, ..., <a_m1, ..., a_mn>>
|
| = <<a_11, ..., a_m1>, ..., <a_1n, ..., a_mn>>
|
| produces the transpose of an n-column matrix.
|
| Manes & Arbib, AAPS, pages 17-18.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤