ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 15
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 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 turn now to the semantics for FPF by associating a partial function
| in Pfn(!DTN!, !DTN!) to each syntactic function. To keep the notation
| as simple as possible we will denote the semantics of the function f
| by f: and so we will write f: t for the value f: assigns to the DTN t.
| Thus, the presence of the colon (which is not in the alphabet of
| Table 1) indicates semantics.
|
| In describing a specific partial function f, if a formula for
| f: t is given for t of a particular form without further comment
| our convention is that f: is not defined for other t. Sometimes,
| of course, DD(f) is sufficiently complicated for a more careful
| description to be necessary.
|
| We begin with the basis-step functions in Table 1.
|
| 8. id: is the identity function,
|
| id: t = t for all t in !DTN!.
|
| head returns the first element of a list and
| tail drops the first element of a list as follows:
|
| head: <t_1, ..., t_k> = t_1 (k >= 1),
|
| tail: <t_1, ..., t_k> = <t_2, ..., t_k> (k >= 1).
|
| Thus, we cannot makes heads or tails of the empty list or numerals.
|
| 9. The arithmetic functions +, -, *, ÷ require an input of the form <m, n>
| where m, n are numerals. The meaning of the operations is then the same
| as in Pascal as described in 1.2.5. Thus,
|
| +: <m, n> = m + n
|
| -: <m, n> = m -°- n
|
| *: <m, n> = m · n
|
| ÷: <m, n> = m div n
|
| where, on the right-hand sides, the numerals m, n represent numbers
| in the usual base-10 way and the numerical results are represented
| as numerals without leading zeros.
|
| 10. The 'numeral' function num is defined by
|
| ( << >> if t is a numeral,
| num: t = <
| ( < > else.
|
| Similarly, the 'equality' function = takes an input of
| the form <t, u> where t, u in !DTN! are arbitrary and
|
| ( << >> if t = u,
| =: <t, u> is <
| ( < > if t =/= u.
|
| Here we have coded the truth values as DTN's by representing
| T as << >> and F as < >. This is analogous to the trick used
| in set theory (mathematicians sometimes adopt the view that
| all of mathematics may be derived from set theory) to define
| natural numbers in terms of sets, wherein 0 is defined as
| the empty set Ø, 1 is defined as the one-element set {Ø},
| 2 is defined as the two-element set {0, 1} = {Ø, {Ø}},
| and n = {0, ..., n-1} in general. Using lists instead of
| sets, that is, by substituting < for { and > for }, the same
| constructions are available in !DTN!. We could have used the
| numerals 0 and 1 for F and T but it seemed more desirable to
| use a convention that would apply to dynamic trees of objects
| other than numerals. In fact, our convention is analogous to
| that used in the programming language Lisp, where the empty
| list Nil is used for the truth value F and where any other
| values may be interpreted as T.
|
| Manes & Arbib, AAPS, pages 14-15.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Program Semantics
01. http://suo.ieee.org/ontology/msg03884.html
02. http://suo.ieee.org/ontology/msg03885.html
03. http://suo.ieee.org/ontology/msg03886.html
04. http://suo.ieee.org/ontology/msg03887.html
05. http://suo.ieee.org/ontology/msg03890.html
06. http://suo.ieee.org/ontology/msg03895.html
07. http://suo.ieee.org/ontology/msg03896.html
08. http://suo.ieee.org/ontology/msg03898.html
09. http://suo.ieee.org/ontology/msg03904.html
10. http://suo.ieee.org/ontology/msg03905.html
11. http://suo.ieee.org/ontology/msg03906.html
12. http://suo.ieee.org/ontology/msg03909.html
13. http://suo.ieee.org/ontology/msg03910.html
14. http://suo.ieee.org/ontology/msg03911.html
15. http://suo.ieee.org/ontology/msg03912.html
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤