Lab 4

[BertLisser]

Exercise 6

trClosList :: Ord a => Rel a -> Rel a -> Rel a
trClosList r s
  | sort s == sort (s `union` (s @@ r)) = s
  | otherwise = trClosList r (s `union` (s @@ r))

trClos :: Ord a => Rel a -> Rel a
trClos r = trClosList r r

The first step will be go wrong.
Solution

trClosList :: Ord a => Rel a -> Rel a -> Rel a
trClosList r s
  | sort s == sort (s `union` (s @@ r)) = s
  | otherwise = trClosList r (s `union` (s @@ r))

trClos :: Ord a => Rel a -> Rel a
trClos r = trClosList (nub r)  (nub r)

Exercise 8
Totally wrong
prop_symClosTrClos :: Ord a => Rel a -> Bool
prop_symClosTrClos r = (symClos . trClos) r == (trClos . symClos) r

test_symClosTrClosEquality :: IO ()
test_symClosTrClosEquality = do
putStrLn ("Testing whether transitive closure of symmetric closure is equal to"
++ " the symmetric closure of the transitive closure")
quickCheck (prop_symClos :: (Rel Int -> Bool))

The test must be

quickCheck (prop_symClosTrClos :: (Rel Int -> Bool))

{-
  Test report: they are equal for all test cases. However, we can also show that
  they would be equal:
  Both functions for transitive closure and symmetric closure only use the union
  operator as a final set operation. This means that applying the function on a
  set will never remove elements from that set. Therefore, the operations are
  associative. This means that the order of calling this functions does not matter,
  the result will be the same.
-}