1 SetTheory

-- # Software Tools for Discrete Mathematics
module Stdm08SetTheory where

import Stdm06LogicOperators

-- # Chapter 8.  Set Theory
type Set a = [a]

errfun :: (Show a) => String -> a -> String -> b
errfun f s msg = error (f ++ ": " ++ show s ++ " is not a " ++ msg)

-- Note that subset does not reject non-sets

subset :: (Eq a, Show a) => Set a -> Set a -> Bool
subset set1 set2 =
  foldr f True set1
  where
    f x sofar = if elem x set2 then sofar else False

-- note that properSubset does not reject non-sets
properSubset :: (Eq a, Show a) => Set a -> Set a -> Bool
properSubset set1 set2 =
  not (setEq set1 set2) /\ (subset set1 set2)

-- note that setEq does not reject non-sets
setEq :: (Eq a, Show a) => Set a -> Set a -> Bool
setEq set1 set2 =
  (set1 `subset` set2) /\ (set2 `subset` set1)

normalForm :: (Eq a, Show a) => [a] -> Bool
normalForm set = length (normalizeSet set) == length set

normalizeSet :: (Eq a) => [a] -> Set a
normalizeSet elts =
  foldr f [] elts
  where
    f x sofar =
      if x `elem` sofar then sofar else x : sofar

infix 3 +++

(+++) :: (Eq a, Show a) => Set a -> Set a -> Set a
(+++) set1 set2 =
  if not (normalForm set1)
    then errfun "+++" set1 "set"
    else
      if not (normalForm set2)
        then errfun "+++" set2 "set"
        else normalizeSet (set1 ++ set2)

infix 4 ***

(***) :: (Eq a, Show a) => Set a -> Set a -> Set a
(***) set1 set2 =
  if not (normalForm set1)
    then errfun "***" set1 "set"
    else
      if not (normalForm set2)
        then errfun "***" set2 "set"
        else [x | x <- set1, (x `elem` set2)]

infix 4 ~~~

(~~~) :: (Eq a, Show a) => Set a -> Set a -> Set a
(~~~) set1 set2 =
  if not (normalForm set1)
    then errfun "~~~" set1 "set"
    else
      if not (normalForm set1)
        then errfun "~~~" set2 "set"
        else [x | x <- set1, not (x `elem` set2)]

infix 5 !!!

(!!!) :: (Eq a, Show a) => Set a -> Set a -> Set a
(!!!) u a =
  if not (normalForm u)
    then errfun "!!!" u "set"
    else
      if not (normalForm a)
        then errfun "!!!" a "set"
        else u ~~~ a

powerset :: (Eq a, Show a) => Set a -> Set (Set a)
powerset set =
  if not (normalForm set)
    then errfun "powerset" set "set"
    else powersetLoop set
  where
    powersetLoop [] = [[]]
    powersetLoop (e : set) =
      let setSoFar = powersetLoop set
       in [e : s | s <- setSoFar] ++ setSoFar

crossproduct ::
  (Eq a, Show a, Eq b, Show b) =>
  Set a ->
  Set b ->
  Set (a, b)
crossproduct set1 set2 =
  if not (normalForm set1)
    then errfun "crossproduct" set1 "set"
    else
      if not (normalForm set2)
        then errfun "crossproduct" set2 "set"
        else [(a, b) | a <- set1, b <- set2]

-- # Software Tools for Discrete Mathematics
module Stdm09InductiveSets where

-- # Chapter 9. Inductively defined sets

module HL04STAL where

import DB
import Data.List

naturals = [0 ..]

evens1 = [n | n <- naturals, even n]

odds1 = [n | n <- naturals, odd n]

evens2 = [2 * n | n <- naturals]

small_squares1 = [n ^ 2 | n <- [0 .. 999]]

small_squares2 = [n ^ 2 | n <- naturals, n < 1000]

run :: Integer -> [Integer]
run n
  | n < 1 = error "argument not positive"
  | n == 1 = [1]
  | even n = n : run (div n 2)
  | odd n = n : run (3 * n + 1)

ones = 1 : ones

characters = nub [x | ["play", _, _, x] <- db]

movies = [x | ["release", x, _] <- db]

actors = nub [x | ["play", x, _, _] <- db]

directors = nub [x | ["direct", x, _] <- db]

dates = nub [x | ["release", _, x] <- db]

universe = nub (characters ++ actors ++ directors ++ movies ++ dates)

direct = [(x, y) | ["direct", x, y] <- db]

act = [(x, y) | ["play", x, y, _] <- db]

play = [(x, y, z) | ["play", x, y, z] <- db]

release = [(x, y) | ["release", x, y] <- db]

charP = \x -> elem x characters

actorP = \x -> elem x actors

movieP = \x -> elem x movies

directorP = \x -> elem x directors

dateP = \x -> elem x dates

actP = \(x, y) -> elem (x, y) act

releaseP = \(x, y) -> elem (x, y) release

directP = \(x, y) -> elem (x, y) direct

playP = \(x, y, z) -> elem (x, y, z) play

q1 = [x | x <- actors, directorP x]

q2 = [(x, y) | (x, y) <- act, directorP x]

q3 = [(x, y, z) | (x, y) <- direct, (y, z) <- release]

q4 = [(x, y, z) | (x, y) <- direct, (u, z) <- release, y == u]

q5 = [(x, y) | (x, y) <- direct, (u, "1995") <- release, y == u]

q6 =
  [ (x, y, z) | (x, y) <- direct, (u, z) <- release, y == u, z > "1995"
  ]

q7 = [x | ("Kevin Spacey", x) <- act]

q8 = [x | (x, y) <- release, y > "1997", actP ("William Hurt", x)]

q9 = q1 /= []

q10 = [x | ("Woody Allen", x) <- direct] /= []

q10' = directorP "Woody Allen"

elem' :: (Eq a) => a -> [a] -> Bool
elem' x [] = False
elem' x (y : ys)
  | x == y = True
  | otherwise = elem' x ys

addElem :: a -> [[a]] -> [[a]]
addElem x = map (x :)

powerList :: [a] -> [[a]]
powerList [] = [[]]
powerList (x : xs) = (powerList xs) ++ (map (x :) (powerList xs))

data S = Void deriving (Eq, Show)

empty :: [S]
empty = []

display :: Int -> String -> IO ()
display n str = putStrLn (display' n 0 str)
  where
    display' _ _ [] = []
    display' n m (x : xs)
      | n == m = '\n' : display' n 0 (x : xs)
      | otherwise = x : display' n (m + 1) xs

module Sol04 where

import Data.List
import HL04STAL
import SetEq

-- 4.44
-- The definition could run like this:
-- L<K :≡ |L| < |K|
--        ∨ (|L| = |K|
--          ∧∃x, xs, y, ys (L = x : xs ∧ K = y : ys ∧ (x < y ∨ (x = y ∧ xs < ys)))).
compare' :: (Ord a) => [a] -> [a] -> Ordering
compare' [] [] = EQ
compare' (x : xs) (y : ys)
  | length (x : xs) < length (y : ys) = LT
  | length (x : xs) > length (y : ys) = GT
  | otherwise = compare (x : xs) (y : ys)

-- And here is how it compares with the standard implementation of compare:
-- Sol4> compare [1,3] [1,2,3]
-- GT
-- Sol4> compare’ [1,3] [1,2,3]
-- LT
-- Sol4> compare [1,3] [1,2]
-- GT
-- Sol4> compare’ [1,3] [1,2]
-- GT

-- 4.46 Since reverse is predefined, we call our version reverse'.
reverse' :: [a] -> [a]
reverse' [] = []
reverse' (x : xs) = reverse' xs ++ [x]

-- 4.47
splitList :: [a] -> [([a], [a])]
splitList [x, y] = [([x], [y])]
splitList (x : y : zs) = ([x], (y : zs)) : addLeft x (splitList (y : zs))
  where
    addLeft u [] = []
    addLeft u ((vs, ws) : rest) = (u : vs, ws) : addLeft u rest

-- A neater version results when we avail ourselves of the map function:
split :: [a] -> [([a], [a])]
split [x, y] = [([x], [y])]
split (x : y : zs) =
  ([x], (y : zs)) : (map (\(us, vs) -> ((x : us), vs)) (split (y : zs)))

-- 4.48
q11 = [y | (x, y) <- act, x == "Robert De Niro" || x == "Kevin Spacey"]

-- 4.49
q12 =
  nub
    ( [y | ("Quentin Tarantino", y) <- act, releaseP (y, "1994")]
        ++ [y | ("Quentin Tarantino", y) <- direct, releaseP (y, "1994")]
    )

-- 4.50
q13 = [x | (x, y) <- release, y > "1997", not (actP ("William Hurt", x))]

-- 4.51
difference :: (Eq a) => [a] -> [a] -> [a]
difference xs [] = xs
difference xs (y : ys) = difference (delete y xs) ys

-- 4.53
genUnion :: (Eq a) => [[a]] -> [a]
genUnion [] = []
genUnion [xs] = xs
genUnion (xs : xss) = union xs (genUnion xss)

genIntersect :: (Eq a) => [[a]] -> [a]
genIntersect [] = error "list of lists should be non-empty"
genIntersect [xs] = xs
genIntersect (xs : xss) = intersect xs (genIntersect xss)

-- 4.54
unionSet :: (Eq a) => Set a -> Set a -> Set a
unionSet (Set []) set2 = set2
unionSet (Set (x : xs)) set2 =
  insertSet x (unionSet (Set xs) (deleteSet x set2))

intersectSet :: (Eq a) => Set a -> Set a -> Set a
intersectSet (Set []) set2 = Set []
intersectSet (Set (x : xs)) set2
  | inSet x set2 = insertSet x (intersectSet (Set xs) set2)
  | otherwise = intersectSet (Set xs) set2

differenceSet :: (Eq a) => Set a -> Set a -> Set a
differenceSet set1 (Set []) = set1
differenceSet set1 (Set (y : ys)) =
  differenceSet (deleteSet y set1) (Set ys)

-- 4.55
-- insertSet will now have to insert an item at the right position to keep the underlying list sorted.
-- This can be done in terms of an auxiliary function insertList, as follows:
insertSet' :: (Ord a) => a -> Set a -> Set a
insertSet' x (Set s) = Set (insertList x s)

insertList x [] = [x]
insertList x ys@(y : ys') = case compare x y of
  GT -> y : insertList x ys'
  EQ -> ys
  _ -> x : ys

-- 4.56
-- The only thing that is needed is a small patch in the function showSet, like this:
showSet [] str = showString "0" str
showSet (x : xs) str = showChar ' ' (shows x (showl xs str))
  where
    showl [] str = showChar ' ' str
    showl (x : xs) str = showChar ',' (shows x (showl xs str))