Solutions to Problem Set 3
==========================

Written by Paul Hudak in literate Haskell style
September 28, 2004

> module PS3 where
> import Region


1.  Exercise 7.2 in SOE

"Using this definition of trees:

> data InternalTree a = ILeaf 
>                    | IBranch a (InternalTree a) (InternalTree a)
>   deriving Show

define functions:

takeTree      :: Int -> InternalTree a -> InternalTree a
takeTreeWhile :: (a -> Bool) -> InternalTree a -> InternalTree a

takeTree returns the first n levels in a tree.  For example, if:

t = let t' = IBranch 1 ILeaf ILeaf
    in Branch 2 t' t'

then takeTree 0 t ===> ILeaf and takeTree 1 t ===> IBranch 2 ILeaf ILeaf.
takeTreeWhile should behave analogously."

Solution:

> takeTree :: Int -> InternalTree a -> InternalTree a
> takeTree n t | n<=0 = ILeaf
> takeTree n ILeaf    = ILeaf
> takeTree n (IBranch x t1 t2) =
>          IBranch x (takeTree (n-1) t1) (takeTree (n-1) t2)
> 
> takeTreeWhile :: (a -> Bool) -> InternalTree a -> InternalTree a
> takeTreeWhile p ILeaf = ILeaf
> takeTreeWhile p (IBranch x t1 t2) =
>          if p x then ILeaf
>                 else IBranch x (takeTreeWhile p t1)
>                                (takeTreeWhile p t2)


2. Define a fold function (call it foldExpr) for the Expr data type.  
Then define evaluate in terms of foldExpr.

Solution:

First recall:

> data Expr = C Float | Expr :+ Expr | Expr :- Expr
>          | Expr :* Expr | Expr :/ Expr

We need to "replace" each constructor with something else; so:

> foldExpr :: (Float->a) -> (a->a->a) -> (a->a->a) -> 
>                           (a->a->a) -> (a->a->a) -> Expr -> a
> foldExpr cf plusf minusf timesf divf expr =
>   let recurse = foldExpr cf plusf minusf timesf divf 
>   in case expr of
>        C x      -> cf x
>        e1 :+ e2 -> plusf  (recurse e1) (recurse e2)
>        e1 :- e2 -> minusf (recurse e1) (recurse e2)
>        e1 :* e2 -> timesf (recurse e1) (recurse e2)
>        e1 :/ e2 -> divf   (recurse e1) (recurse e2)

With this, "evaluate" is trivial to define:

> evaluate :: Expr -> Float
> evaluate = foldExpr id (+) (-) (*) (/)

But to show that foldExpr is more generally useful, here is a function
that counts the number of terms in an expression:

> countTerms :: Expr -> Int
> countTerms = foldExpr (const 1) inc inc inc inc
>   where inc c1 c2 = 1 + c1 + c2

and one that measures the depth of an expression:

> depthExpr :: Expr -> Int
> depthExpr = foldExpr (const 0) mx mx mx mx
>   where mx d1 d2 = 1 + max d1 d2


3.  Exercise 7.5 in SOE, using the result of the above exercise.

"Enhance the Expr data type with variables and let expressions,
similar in intent to Haskell's variables and let expressions, although
you may assume that the let expression does not allow recursive
definitions.  Also enhance the evaluate function to yield the proper
value.  For example:

evaluate (Let "x" (C 5) (V "x" :+ V "x"))  ===>  10

where Let and V are the new constructors in the Expr data type.
Unbound variables should be treated as errors."

Solution:

The new Expr2 and foldExpr2 definitions are straightforward:

> data Expr2 = C2 Float | Expr2 :+: Expr2 | Expr2 :-: Expr2
>            | Expr2 :*: Expr2 | Expr2 :/: Expr2
>            | Var String | Let String Expr2 Expr2
>
> foldExpr2 :: (Float->a) -> (a->a->a) -> (a->a->a) -> 
>                            (a->a->a) -> (a->a->a) ->
>                            (String->a) -> (String->a->a->a)
>                         -> Expr2 -> a
> foldExpr2 cf plusf minusf timesf divf varf letf expr =
>   let recurse = foldExpr2 cf plusf minusf timesf divf varf letf
>   in case expr of
>        C2 x         -> cf x
>        e1 :+: e2    -> plusf  (recurse e1) (recurse e2)
>        e1 :-: e2    -> minusf (recurse e1) (recurse e2)
>        e1 :*: e2    -> timesf (recurse e1) (recurse e2)
>        e1 :/: e2    -> divf   (recurse e1) (recurse e2)
>        Var s        -> varf s
>        Let s e1 e2  -> letf s (recurse e1) (recurse e2)

The new evaluator must deal with environments, which we represent as
functions:

> type Env = String -> Float

The initial environment has no bindings, and thus maps everything to
error:

> env0 :: Env
> env0 s = error ("undefined variable: " ++ s)

Adding a binding to an environment is easy:

> extend env s x = \s' -> if s==s' then x else env s'

Now for the evaluator.  The key point is that the "meaning" of an
expression should be a FUNCTION of type Env -> Float.  For example,
consider the expression e1 :+: e2.  Let's say the meanings of e1 and
e2 are f1 and f2, respectively.  Then the meaning of e1 :+: e2 is:

\env -> f1 env + f2 env

Similarly, the meaning of C2 42 should be \env -> 42.  The only tricky
cases are Var and Let.  The meaning of Var s should be:

\env -> env s

and the meaning of Let s e1 e2 should be:

\env -> f2 (extend env s (f1 env))

where f1 and f2 are the meanings of e1 and e2, respectively.

Putting it all together, and using foldExpr2 to make things concise,
we have:

> evaluate2 :: Expr2 -> Float
> evaluate2 e = foldExpr2 (\x env -> x)
>                 (lift2 (+)) (lift2 (-)) (lift2 (*)) (lift2 (/))
>                 varf letf
>                 e
>                 env0
>    where varf s       = \env -> env s
>          letf s f1 f2 = \env -> f2 (extend env s (f1 env))
> 
> lift2 op f1 f2 env = f1 env `op` f2 env

Note the use of lift2 to deal with arithmetic in a concise way.


4. Exercise 8.3 in SOE.

"Define a function annulus :: Radius -> Radius -> Region which creates
an annulus, or ``donut,'' whose inner radius is the first argument,
and outer is the second."

Solution:

> annulus :: Radius -> Radius -> Region 
> annulus r1 r2 =
>   let c1 = Shape (Ellipse r1 r1)
>       c2 = Shape (Ellipse r2 r2)
>   in Complement c1 `Intersect` c2


5.  Exercise 8.6 in SOE.

"Assume that there is a HalfPlane constructor as described in the
previous exercise.  Assume also that there is no Polygon constructor.
Instead, define a function polygon that realizes convex polygons in
terms of HalfPlane (and possibly other constructors)."

Solution:

> polygon :: [Coordinate] -> Region
> polygon pts =
>   let hps = zipWith halfplane pts (tail pts ++ [head pts])
>   in foldl Intersect univ hps
>
> halfplane :: Coordinate -> Coordinate -> Region
> halfplane = undefined
>
> univ = Complement Empty


6.  Exercise 8.8 in SOE.

"Complete the proofs of the five axioms for regions."

Solution:

Axiom 3:  Union and Itersection are distributive.  That is, for
any r1, r2, and r3:

r1 `Intersect` (r2 `Union` r3)
=== (r1 `Intersect` r2) `Union` (r1 `Intersect` r3)

r1 `Union` (r2 `Intersect` r3)
=== (r1 `Union` r2) `Intersect` (r1 `Union` r3)

Proof (for Intersect):

(r1 `Intersect` (r2 `Union` r3)) `containsR` p
==> r1 `containsR` p && ( (r2 `Union` r3) `containsR` p )
==> r1 `containsR` p && r2 `containsR` p || 
    r1 `containsR` p && r3 `containsR` p 
==> (r1 `Intersect` r2) `containsR p ||
    (r1 `Intersect` r3) `containsR p
==> (r1 `Intersect` r2) `Union` (r1 `Intersect` r3) `containsR p

The proof for Union is very similar, and thus omitted.

Axiom 4: For any r:

r `Union`    Empty === r
r `Intersect` univ === r

Proof:

(r `Union` Empty) `containsR` p
==> r `containsR` p  ||  Empty `containsR` p
==> r `containsR` p  ||  False
==> r `containsR` p

The proof for Intersect is very similar, and thus omitted.

Axiom 5: For any r:

r `Union` Complement r     === univ
r `Intersect` Complement r === Empty

Proof:

(r `Union` Complement r) `containsR` p
==> r `containsR` p  ||  Complement r `containsR` p
==> r `containsR` p  ||  not (r `containsR` p)
==> True
==> not False
==> not (Empty `containsR` p)
==> Complement Empty `containsR` p
==> univ `containsR` p

The proof for Intersect is very similar, and thus omitted.


7.  Exercise 8.9 in SOE, but only for the 1st, 3rd, 5th, and 10th theorems.

"The axioms for regions provide a basis from which theorems can be
proved.  Prove the following theorems using only the axioms (i.e. do
not unfold the definition of containsR):

Th 1:  r I r ~~ r
Th 2:  r U r ~~ r
Th 3:  r U univ ~~ univ
Th 4:  r I Empty ~~ Empty
Th 5:  r1 U (r1 I r2) ~~ r1
Th 6:  r1 I (r1 U r2) ~~ r1
Th 7:  Comp (Comp r) ~~ r
Th 8:  Comp Empty ~~ univ
Th 9:  Comp univ  ~~ Empty
Th 10: Comp (r1 U r2) ~~ Comp r1 I Comp r2
Th 11: Comp (r1 I r2) ~~ Comp r1 U Comp r2"

Solution:

To make things more concise in these proofs, I will use U for `Union`,
I for `Intersection`, and Comp for Complement.  Also, I will use ~~
for the equivalence sign.  Recall the definitions of the axioms:

Ax 1: r1 U (r2 U r3) === (r1 U r2) U r3
      r1 I (r2 I r3) === (r1 I r2) I r3
Ax 2: r1 U r2 === r2 U r1
      r1 I r2 === r2 I r1
Ax 3: r1 I (r2 U r3) === (r1 I r2) U (r1 I r3)
      r1 U (r2 I r3) === (r1 U r2) I (r1 U r3)
Ax 4: r U Empty  === r
      r I univ   === r
Ax 5: r U Comp r === univ
      r I Comp r === Empty

Proof of 1st Theorem: r I r ~~ r

r I r
~~ (r I r) U Empty		Ax 4
~~ (r I r) U (r I Comp r)	Ax 5
~~ r I (r U Comp r)		Ax 3
~~ r I univ			Ax 5
~~ r				Ax 4

Proof of 3rd Theorem: r U univ ~~ univ

r U univ 
~~ (r U univ) I univ		Ax 4
~~ (r U univ) I (r U Comp r)	Ax 5
~~ r U (univ I Comp r)		Ax 3
~~ r U Comp r			Ax 4
~~ univ				Ax 5

Proof of 5th Theorem: r1 U (r1 I r2) ~~ r1

r1 U (r1 I r2) 
~~ (r1 I univ) U (r1 I r2)	Ax 4
~~ r1 I (univ U r2)		Ax 3
~~ r1 I (r2 U univ)		Ax 2
~~ r1 I univ			Ax 5
~~ r1				Ax 4

Proof of 10th Theorem: Comp (r1 U r2) ~~ Comp r1 I Comp r2

...


8.  Exercise 9.3 in SOE.

"What is the type of ys in:

xs = [1,2,3] :: [Float]
ys = map (+) xs           "

Solution:

ys :: [Float -> Float]
       

9.  Exercise 9.4 in SOE.
       
"Define a function applyEach that, given a list of functions, applies
each to some given value.  For example:

applyEach [simple 2 2, (+3)] 5  ===>  [14, 8]

where simple is as defined in Section 1.1."

Solution:

> applyEach fs v = map (\f -> f v) fs

or, using $ from the standard prelude:

> applyEach' fs v = map ($v) fs


10. Exercise 9.5 in SOE.

"Define a function applyAll that, given a list of functions [f1, f2,
..., fn] and a value v, returns the result f1 (f2 (...(fn v)...)).
For example:

applyAll [simple 2 2, (+3)] 5  ===>  20  "

Solution:

> applyAll fs v = foldr ($) v fs

Note in both this exercise and the previus one, that if the arguments
to the function were reversed, we could use currying simplification:

applyEach v = map   ($v)
applyAll    = foldr ($)

(in the latter case it was used twice!)


11. Exercise 9.7 in SOE.
       
"Define a function "twice" that, given a function f, returns a function
that applies f twice to its argument.  For example:

(twice (+1)) 2 ==> 4

What is the principal type of twice?  Describe what 'twice twice'
does, and give an example of its use.  How about 'twice twice twice'
and 'twice (twice twice)'?"

Solution:

twice f x = f (f x)

or, using function composition:

> twice :: (a -> a) -> a -> a
> twice f = f . f

"twice twice f" can be unfolded as follows:
twice twice f
==> (twice . twice) f
==> twice (twice f)
==> twice (f . f)
==> (f . f) . (f . f)
==> f . f . f . f

The last line is justified because function composition is
associative.  So "twice twice" applies its functional argument four
times.

Similarly, both "twice twice twice" and "twice (twice twice)" apply
their functional arguments SIXTEEN times.  You can see this because
the last line above becomes:

twice . twice . twice . twice

which, when applied to f, becomes:

twice (twice (twice (twice f)))

which expands into sixteen compositions of f.

At the next level, i.e. "twice twice twice twice", note that we end up
with sixteen compositions of twice applied to f -- which expands into
2^16 compositions of f, and causes a Hugs stack overflow!!!

In general, n applications of twice will call its function
2^(2^(2^...^2)) times, where there are n stacks of exponents; for
example for n = 4, 2^2^2^2 = 2^16.


12. Exercise 9.9 in SOE.
       
"Suppose we define a function fix as:

fix f = f (fix f)

What is the principal type of fix?  (This is tricky!)  Suppose
further that we have a recursive function:

remainder    :: Integer -> Integer -> Integer
remainder a b = if a<b then a
                else remainder (a-b) b

Rewrite this function using fix so that it is not recursive.  (Also
tricky!)  Do you think that this process can be applied to any
recursive function?"

Hint: A fixpoint of a function f is a value x such that f x = x.
Interestingly, fix computes a fixpoint of a function, because fix f
is defined as f (fix f) -- so by definition it is a fixpoint!!

Now consider the recursive equation ones = 1 : ones.  What value of
ones satisfies this equation?  The answer is the infinite list of
ones.  But note that this is the same as asking what is the fixpoint
of \ones -> 1 : ones, because this function, when applied to its
fixpoint, must equal the same value.  That is:

(\ones -> 1 : ones) ones = 1 : ones = ones

Indeed, fix (\ones -> 1 : ones) is the answer we want.  To convince
yourself of this, try evaluating this in Hugs:

take 10 (fix (\ones -> 1 : ones))

So to solve the original problem, think of the equation for remainder
to be like the equation for ones above, and see if you can work it out.

Solution:

> fix :: (a -> a) -> a
> fix f = f (fix f)

Using the hint, let's rewrite remainder so that it looks like the
equation for ones:

remainder = \a b -> if a<b then a
                    else remainder (a-b) b

Continuing with the hint, we can then define remainder using fix:

> remainder = fix (\remainder -> \a b -> if a<b then a
>                   else remainder (a-b) b)

Note that this is non-recursive!  Indeed, this process can be applied
to any recursive function, thus concentrating all recursion in the
world to exactly one spot: fix!!

By the way, another way to define remainder non-recursively so that it
looks as much like the original function as possible is like this:

> remFun remainder a b = if a<b then a
>                        else remainder (a-b) b
>
> remainder' = fix remFun


13. Exercise 9.10 in SOE.

"Rewrite this example:

map (\x-> (x+1)/2) xs

using a composition of sections."

Solution:

map ((/2).(+1)) xs