module MCWPL where
import Data.List
import FSynF
import Model
type LF = Formula Term
lfSent :: Sent -> LF
lfSent (Sent np vp) = (lfNP np) (lfVP vp)
lfNP :: NP -> (Term -> LF) -> LF
lfNP SnowWhite = \ p -> p (Struct "SnowWhite" [])
lfNP Alice = \ p -> p (Struct "Alice" [])
lfNP Dorothy = \ p -> p (Struct "Dorothy" [])
lfNP Goldilocks = \ p -> p (Struct "Goldilocks" [])
lfNP LittleMook = \ p -> p (Struct "LittleMook" [])
lfNP Atreyu = \ p -> p (Struct "Atreyu" [])
lfNP (NP1 det cn) = (lfDET det) (lfCN cn)
lfNP (NP2 det rcn) = (lfDET det) (lfRCN rcn)
lfVP :: VP -> Term -> LF
lfVP Laughed = \ t -> Atom "laugh" [t]
lfVP Cheered = \ t -> Atom "cheer" [t]
lfVP Shuddered = \ t -> Atom "shudder" [t]
lfVP (VP1 tv np) =
\ subj -> lfNP np (\ obj -> lfTV tv (subj,obj))
lfVP (VP2 dv np1 np2) =
\ subj -> lfNP np1 (\ iobj -> lfNP np2 (\ dobj ->
lfDV dv (subj,iobj,dobj)))
lfTV :: TV -> (Term,Term) -> LF
lfTV Loved = \ (t1,t2) -> Atom "love" [t1,t2]
lfTV Admired = \ (t1,t2) -> Atom "admire" [t1,t2]
lfTV Helped = \ (t1,t2) -> Atom "help" [t1,t2]
lfTV Defeated = \ (t1,t2) -> Atom "defeat" [t1,t2]
lfDV :: DV -> (Term,Term,Term) -> LF
lfDV Gave = \ (t1,t2,t3) -> Atom "give" [t1,t2,t3]
lfCN :: CN -> Term -> LF
lfCN Girl = \ t -> Atom "girl" [t]
lfCN Boy = \ t -> Atom "boy" [t]
lfCN Princess = \ t -> Atom "princess" [t]
lfCN Dwarf = \ t -> Atom "dwarf" [t]
lfCN Giant = \ t -> Atom "giant" [t]
lfCN Wizard = \ t -> Atom "wizard" [t]
lfCN Sword = \ t -> Atom "sword" [t]
lfCN Dagger = \ t -> Atom "dagger" [t]
lfDET :: DET -> (Term -> LF) -> (Term -> LF) -> LF
bInLF :: LF -> [Int]
bInLF (Atom _ _) = []
bInLF (Eq _ _) = []
bInLF (Neg lf) = bInLF lf
bInLF (Impl lf1 lf2) = bInLFs [lf1,lf2]
bInLF (Equi lf1 lf2) = bInLFs [lf1,lf2]
bInLF (Conj lfs) = bInLFs lfs
bInLF (Disj lfs) = bInLFs lfs
bInLF (Forall (Variable _ [i]) f) = i : bInLF f
bInLF (Exists (Variable _ [i]) f) = i : bInLF f
bInLFs :: [LF] -> [Int]
bInLFs = nub . concat . map bInLF
freshIndex :: [LF] -> Int
freshIndex lfs = i+1
where i = maximum (0:(bInLFs lfs))
fresh :: [Term -> LF] -> Int
fresh preds = freshIndex (map ($ dummy) preds)
where dummy = Struct "" []
lfDET Some p q = Exists v (Conj [p (Var v), q (Var v)])
where v = Variable "x" [fresh[p,q]]
lfDET Every p q = Forall v (Impl (p (Var v)) (q (Var v)))
where v = Variable "x" [fresh[p,q]]
lfDET No p q = Neg (Exists v (Conj [p (Var v),q (Var v)]))
where v = Variable "x" [fresh[p,q]]
lfDET The p q = Exists v1 (Conj
[Forall v2 (Equi (p (Var v2))
(Eq (Var v1) (Var v2))),
q (Var v1)])
where
i = fresh[p,q]
v1 = Variable "x" [i]
v2 = Variable "x" [i+1]
lfRCN :: RCN -> Term -> LF
lfRCN (RCN1 cn _ vp) = \ t -> Conj [lfCN cn t, lfVP vp t]
lfRCN (RCN2 cn _ np tv) = \ t -> Conj [lfCN cn t,
lfNP np (\ subj -> lfTV tv (subj,t))]
lf1 = lfSent (Sent (NP1 Some Dwarf)
(VP1 Defeated (NP1 Some Giant)))
lf2 = lfSent (Sent (NP2 The (RCN2 Wizard
That Dorothy Admired))
Laughed)
lf3 = lfSent (Sent (NP2 The (RCN1 Princess
That (VP1 Helped Alice)))
Shuddered)
type Interp a = String -> [a] -> Bool
int0 :: Interp Entity
int0 "Laugh" = \ [x] -> laugh x
int0 "Cheer" = \ [x] -> cheer x
int0 "Shudder" = \ [x] -> shudder x
int0 "Love" = \ [x,y] -> love y x
int0 "Admire" = \ [x,y] -> admire y x
int0 "Help" = \ [x,y] -> help y x
int0 "Defeat" = \ [x,y] -> defeat y x
int0 "Give" = \ [x,y,z] -> give z y x
type Lookup a = Variable -> a
change :: Lookup a -> Variable -> a -> Lookup a
change g x d = \ v -> if x == v then d else g v
ass0 :: Lookup Entity
ass0 = \ v -> A
ass1 :: Lookup Entity
ass1 = change ass0 y B
eval :: Eq a =>
[a] ->
Interp a ->
Lookup a ->
Formula Variable -> Bool
eval domain i = eval' where
eval' g (Atom str vs) = i str (map g vs)
eval' g (Eq v1 v2) = (g v1) == (g v2)
eval' g (Neg f) = not (eval' g f)
eval' g (Impl f1 f2) = not ((eval' g f1) &&
not (eval' g f2))
eval' g (Equi f1 f2) = (eval' g f1) == (eval' g f2)
eval' g (Conj fs) = and (map (eval' g) fs)
eval' g (Disj fs) = or (map (eval' g) fs)
eval' g (Forall v f) = and [ eval' (change g v d) f |
d <- domain ]
eval' g (Exists v f) = or [ eval' (change g v d) f |
d <- domain ]
int1 :: String -> [Int] -> Bool
int1 "R" = rconvert (<)
where
rconvert :: (a -> a -> Bool) -> [a] -> Bool
rconvert r [x,y] = r x y
ass2 :: Variable -> Int
ass2 v = if v == x then 1 else if v == y then 2 else 0
type FInterp a = String -> [a] -> a
zero = Struct "zero" []
fint1 :: FInterp Int
fint1 "zero" [] = 0
fint1 "s" [i] = succ i
fint1 "plus" [i,j] = i + j
fint1 "times" [i,j] = i * j
type TVal a = Term -> a
liftLookup :: FInterp a -> Lookup a -> TVal a
liftLookup fint g (Var v) = g v
liftLookup fint g (Struct str ts) =
fint str (map (liftLookup fint g) ts)
evl :: Eq a =>
[a] ->
Interp a ->
FInterp a ->
Lookup a ->
Formula Term -> Bool
evl domain i fint = evl' where
lift = liftLookup fint
evl' g (Atom str ts) = i str (map (lift g) ts)
evl' g (Eq t1 t2) = lift g t1 == lift g t2
evl' g (Neg f) = not (evl' g f)
evl' g (Impl f1 f2) = not ((evl' g f1) &&
not (evl' g f2))
evl' g (Equi f1 f2) = evl' g f1 == evl' g f2
evl' g (Conj fs) = and (map (evl' g) fs)
evl' g (Disj fs) = or (map (evl' g) fs)
evl' g (Forall v f) = and [ evl' (change g v d) f |
d <- domain ]
evl' g (Exists v f) = or [ evl' (change g v d) f |
d <- domain ]
formula3 = Forall x (Forall y (Impl (Atom "R" [tx,ty])
(Exists z
(Conj [Atom "R" [tx,tz],
Atom "R" [tz,ty]]))))
formula4 = Impl (Atom "R" [tx,ty])
(Exists z
(Conj [Atom "R" [tx,tz],
Atom "R" [tz,ty]]))
int3 :: String -> [Entity] -> Bool
int3 "R" = \ [x,y] -> defeat y x
fint2 :: String -> [Entity] -> Entity
fint2 "zero" [] = A