Contents 1 Some set theory: 2 The naming function 3 The dynamic binding function 4 An example system

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 = unions [phi m q b | b <- toList (alpha m)] << 
                     unions [phi m q b `ranRes` sigma m b | b <- toList (alpha m)]
	   | otherwise =  ids (dom (tau m) `union` 
                          unions [ran (beta (m-1) b b << eta m b) | b <- toList (alpha m)])
 
phi :: Int -> Int -> Int -> Set (String, String)
phi m q b = beta (m-1) q b `comp` (beta (m-1) b b << eta m b)

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", "A.f1"), ("g1", "A.g1")]
tau 2 = fromList [("f2", "B.f2"), ("g2", "B.g2")]
tau 3 = fromList [("f1", "D.f1"), ("g1", "D.g1")]
 
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