Archive for August, 2007

Newer Entries »

Exercise 9.2

Wednesday, August 8th, 2007 
flip f x y = f y x
flip (flip f) x y 
= flip f y x 
= f x y
∴ flip (flip f) = f

Posted in Uncategorized | No Comments »

Exercise 9.1

Wednesday, August 8th, 2007 
(Polygon pts) `containsS` p 
    = let leftOfList = map isLeftOfp
                       (zip pts (tail pts ++ [head pts]))
          isLeftOfp = isLeftOf p
      in and leftOfList

Posted in Uncategorized | No Comments »

Exercise 8.13

Tuesday, August 7th, 2007

First, the new definitions:

data Region = UnitCircle
            | Polygon [Coordinate]
            | AffineTransform Matrix3x3 Region
            | Empty
              deriving Show
 
type Vector3 = (Float, Float, Float)
type Matrix3x3 = (Vector3, Vector3, Vector3)
type Matrix2x2 = ((Float, Float), (Float, Float))

And some old ones that will suffice unchanged:

type Coordinate = (Float, Float)
type Ray = (Coordinate, Coordinate)
 
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
 
containsR :: Region -> Coordinate -> Bool
(Polygon pts) `containsR` 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
Empty `containsR` p = False

Now we have the new forms of containsR to write. The UnitCircle is easy:

UnitCircle `containsR` (x,y) = x^2 + y^2 <= 1

And in general, the transform of a region contains a point if the region contains the inverse transform of that point.

(AffineTransform m r) `containsR` (x,y)
    = if determinant3 m == 0
      then singularContains m (x,y)
      else let m' = inverse m
               (x', y', _) = matrixMul m' (x,y,1)
           in r `containsR` (x', y')

Now some standard code for multiplying and inverting matrices:

matrixMul :: Matrix3x3 -> Vector3 -> Vector3
matrixMul (r1, r2, r3) v
    = (dotProduct r1 v,
       dotProduct r2 v,
       dotProduct r3 v)
 
dotProduct :: Vector3 -> Vector3 -> Float
dotProduct (a,b,c) (x,y,z) = a*x + b*y + c*z
 
inverse :: Matrix3x3 -> Matrix3x3
inverse ((a,b,c), (d,e,f), (g,h,i))
    = let det = determinant3 ((a,b,c), (d,e,f), (g,h,i))
          a' = determinant2 ((e,f), (h,i)) / det
          b' = determinant2 ((c,b), (i,h)) / det
          c' = determinant2 ((b,c), (e,f)) / det
          d' = determinant2 ((f,d), (i,g)) / det
          e' = determinant2 ((a,c), (g,i)) / det
          f' = determinant2 ((c,a), (f,d)) / det
          g' = determinant2 ((d,e), (g,h)) / det
          h' = determinant2 ((b,a), (h,g)) / det
          i' = determinant2 ((a,b), (d,e)) / det
      in ((a',b',c'), (d',e',f'), (g',h',i'))
 
determinant3 :: Matrix3x3 -> Float
determinant3 ((a,b,c), (d,e,f), (g,h,i))
    = let aei = a * e * i
          afh = a * f * h
          bdi = b * d * i
          cdh = c * d * h
          bfg = b * f * g
          ceg = c * e * g
      in aei - afh - bdi + cdh + bfg - ceg
 
determinant2 :: Matrix2x2 -> Float
determinant2 ((a,b), (c,d))
    = a * d - b * c

The only thing left is the question of how to deal with a singular (non-invertible) matrix. If an affine matrix is non-invertible, that means that AE – BD = 0. Either all four coefficients are 0, or AE = BD. If all 4 are 0, then every point in the region will be collapsed into the single point (C,F), and we need to check that this is the given point. If AE = BD otherwise, we have for any point (x,y) in the region:

x' = Ax + By + C
y' = Dx + Ey + F
Dx' = ADx + BDy + CD
Ay' = ADx + AEy + AF
    = ADx + BDy + AF [AE = BD]
∴ Dx' - Ay' = CD - AF
Dx' - Ay' + AF - CD = 0

so any point in the region will be collapsed into the line Dx’ – Ay’ + AF – CD = 0, and we need to check that the given point satisfies this equation.

singularContains :: Matrix3x3 -> Coordinate -> Bool
singularContains ((a,b,c), (d,e,f), _) (x,y)
    = if (a == 0 && b == 0 && d == 0 && e == 0)
      then (x == c && y == f)
      else (d*x - a*y + a*f - c*d == 0)

Posted in Uncategorized | No Comments »

Exercise 8.12

Sunday, August 5th, 2007

There are a couple of ways to do this (the basic problem being how to deal with concave polygons). One way is to convert the polygon to a convex hull and a list of triangles representing subtractions from the convex hull, then check containment within the hull and non-containment within the triangles. However, I present a simpler way: pick a point guaranteed not to be in the polygon, form the ray between that and the point in question, and count the number of times that ray crosses the polygon sides. If it’s even, the point is outside the polygon. This method also works for self-crossing polygons (provided that one considers any internal spaces formed as outside the polygon: consider a pentagram for example).

raysCross :: Ray -> Ray -> Bool
raysCross (a,b) (x,y) = let h = isLeftOf x (a,b) && isRightOf y (a,b)
                            i = isLeftOf y (a,b) && isRightOf x (a,b)
                            j = isLeftOf a (x,y) && isRightOf b (x,y)
                            k = isLeftOf b (x,y) && isRightOf a (x,y)
                        in (h || i) && (j || k)
 
countCrossings :: Ray -> [Ray] -> Int
countCrossings r rs = foldl (+) 0
                      (map (\x -> if raysCross r x then 1 else 0) rs)
 
guaranteedOutside :: [Vertex] -> Vertex
guaranteedOutside vs
    = (foldl maxop 0 xs + 1, foldl maxop 0 ys + 1)
    where (xs, ys) = unzip vs
          maxop a b = if a > b then a else b
 
containsS' :: Shape -> Coordinate -> Bool
(Polygon ps) `containsS'` p
    = let poutside = guaranteedOutside ps
      in (countCrossings (p,poutside)
          (zip ps (tail ps ++ [head ps]))) `mod` 2 == 1

See Exercise 8.4 for definitions of isLeftOf and isRightOf. I am also left feeling that there must be a more elegant way to count the number of list elements that fulfil a predicate (which is what countCrossings is really doing).

Posted in Uncategorized | 3 Comments »

Exercise 8.11

Friday, August 3rd, 2007

See Exercises 2.4 and 5.1. Then:

area'' :: Shape -> Float
area'' (Polygon (v1:vs)) = if convex (Polygon (v1:vs))
                           then let areas = map ((v2, v3) -> triArea v1 v2 v3)
                                               (zip vs (tail vs))
                                in foldl (+) 0 areas
                           else error "Non-convex polygon"

Posted in Uncategorized | No Comments »

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 »

Newer Entries »