Skip to content

Instantly share code, notes, and snippets.

@pqnelson
Last active January 7, 2024 21:23
Show Gist options
  • Save pqnelson/184a13964b5560eac73d821309c5c081 to your computer and use it in GitHub Desktop.
Save pqnelson/184a13964b5560eac73d821309c5c081 to your computer and use it in GitHub Desktop.
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
-}
@pqnelson
Copy link
Author

pqnelson commented Jan 7, 2024

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).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment