Some set theory:
--Set theory
import Data.Set
--domain of a relation
dom :: (Ord a, Ord b) => Set (a, b) -> Set a
dom s = Data.Set.map (\(d, r) -> d) s
--range of a relation
ran :: (Ord a, Ord b) => Set (a, b) -> Set b
ran s = Data.Set.map (\(d, r) -> r) s
--identity of a set
ids :: (Ord a) => Set a -> Set (a, a)
ids s = Data.Set.map (\e -> (e, e)) s
--domain substraction
domSub :: (Ord a, Ord b) => Set a -> Set (a, b) -> Set (a, b)
domSub s r = fromList [(e1,e2) | (e1,e2) <- (toList r), (notMember e1 s)]
--range restriction
ranRes :: (Ord a, Ord b) => Set (a, b) -> Set (b) -> Set (a, b)
ranRes r s = fromList [(e1,e2) | (e1,e2) <- (toList r), (member e2 s)]
--override
(<<) :: (Ord a, Ord b) => Set (a, b) -> Set (a, b) -> Set (a, b)
(<<) s t = union t (domSub (dom t) s)
--composition
comp :: (Ord a, Ord b, Ord c) => Set (a, b) -> Set (b, c) -> Set (a, c)
comp r v = fromList [(e1, e4) | (e1,e2) <- toList r, (e3,e4) <- toList v, e2 == e3 ]
--inverse
inv :: (Ord a, Ord b) => Set (a, b) -> Set (b, a)
inv r = fromList [(e2,e1)|(e1,e2) <- toList r]
--relation image
image :: (Ord a, Ord b) => Set (a, b) -> Set (a) -> Set (b)
image r w = fromList [e2 |(e1,e2) <-toList r, member e1 w]
The naming function
beta :: Int -> Int -> Int -> Set (String, String)
beta 0 0 0 = empty
beta m q p | q > p = empty
| p > m = empty
| p < m = beta(m-1) q p
| q < p = betaPrime m q << theta m q
| otherwise = ids (dom (tau m) `union`
unions [ran (beta (m-1) b b << eta m b) | b <- toList (alpha m)])
betaPrime :: Int -> Int -> Set (String, String)
betaPrime m q = unions [beta (m-1) q b `comp` (ids(ran (beta(m-1) q b)) << eta m b)
| b <- toList (alpha m)]
theta :: Int -> Int -> Set (String, String)
theta m q = unions [beta(m-1) q b `comp` (ids(ran (beta(m-1) q b)) << eta m b) `ranRes` sigma m b
| b <- toList (alpha m)]
The dynamic binding function
gamma :: Int -> String -> Set (Int, String)
gamma st fn = fromList [(dt, f)|dt <- [1..n], f <- toList (image (delta n st dt) (fromList [fn]))]
delta :: Int -> Int -> Int -> Set (String, String)
delta m q p | p > m = empty
| q > p = empty
| p < m = delta (m-1) q p
| otherwise = beta n q m `comp` (
unions [(inv (beta n b b << eta m b)) `comp` delta (m-1) b b | b <- toList (alpha m)]
<< tau m)
An example system
tau:: Int -> Set (String, String)
tau 1 = fromList [("f1", "C1.f1"), ("g1", "C1.g1"), ("s1", "C1.s1")]
tau 2 = fromList [("f2", "C2.f2"), ("g2", "C2.g2"), ("s1", "C2.s1")]
tau 3 = fromList [("f1", "C3.f1"), ("g1", "C3.g1"), ("s1", "C3.s1")]
eta:: Int -> Int -> Set (String, String)
eta 2 1 = fromList [("f1", "f2"), ("g1","g2")]
eta 3 1 = empty
eta 3 2 = empty
alpha:: Int -> Set (Int)
alpha 1 = empty
alpha 2 = insert 1 empty
alpha 3 = fromList [1, 2]
sigma:: Int -> Int -> Set (String)
sigma 2 1 = empty
sigma 3 1 = insert "g1" empty
sigma 3 2 = insert "f2" empty
n :: Int
n = 3
