# Semantics course Fall 2008

## Material

• Selected chapter(s) from Hanne Riis Nielson and Flemming Nielson: Semantics with applications, 1999 (via internet: PDF)
• My own Semantics Course Notes (via internet: PDF)
• Notes on denotational semantics of lambda calculus. (Will be distributed later.)
The first two pieces of material have an overlap, but that's only advantageous.

## Set up

The course consists of "self study" and one weekly get together Tuesday, 10.30 hr at my room HG 02.056.

## The course by week

1. September 16:
1. Study pages 85 -- 94 of Nielson and Nielson
2. Determine the denotational semantics of the program
if x>y then x:=x-y else y:=y-1
3. Make Exercises 4.2, 4.3, 4.4, 4.5 and 4.7
2. September 23:
1. Study pages 95 -- 103 until Example 4.32 of Nielson and Nielson
2. Take special care of Example 4.20, Lemma 4.25, Lemma 4.30 and Example 4.31.
3. Make Exercises 4.12, 4.14, 4.19, 4.21, 4.22, 4.27, 4.28
4. Consider the flat domain of the booleans, containing tt, ff and a bottom element.
Give all monotonic functions that sensibly represent the function "OR" on these booleans.
Discuss notions as strictness and evaluation orders for the "OR" function based on your definitions. Which function corresponds to "parallel evaluation" order?
3. September 30:
1. Study pages 103 -- 112 until 4.4 of Nielson and Nielson
2. Take special care of (the proofs of) Lemma 4.35, Theorem 4.37, Proposition 4.47. (NB Read the proof of Proposition 4.47 first and only then the Lemmas preceeding it.) Also take special care of Example 4.38.
3. Make Exercises 4.33, 4.34, 4.39, 4.40, 4.49, 4.51, 4.53 (the third)
4. October 7:
1. Study (again) pages 103 -- 112 until 4.4 of Nielson and Nielson
2. Make Exercise 4.39, the second, by proving that the following is the general form of F^n(_|_) for the F of exercise 4.3:
F^n(_|_)(s) = s[x|->1, y|-> s(y)*s(x)!] if s(x) = 1, ..., n,
F^n(_|_)(s) = undef otherwise
NB The general form might be just wrong; in that case repair it ...
3. Make Exercises 4.49, 4.51
4. Prove that, for d an element of some ccpo D, g: D -> D continuous and G, F : (D->D)->(D->D) continuous,
if d = G(FIX F) and g = F g, then d<= G g
5. Make Exercise 4.53, the third. (You have to prove a <= and a >=. Hint: First prove the >= using the previous exercise. Note added 8/10/07: There is a simple direct way of proving this.)
5. October 14: FALL HOLIDAY
6. October 21:
1. Study section 4.4 (pages 112 -- 117) of Nielson and Nielson
2. Make Exercise 4.58 and 4.59.
3. Prove that, for D some set, D -> P(D), is a ccpo (where P(D) denotes the power set of D). Of course, you first have to define an ordering on D -> P(D): extend the subset ordering on P(D) to the function space.
Show how a partial function g: D -> D can be "extended" to a total function g* : D -> P(D).
Show that the "known" ordering and lub on partial functions are preserved under this embedding of the set of partial functions into the set of functions to the power set.
4. We extend the language of while with a non-deterministic or construct: S1 or S2 non-deterministically executes S1 or S2. Modify the denotational semantics Sds to include the or statement.
Note that the interpretation of a statement is now an element of D -> P(D). Extend/change Table 4.1 (and if needed the constructions used therein) to include the or statement. (You don't have to prove the well-definedness of your new function Sds.)
5. Study the first part of the section on continuations: pages 126--129 until Exercise 4.73
7. October 28:
1. Study the rest of the section on continuations: pages 129--131
2. Prove that, for f : D1xD2 -> D3, where Di are ccpos, and X and Y subsets of D1 and D2,
lub { lub{f(x,y) | x in X} | y in Y} =lub { lub{f(x,y) | y in Y} | x in X}
assuming that all relevant lubs exist. That is: taking lubs is a commutative operation. (To do this exercise, it may be good to first cast it in the notation of the book.)
3. Make Exercise 4.73 until "Finally, one may use ..." Note that [Cont -> Cont]> is the set of continuous functions, so when defining the lub, you have to prove it is continuous.
4. Exercise 4.74 is by induction on the statement S. Verify it for all statements except for the while do construction.
5. Make Exercise 4.75, 4.77 and 4.79
8. November 4:
1. Study my own set of course notes, until section 2.5 (p.17)
2. Study the examples and exercises in these section
9. November 11:
1. Study section 2.5 of my notes
2. Study chapter 2 until Definition 2.1.12 of the "Grondslagen van de Informatica 2" notes. (To be obtained from Herman.)
3. Make the exercises
10. November 18:
1. Study section 2.2, until 2.2.3 of the "Grondslagen van de Informatica 2" notes.
2. Study section 2.7, until 2.7.5 of the "Grondslagen van de Informatica 2" notes. Omit the proof of 2.7.3.
3. CL is a syntactical lambda-algebra. (For the definition of CL, see the previous exercises.)The proof of this fact is by induction on the proof of lambda |- M =N. Do the base step of this proof: prove that (lambda x.P)Q = P[x:=Q] holds in CL (by induction on the structure of P).
4. CL is not a syntactical lambda-model. A counterexample is found by taking M to be (lambda z.z)x and N to be x. Verify this.
5. Study section 3.1. Note the difference between a cpo and a complete lattice! (NB sup = lub, inf = glb.) Note in particular 3.1.3, 3.1.9 and 3.1.18
6. Define a structure (D,<=) that is a cpo, but not a complete lattice.
7. Complete lattices have least upperbounds and therefore also greatest lower bounds of all subsets. Proposition 3.1.7 states this fact. Complete the details of the proof.
11. November 25:
1. Study sections 3.2, and 3.3 (until 3.3.4) of the "Grondslagen van de Informatica 2" notes.
2. Consider a reflexive D where also G o F is the identity on [D -> D] . Show that the eta-rule (lambda x . M x = M if x not free in M) is valid in this model.
3. For A = {0,1}, describe the sets B0 and B1
4. For A arbitrary, describe the interpretations of I, K and K* in D_A. Prove that K and K* have a different interpretation in D_A.
5. Does the eta-rule hold in D_A? That is: verify if G o F is the identity on [D_A -> D_A]
12. December 2: To be determined
13. December 9: To be determined
14. December 16: To be determined

## Exam

At some date in January, to be determied later, there will be a written exam. It is an "open book" exam, so you can bring the course notes.
Here is a set of test exercises.