Quantifiers

gistfile1.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

module Logic where

-- Quantifier
data Q a
    -- Predicate
    = P (a -> Bool)
    -- Universal Quantifier
    | forall x. (Eq x) => UQ [x] (a -> x) (Q a)
    -- Existential Quantifier
    | forall x. (Eq x) => EX Int [x] (a -> x) (Q a)

-- Given a quantifier and the full range of possible input, answers True or False
askQ :: Q a -> [a] -> Bool
askQ q xs = case q of
    P f -> all f xs
    UQ dom get q -> case dom of
        [    ] -> True
        (d:ds) -> if askQ q $ filter ((==) d . get) xs
                  then askQ (UQ ds get q) xs
                  else False
    EX n dom get q -> if n <= 0 then True else case dom of
        [    ] -> False
        (d:ds) -> if askQ q $ filter ((==) d . get) xs
                  then askQ (EX (n-1) ds get q) xs
                  else askQ (EX n ds get q) xs

ask2 q1 d1 q2 d2 p = askQ 
    ( q1 d1 fst
    $ q2 d2 snd
    $ P p) 
    [(a,b) | a <- d1, b <- d2]

ask3 q1 d1 q2 d2 q3 d3 p = askQ 
    ( q1 d1 (\(a,_,_) -> a) 
    $ q2 d2 (\(_,a,_) -> a) 
    $ q3 d3 (\(_,_,a) -> a) 
    $ P p) 
    [(a,b,c) | a <- d1, b <- d2, c <- d3]

ask4 q1 d1 q2 d2 q3 d3 q4 d4 p = askQ 
    ( q1 d1 (\(a,_,_,_) -> a) 
    $ q2 d2 (\(_,a,_,_) -> a) 
    $ q3 d3 (\(_,_,a,_) -> a) 
    $ q4 d4 (\(_,_,_,a) -> a) 
    $ P p) 
    [(a,b,c,d) | a <- d1, b <- d2, c <- d3, d <- d4]

-- DR6 Solution
forall' :: [a] -> (a -> Bool) -> Bool
forall' = flip all -- the function already exists, we only have to flip it
exists' :: Int -> [a] -> (a -> Bool) -> Bool
exists' n l f = (n<=) . length . filter id $ map f l -- this should be made lazier

main = do
    -- There exists 2 numbers in the domain of {0..4} that are greater than 2.
    print $ askQ (EX 2 [1..4] id $ P (>2)) [0..4]
    let abc = ['a'..'z']
    -- No letter exists that is a blank space
    print $ askQ (UQ abc id $ P (/= ' ')) abc
    let classes = ["Math","English","Science","Art"]
        students = ["Tom","Bill","Sarah","Rose"]
        enrollment =
            [("Math","Sarah")
            ,("Math","Bill")
            ,("English","Bill")
            ,("English","Rose")
            ,("Science","Rose")
            ,("Science","Tom")
            ,("Art","Tom")
            ,("Art","Sarah")
            ]
    -- For each class there exists 2 students that have enrolled in that class.
    print $ askQ (UQ classes fst $ EX 2 students snd $ P (\e -> e `elem` enrollment)) [(c,s) | c <- classes, s <- students]
    print $ ask2 UQ classes (EX 2) students (`elem` enrollment)
    -- Testing DR6 Solution
    let enrol = [["Tom","Bill"],["Tom","Bill"],["Sarah","Rose"],["Bill","Sarah","Rose"]] 
    print $ forall' enrol
        $ \c -> exists' 2 students $ \s -> s `elem` c