Previous

[ 03.html ]

Preparation

Study chapter 3 on semantics pages 34 to 47 inclusive. Prepare some notes and at least one question you need to ask on it.

Denotational Semantics

Basics

Denotational semantics defines a set of maps that take syntactic forms and provides meanings for them. For example suppose that d is a semantic map providing meanings for binary strings:
Net
1. d<<"0">> = 0.
2. d<<"1">> = 1.
3. d<<x "0">> = 2 d<<x>> .
4. d<<x "1">> = 2 d<<x>> +1 .

(End of Net)
This is how d defines the meaning of "101":
Net
1. d<<"101">>
2. = 2 d<<"10">> + 1
3. = 2(2*d<<"1">>) + 1
4. = 2*(2*1)+1
5. = 2*2+1
6. = 4+1
7. = 5.

(End of Net)
Commonly the meaning of something is defined in terms of the meaning of its parts. For example, the meaning of "a=2*b+1;" in C/C++/Java depends on the meaning of "a" and "2*b+1", Because it is an assignment it means evaluate 2*b+1 and put the resulting value in the location of a.

Metalanguage

Symbols for Undefined and Over-defined

These special symbols are used to indicate things that have know meaning.
1. top::= symbol for something that is over defined.
2. bot::=symbol for an undefined meaning.

   Comment on chapter 3

   I'm not too happy with the definitions of domains, products and so on. I'm raiding some other books and will add my definitions to this page.

   Some books and papers use a simpler definition of domain than Scott and Strachey did. This omits the top (over-defined) element but keeps the bot element. I wrote some notes on this some years ago and put them on the web [ math_24_Domains.html ] in the mathematical part of my web site.

   Domain

   A domain is always more than a normal "set".

   A domain is created by

   Elements	defining a set of elements in it,
   Top, bottom	identifying (or adding) the top and bot of the domain.
   Order	defining an order that we interpret as "is less defined than".

   (An order must be transitive, etc...) such that top is more defined than any other element, and bot is less defined than all other elements.

   For example the domain N of numbers in the book is defined by

   Elements	All the integers including negatives and zero.
   top...	The bot and top symbols.
   Order	For all numbers n, bot is less defined than n and top is more defined than n. All numbers are equally defined: neither more or less defined than each other.

   Given a normal set S (with no top or bot)

3. S^o::= following domain,

   Elements	S
   Top...	top, bot
   Order	For all x in S, bot is less defined than x and x is less defined than top.

   Product Domains

   Figure 3.4 in the book is correct. The example of B><V on page 42 is incorrect.

   Given two domains A and B the product domain is defined by

4. A><B::=following domain

   Elements	{ (a,b). for each a:A and b:B } -- including (bot, x) for example.
   -	bot := ( A.bot, B.bot ), top := (A.top, B.top).
   Order	For a1,a2:A, b1,b2:B, (a1,b1) is less defined than (a2,b2) if and only if a1 is less defined than a2 and b1 is less defined than b2.

   Note that for sets S1 and S2, if D1=S1^o and D2=S2^o then D1><D2 is not the same as (S1 >< S2)^o.

   Where the book uses a downward pointing arrow.... most people would use a simple subscript.

   The test does not waste time distinguishing (A><B)><C from A><(B><C) because in set theory and domain theory they are isomorphic (same thing in disguise). It flattens them to (A><B><C).

   Simple Power Domains

   Taking products of a domain with itself gives us powers:
5. A^0 = {bot, (), top).
6. A^1 = A.
7. A^2 = A><A.
8. A^3 = A><A><A.
9. and so on.

   Sum Domains

   These are also called disjoint unions. The idea is to define a domain that contains a copy of one domain and a separate copy of the other --- even if they have overlapping elements.

   Given a couple of domains A and B the sum domain is defined as

10. A+B::=following domain

    Elements	{ (a,1). for a:A } | { (b,2). for b:B }.
    "	(A.bot,1), (A.top, 1), (B.bot,2), and (B.top,2) are all in this domain.
    -	Add new top and bot elements.
    Order	For a1, a2: A, (a1,1) is less defined than (a2,1) if a1 is less defined than a2.
    "	For b1, b2: B, (b1,2) is less defined than (b2,2) if b1 is less defined than b2.
    "	(a,1) and (b,2) are not less or more defined than each other.
    "	For all (x,i), bot is less defined than (x,i) and (x,i) is less defined than top.

    Infinite Sum Domains

    Now we have powers and sums we can define
11. A^*::= {()} + A + A^2 + A^3 +... and Scott and Strachey have shown that this is a meaningful "limit" ...

    Functions

    Used for modeling memory state, and many other things.

    A function (or power domain) of two domains A and B can be defined by

12. A -> B::=following domain

    Elements	{ f. for all a:A, one b:B ( f(a) = b ) }.
    -	Add bot and top as functions than map every a:A in bot and top respectively.
    Order	For f,g: A->B, f is less defined than g if for all a:A ( f(a) is less defined than g(a) ).

    Lists

    These are defined using the above function. I'd call them string operations!

    Operators on Domains

    We now have an algebra of domains with product, sum, and powers/functions.

    Injection and Projection on Sum Domains

    The book defines some useful notations/ideas for sum domains.

    The book defines projection (|)and injection (in) operators. These are just like up and down casting operations in an OO language like C++. Suppose we had a domain Number which was the sum of Int and Float domains:

13. Number = Int + Float. Then 1.234 is an element of Float, but (1.234 in Number) is an element of Number. Howver suppose we had a number x that is a Number, then it may be an Int or it may be a Float. x|Int is meaningful if x is an Int and is the value of x as an Int. Similarly with x|Float.

    A condition that make sure that an element is in a particular part of the sum: For x:D1+D2+....+D[i]+..., x E D[i]::x is in D[i].

    Changing Functions

    Functions are going to be used to model storage. We need there to be able to change their values (change the value stored in a location). The book uses a common notation f[b/a] for this.

    x	f(x)
    a	b
    else	f(x)

    I tend to misread this and so write f[a+>b] ::= f[a:=b]. f[a:=b] ::= the f' where for all x(if x=a then f'(x)=b else f'(x) = f(x)).

. . . . . . . . . ( end of section Metalanguage) <<Contents | Index>>

Simple Semantic Equations

. . . . . . . . . ( end of section Denotational Semantics) <<Contents | Index>>

Questions

Why do we need precise semantics

As programmers, compiler writers, consultants, and teachers we need to be able to answer questions about statements in programming languages. Semantics handles questions about what something in a language means. Precise semantics mean we can find out precisely what is ment by a piece of a program.

Notice we can not rely on the compiler or a vendor to define the meaning of a language. The result allows programs to suddenly start misbehaving as their meaning changes.

Trying to us ENglish in a standard has lead to langauges that are paradoxical ... the meanings contradict each other, or undefined -- we can not figure out what a staement or expressions means. Formal (mathematical and/or logical) methods have tended to provide clear answers to questions and early indicators of error in a language specification.

What is the a on line 5 of Page 44

It is an example of a character. It is an element
1. of the domain C. Since C is a subset of C* the a is also a member of C*.

   Similarly lines 3 and 4 show a member of I and of R (real).

   So each line is a member of (I+ C* + R).

   So, all three lines is a sequence in (I + C* + R)*

   Can you give examples of D1->D2 on page 44.

   A Function domain is used to model the behavior of storage.

   Suppose we have a domain of variable names Var and a domain of values Val, then storage is modelled as

2. Var -> Val. Commonly the values can be different types: bool, int, float,... and
3. Var -> (Bool + Int + Float).

   So if s:Var->(Bool+Int+FLoat) we might have

4. s(test) = true.
5. s(i) = 42.

   Another common example is modelling changes to State. Each change is a function mapping the past into the present:

6. State -> State.

   Explain the notations of Page 46.

   The in and | operators are very like casts in C++ the change the type of an expression fro the special to the general or back again.

   Explain Maps from Syntax to Semantics

   A Semantic map is a function that takes a piece of syntax and gives us the meaning of the syntax in return. For example if we had a language with a skip statement that did nothing, and Id is the identity map, then we can define a map
7. "skip" +> Id Or more formally
8. m<<skip>> = Id.

   Explain the notation on page 39.

   The key notation is like this:
9. name_of_semantic_map << piece_of_syntax >> which describes the result of applying the map to the syntax.

   Is there an error in Figure 3.5

   YES! The bot[B] symbol in the left hand side of the lattice should be \bot[L].

   Explain a Lattice.

   A lattice is a mathematical algebra based on two operators called the least upper bound (supremum) and greatest lower bound (infimum). I have got some documentation on lattices that can be found via: [ lookup.php?search=lattice ]

   Lattice are a useful way of looking at many things and have been recently used in sofware engineering. Here is a pretty example [ Programming_Languages in logic_42_Properties_of_Relation ] that describes languages and how they are related.

   On page 45 explain the notation

   The notation
10. s:S means that S is a set or domain and s is an element in the set or domain.

    In the example given

11. s: S= Operators -> ( (C><C) -> N ) we have a set of maps that take an operator like "+" and tell us how it works. The particular s can be applied to "+" and the result applied to two C's to give an N
12. s[+](4,3).

    I think the book's formula s[+(3,4)] is wrong.

. . . . . . . . . ( end of section Questions) <<Contents | Index>>

Examples

Using semantic equations to evaluate expressions. Page 41.

Semantic Equations
Net

1. (a): e<<E+T>> = e<<E>> + e<<T>>.
2. (b): e<<E-T>> = e<<E>> - e<<T>>.
3. (c): e<<T>> = a<<T>>.
4. (d): a<<T*F>>= a<<T>> * a<<F>>.
5. (e): a<<T/F>>= a<<T>> / a<<F>>.
6. (f): a<<F> = b<<F>>
7. (g): b<<(E)>> = (e<<E>>).
8. (h): b<<constant>> = some value in the integers.

(End of Net)


Determining the meaning of 3*2+1. Note, in my notation on web pages the steps in a proof are linked to the rules that were applied.
Net

1. e<<3*2+1>>
   
2. (parsing) |-
3. = e<<(3*2)+1>>
   
4. (a) |-
5. = e<<(3*2)>> + e<<1>>
   
6. (c) |-
7. = e<<(3*2)>> + a<<1>>
   
8. (f) |-
9. = e<<(3*2)>> + b<<1>>
   
10. (h) |-
11. = e<<(3*2)>> + 1
    
12. (c) |-
13. = a<<(3*2)>> +1
    
14. (f) |-
15. = b<<(3*2)>> +1
    
16. (g) |-
17. = (e<< 3*2 >> ) +1
    
18. (c) |-
19. = (a<<3*2>>) +1
    
20. (d) |-
21. = (a<<3>>*a<<2>>) +1
    
22. (f, f) |-
23. = (b<<3>>*b<<2>>) +1
    
24. (h, h) |-
25. = (3*2) +1
    
26. (arithmetic) |-
27. = 6+1
    
28. (arthmetic) |-
29. = 7.

(End of Net)


Laboratory 4

This is to review the idea of the WHILE language. Here is a working C++ program that reads a single positive non-zero number and outputs a pretty random series of numbers. [ 04.cpp ]

DON'T try to figure it out! I chose a useless program with a well known unpredictable calculation.

Your task is to remove all control structures except while loops. NO ifs, do-whiles, GOTOs, switches, ... No (_?_:_) are allowed. Assignments, conditions, expressions, input and output are ok. Your version must produce precisely the same results as the original.

Be ready to show me your code and demonstrate it before the end of the laboratory today.

Next

Study chapter 3 on semantics pages 48 to 64 inclusive. [ 05.html ]

. . . . . . . . . ( end of section CSCI620 Session 4) <<Contents | Index>>

Glossary