module MCWPL where
import Data.List
import FSynF
import Model
-- logical formulas -- what english will be translated to.
type LF = Formula Term
-- translate sentence to logical formula
lfSent :: Sent -> LF
lfSent (Sent np vp) = (lfNP np) (lfVP vp)
-- translate noun phrase
-- meaning of noun phrase has type (Term -> LF) -> LF
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)
-- translate verb phrases
-- meaning of verb phrase has type Term -> LF
lfVP :: VP -> Term -> LF
lfVP Laughed = \ t -> Atom "laugh" [t]
lfVP Cheered = \ t -> Atom "cheer" [t]
lfVP Shuddered = \ t -> Atom "shudder" [t]
-- handle Verb phrases with transitive and ditransitive verbs
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)))
-- Translate transitive verbs
-- meaning of transitive verb has type (Term,Term) -> LF
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]
-- Translate ditransitive verbs
-- meaning of ditransitive verb is (Term,Term,Term) -> LF
lfDV :: DV -> (Term,Term,Term) -> LF
lfDV Gave = \ (t1,t2,t3) -> Atom "give" [t1,t2,t3]
-- Translate common nouns
-- Meaning of common noun has type Term -> LF
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]
-- The type of determiners
lfDET :: DET -> (Term -> LF) -> (Term -> LF) -> LF
-- Helper functions:
-- Collecting indices of binding occurrences of variables
-- I.e., subscripts of those variables in the scope of a quantifier
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
-- Create an index not occurring in the parameter list
freshIndex :: [LF] -> Int
freshIndex lfs = i+1
where i = maximum (0:(bInLFs lfs))
-- Creative fresh variable not in the parameter list
fresh :: [Term -> LF] -> Int
fresh preds = freshIndex (map ($ dummy) preds)
where dummy = Struct "" []
-- Translated determiners
-- When translate make sure all bound variables are new to avoid capture
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]
-- Translate a common noun with the associated relative clause
-- meaning has same type as a plain common nount
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))]
-- Some sample sentences
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)
-- Section 6.4
-- The imported module Model provides a model for the language defined
-- in FSynF. Code in this section uses this model to interpret predicate
-- logic formulas that are the meanings of our natural language subset.
-- by providing the function I to interpret n-relations
-- Interp takes a string (the name of the relation) and an
-- n-tuple of values and says whether the relation is true or false
-- of that n-tuple
type Interp a = String -> [a] -> Bool
-- Interpretations of one place and two place relations
-- unary relations are interpreted as characteristic functions of one argument
-- binary relations are interpreted as characteristic functions of a pair of arguments
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 "sdmire" = \ [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
int0 "princess" = \ [x] -> princess x
-- Variable assignments for the model
-- function g that tells meaning of variables in formula
type Lookup a = Variable -> a
-- Update a variable assignment
-- change g x d updates g so x now has meaning d
change :: Lookup a -> Variable -> a -> Lookup a
change g x d = \ v -> if x == v then d else g v
-- A boring variable assignment that maps everything to element A
ass0 :: Lookup Entity
ass0 = \ v -> A
-- A slightly less boring variable assignment that maps y to B
-- and everything else to A
ass1 :: Lookup Entity
ass1 = change ass0 y B
-- The type of an evaluation function for predicate logic
-- The arguments are a domain (represented as a list), an interpretation function,
-- a variable assignment and a formula. It returns a Boolean value.
-- This particular interpretation function does not handle terms.
-- As a result we'll actually use evl from farther down
eval :: Eq a =>
[a] ->
Interp a ->
Lookup a ->
Formula Variable -> Bool
eval domain i = eval' where
-- eval' has frozen the domain and interpretation function
-- Its arguments are q variable assignment and a formula
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 ]
-- Interpret R as less than
int1 :: String -> [Int] -> Bool
int1 "R" = rconvert (<)
where
rconvert :: (a -> a -> Bool) -> [a] -> Bool
rconvert r [x,y] = r x y
-- An assignment where x is less than y
ass2 :: Variable -> Int
ass2 v = if v == x then 1 else if v == y then 2 else 0
-- In this section we add more complicated terms to language
type FInterp a = String -> [a] -> a
-- The constant zero
zero = Struct "zero" []
-- Interpreting arithmetic functions
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
-- Extend variable assignments to assign values to terms
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)
-- Evaluating a formula in a model requires a domain parameter, an
-- interpretation of relation symbols, an interpretation of functions symbols,
-- a variable assignment and a formula
evl :: Eq a =>
[a] ->
Interp a ->
FInterp a ->
Lookup a ->
Formula Term -> Bool
-- Evaluation function for a language that includes function symbols
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 ]
-- Sample formulas to evaluate
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