Com S 641 --- Semantic Models of Programming Languages

			HOMEWORK 2: Functions
		 (File $Date: 2002/03/10 06:02:05 $)

Due: Feb. 13, 2002.

The following are exercises from chapter 4 of Back and von Wright's book.
Please use the proof format described in chapter 4 for all of your
proofs, and do the proofs formally.  You may find it helpful to do
such proofs on the computer. 

1. (10 points) [4.2]
   Derive the rules for operator and operand congruence
   from the rule for replacing equals by equals.

2. (10 points) [4.4]
   Derive the rule of the eta-conversion using other rules given in
   this chapter.

3. (10 points) [4.6]
   Derive the inference rules given for the let construct.

4. (10 points) [4.7]
   We define the constant "twice" by
          ^
    twice = (\ f x . f.(f.x))

  (a) What is the type of twice?
  (b) Simplify (twice o twice).(\ x . x + 2).3
      (note that this is not a case of self-application).

5. (10 points) [4.8b]
   Define three constants (known as combinators) as follows:
              ^
          I.x = x
              ^
      S.f.g.x = f.x.(g.x)
              ^
        K.x.y = x

   Prove that I == S.K.K

6. (15 points) [4.9]
   Assume that T is a type and that e: T, inv: T -> T,
   and +: T -> T -> T (infix) are constants satisfying the following
   rules:

    _____________________________     (+ associative)
    |- s + (t + u) == (s + t) + u

    _____________                     (+ right identity)
    |- s + e == s

    ________________                  (+ inverse)
    |- s + inv.s == e

    Phi |- s + t == e
    _________________                 (opposites)
    Phi |- t == inv.s

    Prove |- inv.(s + t) == inv.t + inv.s by a derivation.

    Don't assume that + is commutative!