[Index] [Schedule] [Syllabi] [Text] [Labs] [Projects] [Resources] [Search] [Grading]

Tue Apr 13 17:53:42 PDT 2004

- CSCI620 Session 4
- : Previous
- : Preparation
- : Denotational Semantics
- : : Basics
- : : Metalanguage
- : : : Symbols for Undefined and Over-defined
- : : : Comment on chapter 3
- : : : Domain
- : : : Product Domains
- : : : Simple Power Domains
- : : : Sum Domains
- : : : Infinite Sum Domains
- : : : Functions
- : : : Lists
- : : : Operators on Domains
- : : : Injection and Projection on Sum Domains
- : : : Changing Functions
- : : Simple Semantic Equations
- : Questions
- : : Why do we need precise semantics
- : : What is the a on line 5 of Page 44
- : : Can you give examples of D1->D2 on page 44.
- : : Explain the notations of Page 46.
- : : Explain Maps from Syntax to Semantics
- : : Explain the notation on page 39.
- : : Is there an error in Figure 3.5
- : : Explain a Lattice.
- : : On page 45 explain the notation
- : Examples
- : Laboratory 4
- : Next
- Glossary
- Index of defined terms etc.

- d<<"0">> = 0.
- d<<"1">> = 1.
- d<<x "0">> = 2 d<<x>> .
- d<<x "1">> = 2 d<<x>> +1 .
- d<<"101">>
- = 2 d<<"10">> + 1
- = 2(2*d<<"1">>) + 1
- = 2*(2*1)+1
- = 2*2+1
- = 4+1
- = 5.
- top::=
*symbol for something that is over defined*. - 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

(An order must be transitive, etc...) such thatElements 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". *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 byElements 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. - 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

- A><B::=following domain

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.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. 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: - A^0 = {
*bot*, (),*top*). - A^1 = A.
- A^2 = A><A.
- A^3 = A><A><A.
- 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

- 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 - 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

- 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: - 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.

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)).x f(x) a b else f(x) - 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 - Var -> Val. Commonly the values can be different types: bool, int, float,... and
- Var -> (Bool + Int + Float).
So if s:Var->(Bool+Int+FLoat) we might have

- s(test) = true.
- s(i) = 42.
Another common example is modelling changes to State. Each change is a function mapping the past into the present:

- 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 - "skip" +> Id Or more formally
- m<<skip>> = Id.
### Explain the notation on page 39.

The key notation is like this: - 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 - s:S
means that
*S*is a set or domain and*s*is an element in the set or domain.In the example given

- 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
- s[+](4,3).
I think the book's formula s[+(3,4)] is wrong.

- e<<3*2+1>>
- (parsing) |-
- = e<<(3*2)+1>>
- (a) |-
- = e<<(3*2)>> + e<<1>>
- (c) |-
- = e<<(3*2)>> + a<<1>>
- (f) |-
- = e<<(3*2)>> + b<<1>>
- (h) |-
- = e<<(3*2)>> + 1
- (c) |-
- = a<<(3*2)>> +1
- (f) |-
- = b<<(3*2)>> +1
- (g) |-
- = (e<< 3*2 >> ) +1
- (c) |-
- = (a<<3*2>>) +1
- (d) |-
- = (a<<3>>*a<<2>>) +1
- (f, f) |-
- = (b<<3>>*b<<2>>) +1
- (h, h) |-
- = (3*2) +1
- (arithmetic) |-
- = 6+1
- (arthmetic) |-
- = 7.
- BNF::="Backus-Naur Form", for syntax and grammar, developed by Backus and Naur.
- EBNF::="Extended "
*BNF*. - HTML::= "HyperText Markup Language", used on the
*WWW*. - HTML_page::syntax= "<HTML>" head body.
- Java::="An "
*OO*" Language from Sun". - LISP::= "LISt Processing Language".
- LRM::="Language Reference Manual".
- OO::="Object-Oriented".
- Prolog::="Programming in Logic".
- TBA::="To Be Announced".
- UML::="Unified Modeling Language".
- URL::=Universal_Resource_Locator,
- Universal_Resource_Locator::syntax=
*protocol*":"*location*, where

Net

(End of Net)

- WWW::= See http://www.csci.csusb.edu/dick/cs620/, index to web site for this class.
- XBNF::="eXtreme"
*BNF*, developed by the teacher from*EBNF*, designed to ASCII input of syntax, semantics, and other formal specifications.

Net

(End of Net)

This is how

Net

(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

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

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

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.

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

Semantic Equations

Net

(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

(End of Net)

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.

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

- a (Formula)
- A+B (Definition)
- A><B (Definition)
- b (Formula)
- BNF (Definition)
- bot (Definition)
- c (Formula)
- d (Formula)
- EBNF (Definition)
- e (Formula)
- f (Formula)
- g (Formula)
- h (Formula)
- HTML (Definition)
- HTML_page (Declaration)
- Java (Definition)
- LISP (Definition)
- location (Definition)
- LRM (Definition)
- OO (Definition)
- Prolog (Definition)
- protocol (Definition)
- TBA (Definition)
- top (Definition)
- UML (Definition)
- Universal_Resource_Locator (Declaration)
- URL (Definition)
- WWW (Definition)
- XBNF (Definition)