Com S 641 --- Semantic Models of Programming Languages

   HOMEWORK 1: Posets, Lattices, Categories, and Higher-Order Logic
		 (File $Date: 2002/02/27 20:54:59 $)

Due: problems 1-6,8-11, Feb. 1, 2002; the rest on Feb. 4, 2002.

The following are exercises from chapter 2 of Back and von Wright's book.

1. (10 points) Do exercise 2.1 on p. 54 in Back and von Wright's
   book.  Note that the ordering should be written as "m <= n means
   that m divides n" (see the errata on the course web page).

2. (5 points) What's the smallest example of a poset that is a
   lattice?

3. (5 points) What's the smallest example of a poset that is not a
   lattice?

4. (10 points) Do exercise 2.2 on p. 54 in Back and von Wright's
   book.  (Show that the composition of two monotonic functions is
   monotonic.)

5. (10 points) [Exercise 2.4 on p. 55]
   Let L be the set of all cofinite sets of naturals (i.e. all sets whose
   complement is finite), ordered by set inclusion.  Show that L is a
   lattice but not a complete lattice.
   Does it have a top or a bottom element?

6. (20 points) [Exercise 2.5 on p. 55]
   Prove that Bool x Nat ordered by (==>) x (<=) is a lattice.
   Show that f: Bool x Nat -> Nat, defined by
	  f.(F,n) == 2n and f(T,n) == 2n+1
   is monotonic but not an order embedding of Bool x Nat into Nat.

7. (canceled) [Exercise 2.6 on p. 55]
   The original version of this problem reads:

      Let A be an infinite set.  Then (A -> Bool, \subseteq) is an atomic
      complete Boolean lattice.  Show that (A -> Bool) -> (A -> Bool)
      ordered by pointwise-extended set-inclusion is not atomic.

   According to the errata:
      If A is a set, and B is an atomic Boolean lattice, then (A -> B) is
      an atomic Boolean lattice, where the atoms are,
      for all a \in A, b \in B
        f_{a,b} such that f_{a,b}.y := if a == y then b else \bot fi
      (where \bot is the bottom element of B).

8. (10 points) [Exercise 2.7 on p. 55]
   Assume that f and g are bijective monotonic functions with
   f <= g.  Either show that g^{-1} <= f^{-1} or find a counter-example.
   If you find a counter-example, see if you can prove that
   g^{-1} <= f^{-1} under *one* of the following additional assumptions:

   (a) f and g are order embeddings,
   (b) f and g are join (or meet) homomorphisms,
   (c) the domain of f and g is finite, or
   (d) the domain of f and the domain of g are the same poset.
   
9. (10 points) Pick one of the implications in figure 2.6, and show
   that it is valid.

10. (10 points) [Exercise 2.10 on p. 55]
    Let A be an arbitrary set and \bot and \top two elements not in A.
    Show that A \union {\bot, \top} is a complete lattice under the ordering
       a <= b  <==> a == b \/ a == \bot \/ b == \top.
    To clarify, you can assume that \bot is distinct from \top.

11. (15 points) [Exercise 2.11 on p. 55]
    Show that the meet operation in a complete lattice has the following
    property.
      x == \meet A
          <==> (\forall y :: y <= x <==> (\forall a \in A :: y <= a))
    What is the dual characterization of join?

The following are exercises from chapter 2 of Back and von Wright's book.

12. (10 points) [Exercise 3.1 on p. 67]
    Assume that \Sigma and \Gamma are types and that c: \Sigma
    and g: \Gamma -> Bool are constants.  Deduce the types of all subterms
    of the following term: 
        (\ x : Bool . \ y . f.x.c == g.y)

13. (15 points) [Exercise 3.2 on p. 67]
    Show that the typing rules of higher-order logic rule out
    self-application of the form t.t; i.e., show that a term can never be
    applied to itself.

14. (15 points) [Exercise 3.3 on p. 67]
    We want to create a theory over a single type T with the following
    constants:
       P : T -> T -> Bool,
       A : T -> T -> Bool,
    and with the following two inference rules:

                        |- A.t.t'    |- P.t'.t''
     __________         ________________________
      |- A.t.t                 A.t.t''

   (a) Write a deduction of |- A.x.z from |- P.x.y and |- P.y.z.

   (b) Show that if there are deductions of |- A.t.t' and |- A.t'.t''
       using only the two inference rules above, then there is also a
       deduction of |- A.t.t''.

15. (20 points) Suppose you have two types, say C and P, such that you
    want to consider C to be a subtype of P.  Unfortunately, HOL
    doesn't support subtyping.  What practical problems does that
    cause?