public
Last active

Quantifiers

  • Download Gist
gistfile1.hs
Haskell
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
{-# 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

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.