## Archive for the ‘Uncategorized’ Category

### Exercise 8.10

Friday, August 3rd, 2007

The first “fact” cannot be proven because it is false! Given the definition:

```containsS :: Shape -> Coordinate -> Bool (Rectangle s1 s2) `containsS` (x,y) = let t1 = s1 / 2 t2 = s2 / 2 in -t1 <= x && x <= t1 && -t2 <= y && y <= t2 (Ellipse r1 r2) `containsS` (x,y) = (x/r1)^2 + (y/r2)^2 <= 1```

It is not true that:

`Rectangle s1 s2 `containsS` p = Rectangle (-s1) s2 `containsS` p`

This can be easily seen e.g. when s1 = 4, s2 = 2, p = (1,1). However, it’s true that:

`rectangle s1 s2 `containsS` p = rectangle (-s1) s2 `containsS` p`

Given our updated definition of `containsS` for polygons from Exercise 8.4. To prove the second fact is trivial:

```Ellipse (-r1) r2 `containsS` (x,y)
= (x/(-r1))2 + (y/r2)2 <= 1
= (x2/(-r1)2) + (y/r2)2 <= 1
= (x2/r12) + (y/r2)2 <= 1
= (x/r1)2 + (y/r2)2 <= 1
= Ellipse r1 r2 `containsS` (x,y)```

### Exercise 8.9

Wednesday, August 1st, 2007

Proof from axioms is something that takes great care: it is all too easy to skip a step that “obviously follows” from the axioms without proving that step. I’m not convinced this is all correct…

```r â‰¡ r `Intersect` univ [Axiom 4] â‰¡ r `Intersect` (r `Union` Complement r) [Axiom 5] â‰¡ (r `Intersect` r) `Union` (r `Intersect` Complement r) [Axiom 3] â‰¡ (r `Intersect` r) `Union` Empty [Axiom 5] â‰¡ (r `Intersect` r) [Axiom 4]   Lemma 1: r â‰¡ (r `Intersect` r)   r â‰¡ r `Union` Empty [Axiom 4] â‰¡ r `Union` (r `Intersect` Complement r) [Axiom 5] â‰¡ (r `Union` r) `Intersect` (r `Union` Complement r) [Axiom 3] â‰¡ (r `Union` r) `Intersect` univ [Axiom 5] â‰¡ (r `Union` r) [Axiom 4]   Lemma 2: r â‰¡ (r `Union` r)   r `Union` univ â‰¡ r `Union` (r `Union` Complement r) [Axiom 5] â‰¡ (r `Union` r) `Union` Complement r [Axiom 1] â‰¡ r `Union` Complement r [Lemma 2] â‰¡ univ [Axiom 5]   Lemma 3: r `Union` univ â‰¡ univ   r `Intersect` Empty â‰¡ r `Intersect` (r `Intersect` Complement r) [Axiom 5] â‰¡ (r `Intersect` r) `Intersect` Complement r [Axiom 1] â‰¡ r `Intersect` Complement r [Lemma 1] â‰¡ Empty [Axiom 5]   Lemma 4: r `Intersect` Empty â‰¡ Empty   Let X = (r1 `Union` (r1 `Intersect` r2)) X `Intersect` Complement r1 â‰¡ (r1 `Union` (r1 `Intersect` r2)) `Intersect` Complement r1 â‰¡ (r1 `Intersect` Complement r1) `Union` ((r1 `Intersect` r2) `Intersect` Complement r1) [Axiom 3] â‰¡ Empty `Union` ((r1 `Intersect` r2) `Intersect` Complement r1) [Axiom 5] â‰¡ (r1 `Intersect` r2) `Intersect` Complement r1 [Axiom 4] â‰¡ (r2 `Intersect` r1) `Intersect` Complement r1 [Axiom 2] â‰¡ r2 `Intersect` (r1 `Intersect` Complement r1) [Axiom 1] â‰¡ r2 `Intersect` Empty [Axiom 5] â‰¡ Empty [Lemma 4] âˆ´ by Axiom 5, X = r1   Lemma 5: (r1 `Union` (r1 `Intersect` r2)) â‰¡ r1   r1 `Intersect` (r1 `Union` r2) â‰¡ (r1 `Union` r1) `Intersect` (r1 `Union` r2) [Lemma 2] â‰¡ r1 `Union` (r1 `Intersect` r2) [Axiom 3] â‰¡ r1 [Lemma 5]   Lemma 6: (r1 `Intersect` (r1 `Union` r2)) â‰¡ r1   Let X = Complement (Complement r) X `Union` (Complement r) â‰¡ Complement (Complement r) `Union` (Complement r) â‰¡ univ [Axiom 5] âˆ´ by Axiom 5, X = r   Lemma 7: Complement (Complement r) â‰¡ r   Let X = Complement Empty X `Union` Empty â‰¡ Complement Empty `Union` Empty â‰¡ univ [Axiom 5] âˆ´ by Axiom 4, X = univ   Lemma 8: Complement Empty â‰¡ univ   Complement univ â‰¡ Complement (Complement Empty) [Lemma 8] â‰¡ Empty [Lemma 7]   Lemma 9: Complement univ â‰¡ Empty   Let X = Complement (r1 `Union` r2) (r1 `Union` r2) `Union` X â‰¡ (r1 `Union` r2) `Union` Complement (r1 `Union` r2) â‰¡ univ [Axiom 5]   Let Y = Complement r1 `Intersect` Complement r2 (r1 `Union` r2) `Union` Y â‰¡ (r1 `Union` r2) `Union` (Complement r1 `Intersect` Complement r2) â‰¡ ((r1 `Union` r2) `Union` Complement r1) `Intersect` ((r1 `Union` r2) `Union` Complement r2) [Axiom 3] â‰¡ ((r2 `Union` r1) `Union` Complement r1) `Intersect` ((r1 `Union` r2) `Union` Complement r2) [Axiom 2] â‰¡ (r2 `Union` (r1 `Union` Complement r1)) `Intersect` ((r1 `Union` r2) `Union` Complement r2) [Axiom 1] â‰¡ (r2 `Union` (r1 `Union` Complement r1)) `Intersect` (r1 `Union` (r2 `Union` Complement r2)) [Axiom 1] â‰¡ (r2 `Union` univ) `Intersect` (r1 `Union` (r2 `Union` Complement r2)) [Axiom 5] â‰¡ (r2 `Union` univ) `Intersect` (r1 `Union` univ) [Axiom 5] â‰¡ univ `Intersect` (r1 `Union` univ) [Lemma 3] â‰¡ univ `Intersect` univ [Lemma 3] â‰¡ univ [Lemma 3]   âˆ´ X â‰¡ Y   Lemma 10: Complement (r1 `Union` r2) â‰¡ Complement r1 `Intersect` Complement r2   Let X = Complement (r1 `Intersect` r2) (r1 `Intersect` r2) `Union` X â‰¡ (r1 `Intersect` r2) `Union` Complement (r1 `Intersect` r2) â‰¡ univ [Axiom 5]   Let Y = Complement r1 `Union` Complement r2 (r1 `Intersect` r2) `Union` Y â‰¡ (r1 `Intersect` r2) `Union` (Complement r1 `Union` Complement r2) â‰¡ (r1 `Union` (Complement r1 `Union` Complement r2)) `Intersect` (r2 `Union` (Complement r1 `Union` Complement r2)) [Axiom 3] â‰¡ (r1 `Union` (Complement r1 `Union` Complement r2)) `Intersect` ((Complement r1 `Union` Complement r2) `Union` r2) [Axiom 2] â‰¡ ((r1 `Union` Complement r1) `Union` Complement r2) `Intersect` ((Complement r1 `Union` Complement r2) `Union` r2) [Axiom 1] â‰¡ ((r1 `Union` Complement r1) `Union` Complement r2) `Intersect` (Complement r1 `Union` (Complement r2 `Union` r2)) [Axiom 1] â‰¡ (univ `Union` Complement r2) `Intersect` (Complement r1 `Union` (Complement r2 `Union` r2)) [Axiom 5] â‰¡ (univ `Union` Complement r2) `Intersect` (Complement r1 `Union` (r2 `Union` Complement r2)) [Axiom 2] â‰¡ (univ `Union` Complement r2) `Intersect` (Complement r1 `Union` univ) [Axiom 5] â‰¡ (univ `Union` Complement r2) `Intersect` univ [Lemma 3] â‰¡ univ `Union` Complement r2 [Axiom 4] â‰¡ Complement r2 `Union` univ [Axiom 2] â‰¡ univ [Lemma 3]   âˆ´ X â‰¡ Y   Lemma 11: Complement (r1 `Intersect` r2) â‰¡ Complement r1 `Union` Complement r2```

### Exercise 8.8

Wednesday, August 1st, 2007

Leaving aside the argument about axioms by definition not requiring proof…

Axiom 3:

```(r1 `Intersect` (r2 `Union` r3)) `containsR` p => (r1 `containsR` p) && ((r2 `Union` r3) `containsR` p) => (r1 `containsR` p) && ((r2 `containsR` p) || (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   âˆ´ (r1 `Intersect` (r2 `Union` r3)) â‰¡ ((r1 `Intersect` r2) `Union` (r1 `Intersect` r3))   (r1 `Union` (r2 `Intersect` r3)) `containsR` p => (r1 `containsR` p) || ((r2 `Intersect` r3) `containsR` p) => (r1 `containsR` p) || ((r2 `containsR` p) && (r3 `containsR` p)) => ((r1 `containsR` p) || (r2 `containsR` p)) && ((r1 `containsR` p) || (r3 `containsR` p)) => ((r1 `Union` r2) `containsR` p) && ((r1 `Union` r3) `containsR` p) => ((r1 `Union` r2) `Intersect` (r1 `Union` r3)) `containsR` p   âˆ´ (r1 `Union` (r2 `Intersect` r3)) â‰¡ ((r1 `Union` r2) `Intersect` (r1 `Union` r3))```

Axiom 4:

```univ = Complement Empty   (r `Union` Empty) `containsR` p => (r `containsR` p) || (Empty `containsR` p) => (r `containsR` p) || False => r `containsR` p   âˆ´ (r `Union` Empty) â‰¡ r   (r `Intersect` univ) `containsR` p => (r `Intersect` Complement Empty) `containsR` p => (r `containsR` p) && (Complement Empty `containsR` p) => (r `containsR` p) && not (Empty `containsR` p) => (r `containsR` p) && not False => (r `containsR` p) && True => r `containsR` p   âˆ´ (r `Intersect` univ) â‰¡ r```

Axiom 5:

```(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   âˆ´ (r `Union` Complement r) â‰¡ univ   (r `Intersect` Complement r) `containsR` p => (r `containsR` p) && (Complement r `containsR` p) => (r `containsR` p) && not (r `containsR` p) => False => Empty `containsR` p   âˆ´ (r `Intersect` Complement r) â‰¡ Empty```

### Exercise 8.7

Tuesday, July 31st, 2007

One way to do this is to handle each constructor for a Region (and a Shape for those cases) and reflect those in the x-axis, i.e.

```flipX :: Region -> Region flipX (Translate (a,b) r) = Translate (a,-b) (flipX r) flipX (Scale (a,b) r) = Scale (a,-b) (flipX r) flipX (Complement r) = Complement (flipX r) flipX (r1 `Union` r2) = (flipX r1) `Union` (flipX r2) flipX (r1 `Intersect` r2) = (flipX r1) `Intersect` (flipX r2) flipX (HalfPlane (x1,y1) (x2,y2)) = HalfPlane (x2,-y2) (x1,-y1) flipX Empty = Empty flipX (Shape s) = Shape (flipXShape s) where flipXShape (RtTriangle a b) = RtTriangle a (-b) flipXShape (Polygon vs) = Polygon (map ((x,y) -> (x,-y)) vs) flipXShape s = s```

And similarly (negating the x-coordinate) for flipY. Note that the order of points must change in HalfPlane, and should also be reversed in flipping a Polygon if we had the clockwise ordering constraint. Another way to solve this exercise is to use the Scale constructor on a Region:

```flipX :: Region -> Region flipX r = Scale (1, -1) r   flipY :: Region -> Region flipY r = Scale (-1, 1) r```

### Exercise 8.6

Sunday, July 29th, 2007
```polygon :: [Coordinate] -> Region polygon [] = Empty polygon [x] = Empty polygon (x:xs) = halfPlanes x (xs ++ [x]) where halfPlanes x1 (x2:xs) = HalfPlane x1 x2 `Intersect` halfPlanes x2 xs halfPlanes xlast [] = Complement Empty```

### Exercise 8.5

Sunday, July 29th, 2007
```data Region = ... | HalfPlane Coordinate Coordinate ...   (HalfPlane p1 p2) `containsR` p = p `isLeftOf` (p1,p2)```

### Exercise 8.4

Sunday, July 29th, 2007

The simplest way to allow vertices in clockwise or anticlockwise order is to define isRightOf analogously to isLeftOf, and combine them with a boolean expression.

```isLeftOf :: Coordinate -> Ray -> Bool (px,py) `isLeftOf` ((ax,ay), (bx,by)) = let (s,t) = (px-ax, py-ay) (u,v) = (px-bx, py-by) in s * v >= t * u   isRightOf :: Coordinate -> Ray -> Bool (px,py) `isRightOf` ((ax,ay), (bx,by)) = let (s,t) = (px-ax, py-ay) (u,v) = (px-bx, py-by) in s * v <= t * u   (Polygon pts) `containsS` p = let leftOfList = map isLeftOfp (zip pts (tail pts ++ [head pts])) isLeftOfp p' = isLeftOf p p' rightOfList = map isRightOfp (zip pts (tail pts ++ [head pts])) isRightOfp p' = isRightOf p p' in and leftOfList || and rightOfList```

### Exercise 8.3

Sunday, July 29th, 2007
```r1 `difference` r2 = r1 `Intersect` (Complement r2)   annulus :: Radius -> Radius -> Region annulus rinner router = Shape (circle router) `difference` Shape (circle rinner)```

### Exercise 8.2

Sunday, July 29th, 2007
```area (Rectangle a b) = abs(a * b) area (RtTriangle a b) = abs(a * b) / 2 area (Ellipse r1 r2) = pi * abs(r1 * r2)   perimeter (Rectangle s1 s2) = 2 * (abs s1 + abs s2) perimeter (RtTriangle s1 s2) = abs s1 + abs s2 + sqrt(s1^2 + s2^2) perimeter (Ellipse r1 r2) | abs r1 > abs r2 = ellipsePerim (abs r1) (abs r2) | otherwise = ellipsePerim (abs r2) (abs r1) where ellipsePerim r1 r2 = let e = sqrt (r1^2 - r2^2) / r1 aux s i = nextEl e s i s = scanl aux (0.25 * e^2) [2..] test x = x > epsilon sSum = sum (takeWhile test s) in 2 * r1 * pi * (1 - sSum)```

The definitions dealing with other kinds of Shape need not be changed.

### Exercise 8.1

Sunday, July 29th, 2007
```oneCircle = Shape (Ellipse 1 1) manyCircles' = [Translate (x,y) oneCircle | x <- centers, y <- centers] where centers = [0, 2 ..] ++ [-2, -4 ..] manyCirclesRegion = foldl Union Empty manyCircles' rectRegion = Translate (4,0) (Shape (Rectangle 10 2)) fiveCircles' = rectRegion `Intersect` manyCirclesRegion```

This is technically correct, but the problem here lies with the inability to lazy evaluate Intersect in a matter similar to take. I’m not sure this could easily be made to work: we would need to define Intersect differently and probably also impose an ordering constraint on Region composition. Even then, I think we still have an ordering problem with the positive-and-negative-infinite list evaluation, whereby a bounded Region and an infinite Region (e.g. a semi-infinite halfplane) would be incompatible (although I could be wrong about this depending on how Haskell’s lazy evaluation works exactly).