(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

## Contents

### 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```