Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment