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 -}