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?