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

- September 16:
- Study pages 85 -- 94 of Nielson and Nielson
- Determine the denotational semantics of the program

if x>y then x:=x-y else y:=y-1 - Make Exercises 4.2, 4.3, 4.4, 4.5 and 4.7

- September 23:
- Study pages 95 -- 103 until Example 4.32 of Nielson and Nielson
- Take special care of Example 4.20, Lemma 4.25, Lemma 4.30 and Example 4.31.
- Make Exercises 4.12, 4.14, 4.19, 4.21, 4.22, 4.27, 4.28
- 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?

- September 30:
- Study pages 103 -- 112 until 4.4 of Nielson and Nielson
- 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.
- Make Exercises 4.33, 4.34, 4.39, 4.40, 4.49, 4.51, 4.53 (the third)

- October 7:
- Study (again) pages 103 -- 112 until 4.4 of Nielson and Nielson
- 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 ... - Make Exercises 4.49, 4.51
- 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* - 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.)

- October 14: FALL HOLIDAY
- October 21:
- Study section 4.4 (pages 112 -- 117) of Nielson and Nielson
- Make Exercise 4.58 and 4.59.
- 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. - 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*.) - Study the first part of the section on continuations: pages 126--129 until Exercise 4.73

- October 28:
- Study the rest of the section on continuations: pages 129--131
- 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.) - 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. - Exercise 4.74 is by induction on the statement
*S*. Verify it for all statements except for the*while do*construction. - Make Exercise 4.75, 4.77 and 4.79

- November 4:
- Study my own set of course notes, until section 2.5 (p.17)
- Study the examples and exercises in these section

- November 11:
- November 18:
- Study section 2.2, until 2.2.3 of the "Grondslagen van de Informatica 2" notes.
- Study section 2.7, until 2.7.5 of the "Grondslagen van de Informatica 2" notes. Omit the proof of 2.7.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*). - 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. - 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
- Define a structure
*(D,<=)*that is a cpo, but not a complete lattice. - 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.

- November 25:
- Study sections 3.2, and 3.3 (until 3.3.4) of the "Grondslagen van de Informatica 2" notes.
- 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. - For
*A = {0,1}*, describe the sets*B0*and*B1* - 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*. - Does the eta-rule hold in
*D_A*? That is: verify if*G o F*is the identity on*[D_A -> D_A]*

- December 2: To be determined
- December 9: To be determined
- December 16: To be determined

Here is a set of test exercises.

- For those interested in a course on Domain theory, there is a course taught by Mai Gehrke.

herman at cs dot ru dot nl Last modified: Fri Jan 18 15:19:33 CET 2008