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.)
|
| We will give a denotational semantics for FPF. We begin by discussing !DTN!,
| whose inductive definition is given in Table 1, which is the set of DTN's,
| that is, 'dynamic trees of numerals' (note the different typeface for the
| set and for the generic name of elements of the set). This set includes
| lists of numerals, namely, the DTN's of form <n_1, ..., n_k>, where n_i
| are numerals. The case k = 0 gives the 'empty list' < > as a DTN.
| Similarly, we can have a list of lists such as <<5, 17>, < >, <035>>,
| the list whose first entry is the list <5, 17>, whose second entry is
| the empty list, and whose third entry is the length-1 list consisting
| of the numeral 035. Other examples are less homogeneous, for example,
| <05, << >>, <2, 3>>. An m x n matrix of numerals (a_ij), usually
| visualized as a retangular array with the numeral a_ij in row i
| and column j, may conveniently be coded as the DTN:
|
| 2. <<a_11, ..., a_1n>, ..., <a_m1, ..., a_mn>>.
|
| The input to a matrix multiplication algorithm may then be coded as
| a length-2 list whose entries are matrices as in (2). These examples
| suggest the ease with which DTN's model complex inputs and outputs.
|
| Each DTN has a unique 'derivation tree' describing how to build it
| using the basis and inductive steps in the definition of !DTN! of
| Table 1. For example, <1, <<0, 10>, < >>> has derivation tree
|
| 0 01
| o o
| \ /
| o o
| 1 \ /
| o o
| \ /
| @
|
| where each node [= @ or o] indicates a list whose entries are the
| subtrees branching from that node (read in left-to-right order).
| A node without branches thus indicates the empty list. The node
| at the root [= @] of the tree indicates the lists represented by
| the whole tree. It is clear that such derivation trees are in
| natural one-to-one correspondence with the elements of !DTN!
| and, indeed, that the list notation is just a convenient
| way to code such a tree as a string. This explains the
| term dynamic 'tree' of numerals. "Dynamic" is in the
| same sense as in the term "dynamic array" in Pascal,
| meaning that the lengths and shapes of DTN's are
| not prespecified in a "declaration".
|
| Manes & Arbib, AAPS, pages 12-13.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
Nota Bene. The way I remember it, computicians initially fell into
the habit of drawing their trees upside down, not because they were
more enamored of genealogists than of botanists in their phyllogeny,
but because of a need to print trees out on the old teletypewriters,
which scrolled the papyrus inexorably upward with neither piety nor
wit in their more than purely symbolic denaturing of nature. But I,
having been raised in a school of graph theory that accords its due
respect to the light of nature, am compelled to take liberties with
the authors' rendering of trees, and to reset their matters upright.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤