flip f x y = f y x flip (flip f) x y = flip f y x = f x y ∴ flip (flip f) = f |
Archive for August, 2007
Exercise 9.2
Wednesday, August 8th, 2007Exercise 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 |
Exercise 8.13
Tuesday, August 7th, 2007First, 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) |
Exercise 8.12
Sunday, August 5th, 2007There 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).
Exercise 8.11
Friday, August 3rd, 2007Exercise 8.10
Friday, August 3rd, 2007The 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, 2007Proof 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, 2007Leaving 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 |