Semantics course Fall 2007

Teacher

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

Set up

The course by week

1. September 14:
   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 24:
   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. October 1:
   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 8:
   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 15:
   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
6. October 22: FALL HOLIDAY
7. October 29:
   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 5: (Ill, so moved to November 12)
   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 19:
   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 26: Ill
11. December 3:
    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.
12. December 10:
    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]
13. December 17: No lecture, because of the symposium Reflections on Type Theory, Lambda Calculus, and the Mind, celebrating Henk Barendregt's 60th birthday. Please come to the symposium!

Exam

Links

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