What's an anagram of Banach-Tarski? Banach-Tarski Banach-Tarski.

banach-tarski.purs

module BanachTarski where

import Prelude

import Data.Foldable (and, foldr)
import Data.Group.Free (FreeGroup(..), Signed(..), free)
import Data.List ((:))
import Data.Tuple (Tuple, snd)
import Math (Radians, acos, cos, sin)

data Generator = RotateX | RotateY

derive instance eqGenerator :: Eq Generator

type Point3D = { x :: Number, y :: Number, z :: Number }

-- Rotate by `theta` radians around the X-axis.
rotateX :: Radians -> Point3D -> Point3D
rotateX theta { x, y, z } = { x: x, y: c * y - s * z, z: s * y +  c * z } where
  s = sin theta
  c = cos theta

-- Rotate by `theta` radians around the Y-axis.
rotateY :: Radians -> Point3D -> Point3D
rotateY theta { x, y, z } = { x: c * x - s * z, y : y, z: s * x + c * z } where
  s = sin theta
  c = cos theta

-- The "paradoxical" decomposition of the free group
-- Every element of the free group has two preimages
-- Except for `mempty`, which has three
paradoxical :: FreeGroup Generator -> FreeGroup Generator
paradoxical (FreeGrp (Negative _ : tl)) = FreeGrp tl
paradoxical x                        = x

-- paradoxical <<< paradoxicalA is the identity
-- forall x y. paradoxicalA x /= paradoxical1 y
paradoxicalA :: FreeGroup Generator -> FreeGroup Generator
paradoxicalA (FreeGrp x@(Positive RotateX : _)) = FreeGrp x
paradoxicalA (FreeGrp x)                        = FreeGrp $ Negative RotateX : x

-- paradoxical <<< paradoxical1 is the identity
-- forall x y. paradoxicalA x /= paradoxical1 y
paradoxical1 :: FreeGroup Generator -> FreeGroup Generator
paradoxical1 (FreeGrp x@(Positive RotateY : _)) = FreeGrp x
paradoxical1 (FreeGrp x)                        = FreeGrp $ Negative RotateY : x

-- The free group acts on 3D space in a spherically symmetric way
-- I.e., `p` and `act x p` have the same norm
act :: FreeGroup Generator -> Point3D -> Point3D
act (FreeGrp xs) p = foldr act' p xs where
  theta = acos $ 1.0 / 3.0

  act' (Positive RotateX) = rotateX theta
  act' (Negative RotateX) = rotateX (-theta)
  act' (Positive RotateY) = rotateY theta
  act' (Negative RotateY) = rotateY (-theta)

-- A function that, given a point, returns a tuple of a point and an element of `Free Generator`.
-- If `f :: Choice`, `f x = Tuple y g` then `act g y = x`
-- Also, if `g :: FreeGroup Generator`, then `fst $ f (g x) == fst $ f x`.
-- The proof requires the axiom of choice to prove the existence of such a function,
-- but we'll just use `Reader` to skirt the issue.
type Choice = Point3D -> Tuple Point3D (FreeGroup Generator)

-- `banachTarski choice` is a function that maps the unit sphere to two copies of the unit sphere.
-- (i.e., every point on the unit sphere has two preimages)
-- This is based on the "paradoxical decomposition" but is a bit more complicated
banachTarski :: Choice -> Point3D -> Point3D
banachTarski choice pt = 
  case groupElement of
        FreeGrp (Negative RotateY : _) -> act (free $ RotateY) pt
        FreeGrp x@(Negative RotateX : _) -> if isPureNegXRotation x
                                              then pt
                                              else act (free $ RotateX) pt
        _ -> pt
  where groupElement = snd $ choice pt  
        isPureNegXRotation el = and $ map ((==) (Negative RotateX)) el

-- Exercise: Write functions `banachTarskiA` and `banachTarski1` such that 
--        banachTarski <=< banachTarskiA is the identity
--        banachTarski <=< banachTarski1 is the identity
--        forall choice x y. banachTarski1 choice x y /= banachTarskiA choice x y