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?