Archive for the ‘Uncategorized’ Category

« Older Entries
Newer Entries »

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)

Posted in Uncategorized | 1 Comment »

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

Posted in Uncategorized | 5 Comments »

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

Posted in Uncategorized | No Comments »

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

Posted in Uncategorized | 2 Comments »

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

Posted in Uncategorized | 6 Comments »

Exercise 8.5

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

Posted in Uncategorized | No Comments »

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

Posted in Uncategorized | 9 Comments »

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)

Posted in Uncategorized | No Comments »

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.

Posted in Uncategorized | No Comments »

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).

Posted in Uncategorized | 1 Comment »

« Older Entries
Newer Entries »