bourbaki.hs

import Data.Set

type Letter = String

data Term = TTau Integer Letter Relation
          | TBox Integer Letter
          | TVar Letter
          | TSubst Term Letter Term
          | TPair Term Term
          deriving (Show, Eq)
data Relation = ROr Relation Relation
              | RNot Relation
              | RSubst Term Letter Relation
              | REq Term Term
              | RIn Term Term
              deriving (Show, Eq)

rand :: Relation -> Relation -> Relation
rand a b = RNot (ROr (RNot a) (RNot b))

implies :: Relation -> Relation -> Relation
implies a b = ROr (RNot a) b

iff :: Relation -> Relation -> Relation
iff a b = rand (implies a b) (implies b a)

class Subst a where
  subst :: Letter -> Term -> a -> a

instance Subst Term where
  subst y t t' = case t' of
    (TVar x) -> if x==y
                then t
                else t'
    (TSubst b x a) -> if x==y
                      then (TSubst b x a)
                      else (TSubst (subst y t b) x (subst y t a))
    _ -> t'

instance Subst Relation where
  subst y t (ROr a b) = ROr (subst y t a) (subst y t b)
  subst y t (RNot a) = RNot (subst y t a)
  subst y t (RSubst b x r) = if y==x then (RSubst b x r)
                             else RSubst (subst y t b) x (subst y t r)
  subst y t (REq a b) = REq (subst y t a) (subst y t b)
  subst y t (RIn a b) = RIn (subst y t a) (subst y t b)

class Simplifier a where
  simp :: a -> a

instance Simplifier Relation where
  simp (ROr a b) = let a' = simp a
                       b' = simp b
                   in if (simp (RNot a')) == b' then (REq (TVar "_") (TVar "_"))
                      else ROr a' b'
  simp (RNot (RNot a)) = simp a
  simp (RNot a) = RNot (simp a)
  simp (RSubst t x r) = subst x t r -- RSubst (simp t) x (simp r)
  simp (REq a b) = REq (simp a) (simp b)
  simp (RIn a b) = RIn (simp a) (simp b)

instance Simplifier Term where
  simp (TTau m x r) = TTau m x (simp r)
  simp (TBox m x) = TBox m x
  simp (TVar x) = TVar x
  simp (TSubst t x b) = subst x t b -- TSubst (simp t) x (simp b)
  simp (TPair a b) = TPair (simp a) (simp b)

class Shift a where
  shift :: a -> a

instance Shift Term where
  shift (TTau m x r) = TTau (m+1) x r
  shift (TBox m x) = TBox (m+1) x
  shift (TVar x) = TVar x
  shift (TSubst b x a) = TSubst (shift b) x (shift a)
  shift (TPair a b) = TPair (shift a) (shift b)

instance Shift Relation where
  shift (ROr a b) = ROr (shift a) (shift b)
  shift (RNot a) = RNot (shift a)
  shift (RSubst a x r) = RSubst (shift a) x (shift r)
  shift (REq a b) = REq (shift a) (shift b)
  shift (RIn a b) = RIn (shift a) (shift b)

tau :: Letter -> Relation -> Term
tau x r = TTau 0 x $ subst x (TBox 0 x) (shift r)

class Vars a where
  vars :: a -> Set Letter

instance Vars Term where
  vars (TTau _ x r) = Data.Set.union (Data.Set.singleton x) (vars r)
  vars (TBox _ x) = (Data.Set.singleton x)
  vars (TVar x) = Data.Set.singleton x
  vars (TSubst b x a) = Data.Set.delete x (Data.Set.union (vars a) (vars b))
  vars (TPair a b) = Data.Set.union (vars a) (vars b)

instance Vars Relation where
  vars (ROr a b) = Data.Set.union (vars a) (vars b)
  vars (RNot a) = vars a
  vars (RSubst a x r) = Data.Set.delete x (Data.Set.union (vars a) (vars r))
  vars (REq a b) = Data.Set.union (vars a) (vars b)
  vars (RIn a b) = Data.Set.union (vars a) (vars b)

freshVar :: Letter -> Int -> Set Letter -> Letter
freshVar x m vs = if (x++(show m)) `Data.Set.member` vs
  then freshVar x (m+1) vs
  else x++(show m)

fresh :: Vars a => Letter -> a -> Letter
fresh x fm = let vs = vars fm
  in if x `elem` vs
     then freshVar x 0 vs
     else x

class Occur a where
  occur :: Letter -> a -> Integer

instance Occur Term where
  occur x (TTau _ y r) = if x==y then 0 else (occur x r)
  occur x (TBox _ _) = 0
  occur x (TVar y) = if x==y then 1 else 0
  occur x (TSubst b y a) = if x==y
    then (occur x b)*(occur x a)
    else (occur x b)*(occur y a)+(occur x a)
  occur x (TPair a b) = (occur x a) + (occur x b)

instance Occur Relation where
  occur x (ROr a b) = (occur x a) + (occur x b)
  occur x (RNot a) = occur x a
  occur x (RSubst a y r) = if x==y
    then (occur x a)*(occur x r)
    else (occur x a)*(occur y r) + (occur x r)
  occur x (REq a b) = (occur x a) + (occur x b)
  occur x (RIn a b) = (occur x a) + (occur x b)
  
class Len a where
  len :: a -> Integer

instance Len Term where
  len (TTau _ _ r) = 1 + len r
  len (TBox _ _) = 1
  len (TVar _) = 1
  len (TSubst b x a) = ((len b) - 1)*(occur x a) + (len a)
  len (TPair a b) = 1 + (len a) + (len b)

instance Len Relation where
  len (ROr a b) = 1 + len a + len b
  len (RNot a) = 1 + len a
  len (RSubst a y r) = ((len a) - 1)*(occur y r) + (len r)
  len (REq a b) = 1 + len a + len b
  len (RIn a b) = 1 + len a + len b

exists :: Letter -> Relation -> Relation
exists x r = RSubst (tau x r) x r
-- exists x r = RSubst (TTau 0 x (shift r)) x (shift r)

forall :: Letter -> Relation -> Relation
forall x r = RNot (exists x (RNot r))

{-
After C49. in ch II sec 1.6, Bourbaki introduces notation "To represent
the term $\tau_{y}(\forall x)((x\in y)\iff R)$ which does not depend on
the choice of $y$ (distinct from $$ and not appearing in $R$), we shall
introduce a functional symbol $\mathcal{E}_{x}(R)$; the corresponding
term does not contain $x$. This term is denoted by 'the set of all $x$
such that $R$'."

We denote this by `ens x R`.
-}
ens :: Letter -> Relation -> Term
ens x r = let y = fresh "y" r
  in TTau 0 y (shift (forall x (iff (RIn (TVar x) (TVar y)) r)))
-- tau y (forall x (iff (RIn (TVar x) (TVar y)) r))


-- The set with two elements, a.k.a., the unordered pair.
pair :: Term -> Term -> Term
pair x y = let z = fresh "z" (REq x y)
  in ens z (ROr (REq x (TVar z)) (REq y (TVar z)))

ssingleton :: Term -> Term
ssingleton x = let z = fresh "z" x
               in ens z (REq x (TVar z))

--- use orderedPair = TPair for debugging purposes
orderedPair :: Term -> Term -> Term
orderedPair x y = pair (ssingleton x) (pair x y)

orderedTriple :: Term -> Term -> Term -> Term
orderedTriple x y z = orderedPair (orderedPair x y) z

cartesianProduct :: Term -> Term -> Term
cartesianProduct x y = ens "z" (exists "x'"
                                (exists "y'"
                                 (rand (REq (TVar "z") (orderedPair (TVar "x'") (TVar "y'")))
                                       (rand (RIn (TVar "x'") x)
                                             (RIn (TVar "y'") y)))))

subset :: Term -> Term -> Relation
subset u v = forall "s" (implies (RIn (TVar "s") u) (RIn (TVar "s") v))

emptySet :: Term
emptySet = TTau 0 "X" (forall "x" (RNot (RIn (TVar "x") (TVar "X"))))

termA :: Term -> Letter -> Letter -> Letter -> Relation
termA x u upperU z = REq (TVar u) (orderedTriple (TVar upperU) x (TVar z))

termB :: Term -> Letter -> Letter -> Relation
termB x upperU z = subset (TVar upperU) (cartesianProduct x (TVar z))

termC :: Term -> Letter -> Relation
termC x upperU = forall "x" (implies (RIn (TVar "x") x)
                                    (exists "y" (RIn (orderedPair (TVar "x") (TVar "y"))
                                                     (TVar upperU))))

termD :: Letter -> Relation
termD upperU = forall "x"
  (forall "y" (forall "z"
                (implies (rand (RIn (orderedPair (TVar "x") (TVar "y")) (TVar upperU))
                                (RIn (orderedPair (TVar "x") (TVar "z")) (TVar upperU)))
                          (REq (TVar "y") (TVar "z")))))

termE :: Letter -> Letter -> Relation
termE upperU z = forall "y" (implies
                             (RIn (TVar "y") (TVar z))
                             (exists "x" (RIn (orderedPair (TVar "x") (TVar "y"))
                                              (TVar upperU))))

card :: Term -> Term
card x = TTau 0 "Z" (exists "u" (exists "U" (rand (termA x "u" "U" "Z")
                                          (rand (termB x "U" "Z")
                                           (rand (termC x "U")
                                            (rand (termD "U")
                                             (termE "U" "Z")))))))

one :: Term
one = card (ssingleton emptySet)

two :: Term
two = card (pair emptySet (ssingleton emptySet))

{-
The value f(x) corresponding to x of a function f, when G is the graph of f, is (slightly optimized) the y s.t. (x,y) is in G.

Bourbaki defines (ch.II sec.3.1, definition 3, remark 1) the image of a set X according to a graph G as
> ens y (exists "x" (rand (RIn (TVar "x") X)
>                         (RIn (orderedPair (TVar "x") y) G)))
But since X is a singleton for our case, we don't need to check x\in{x}.

I further simplify things and just say the value of x in G is that y s.t. (x,y) in G.
-}
val :: Term -> Term -> Term
val x graph = tau "y" (RIn (orderedPair x (TVar "y")) graph)


{-
In a remark after Proposition 5 (ch III section 3.3), Bourbaki notes
if `a` and `b` are two cardinals, and `I` a set with two elements (e.g.,
the cardinal 2), then there exists a mapping o mapping f of I onto {a, b}
for which the sum of this family is denoted a+b.

The sum of a family of sets is discussed in Ch II section 4.8, definition 8 gives it as:
Let (X_{i})_{i\in I} be a family of sets.
The sum of this family is the union of the family of sets (X_{i}\times \{i\})_{i\in I}.

The notion of a family of sets is defined in II.3.4. It is basically the graph of a function I\to {X_{i}}.

The union of a family of sets (X_{i})_{i\in I} is (ch II section 4.1 definition 1)
ens x (exists "i" (and (RIn (TVar "i") I) (RIn (TVar x) X)))

The family {X_{0}, X_{1}} when X_{0}=X_{1}=1 is then `cartesianProduct two one`.

Combining this together, we get the sum as:
-}
setSum :: Term -> Term -> Term
setSum idx family = ens "x" (exists "i"
                             (rand (RIn (TVar "i") idx)
                               (RIn (TVar "x") (val (TVar "i") family))))

{-
When `a` and `b` are cardinal numbers, Bourbaki uses the
indexed family {f_1, f_2} where f_1=a and f_2=b. This indexed family
coincides with the cartesian product of the cardinality 2 with
the unordered pair `{a, b}`. Then the sum of this family is the sum
of cardinals.
-}
cardSum :: Term -> Term -> Term
cardSum a b = setSum two (cartesianProduct two (pair a b))

onePlusOneIsTwo :: Relation
onePlusOneIsTwo = REq two (cardSum one one)

-- just curious about how big these terms are...
pairOfOnes :: Term
pairOfOnes = pair one one

productTwoOnes :: Term
productTwoOnes = cartesianProduct two pairOfOnes

main = do
  putStrLn ("The size of {x, y} = " ++ (show (len (pair (TVar "x") (TVar "y")))))
  putStrLn ("Size of (x, y) = " ++ (show (len (orderedPair (TVar "x") (TVar "y")))))
  putStrLn ("Size of the Empty Set = " ++ (show (len emptySet)))
  putStrLn ("Size of $X\\times Y$ = " ++ (show (len (cartesianProduct (TVar "X") (TVar "Y")))))
  putStrLn ("Size of       1   = " ++ (show (len one)))
  putStrLn ("Size of `{1,1}`   = " ++ (show (len pairOfOnes)))
  putStrLn ("Size of `2*{1,1}` = " ++ (show (len productTwoOnes)))
  putStrLn ("Size of '1+1=2' = " ++ (show (len onePlusOneIsTwo)))
  putStrLn ("Size of 1*      = " ++ (show (len (simp one))))
  putStrLn ("Size of A = " ++ (show (len (termA (ssingleton emptySet) "u" "U" "Z"))))
  putStrLn ("Size of B = " ++ (show (len (termB (ssingleton emptySet) "U" "Z"))))
  putStrLn ("Size of C = " ++ (show (len (termC (ssingleton emptySet) "U"))))
  putStrLn ("Size of D = " ++ (show (len (termD "U"))))
  putStrLn ("Size of E = " ++ (show (len (termE "U" "Z"))))

{- prints (after about 7 minutes 30 seconds):
The size of {x, y} = 205
Size of (x, y) = 4545
Size of the Empty Set = 12
Size of $X\times Y$ = 3184591216053048167
Size of 1         = 2409875496393137472149767527877436912979508338752092897
Size of `{1,1}`   = 67476513899007849220193490780568233563426233485058601293
Size of `2*{1,1}` = 48825985993649371395098650759903534013224010482907737605003605636688887
Size of '1+1=2'   = 22411322875029037193545441224646148573589725893763139344694162029240084343041 ~ 2.24113228750290371 * 10^76
Size of A = 15756227
Size of B = 10006221599868316846
Size of C = 59308566315
Size of D = 364936653508895574881
Size of E = 101217516631
-}

I have refactored this out into its own project, with a literate Haskell program which pretty prints the code and has commentary (as well as citations to definitions in Bourbaki's Theory of Sets).