{-# OPTIONS -W #-} {-# LANGUAGE TypeFamilies, FlexibleContexts, NoMonomorphismRestriction #-} module Lambda.Semantics where -- | Here we encode the "target language", the language -- to express denotations (or, meanings) -- Following Montague, our language for denotations -- is essentially Church's "Simple Theory of Types" -- also known as simply-typed lambda-calculus -- It is a form of a higher-order predicate logic. -- data Entity = John | Mary deriving (Eq, Show) -- | We define the grammar of the target language the same way -- we have defined the grammar for (source) fragment -- class Lambda lrepr where john' :: lrepr Entity mary' :: lrepr Entity like' :: lrepr (Entity -> Entity -> Bool) own' :: lrepr (Entity -> Entity -> Bool) farmer':: lrepr (Entity -> Bool) donkey':: lrepr (Entity -> Bool) true :: lrepr Bool neg :: lrepr Bool -> lrepr Bool conj :: lrepr Bool -> lrepr Bool -> lrepr Bool exists :: lrepr ((Entity -> Bool) -> Bool) app :: lrepr (a -> b) -> lrepr a -> lrepr b lam :: (lrepr a -> lrepr b) -> lrepr (a -> b) -- Examples lsen1 = neg (conj (neg (neg true)) (neg true)) lsen2 = lam (\x -> neg x) lsen3 = app (lam (\x -> neg x)) true disj x y = neg (conj (neg x) (neg y)) -- disj true (neg true) ldisj = lam (\x -> lam (\y -> disj x y)) lsen4 = disj true (neg true) lsen4' = app (app ldisj true) (neg true) lsen5 = app exists (lam (\x -> app (app like' mary') x)) -- | Syntactic sugar exists_ r = lam (\p -> app exists (lam (\x -> conj (app r x) (app p x) )) ) forall_ r = lam (\p -> neg (app exists (lam (\x -> conj (app r x) (neg (app p x)))))) forall = forall_ (lam (\_ -> true)) -- | The first interpretation: evaluating in the world with John, Mary, -- and Bool as truth values. -- Lambda functions are interpreted as Haskell functions and Lambda -- applications are interpreted as Haskell applications. -- The interpreter R is metacircular (and so, efficient). -- data R a = R { unR :: a } instance Lambda R where john' = R John mary' = R Mary like' = R (\o s -> elem (s,o) [(John,Mary), (Mary,John)]) own' = R (\o s -> elem (s,o) [(Mary,John)]) farmer' = R (\s -> s == Mary) donkey' = R (\s -> s == John) true = R True neg (R True) = R False neg (R False) = R True conj (R True) (R True) = R True conj _ _ = R False exists = R (\f -> any f domain) app (R f) (R x) = R (f x) lam f = R (\x -> unR (f (R x))) domain = [John, Mary] instance (Show a) => Show (R a) where show (R x) = show x -- | "Running" the examples lsen1_r = lsen1 :: R Bool lsen2_r = lsen2 :: R (Bool -> Bool) lsen3_r = lsen3 :: R Bool ldisj_r = ldisj :: R (Bool -> Bool -> Bool) lsen4_r = lsen4 :: R Bool lsen4'_r = lsen4' :: R Bool lsen5_r = lsen5 :: R Bool -- | We now interpret Lambda terms as Strings, so we can show -- our formulas. -- Actually, not quite strings: we need a bit of _context_: -- the precedence and the number of variables already bound in the context. -- The latter number lets us generate unique variable names. -- data C a = C { unC :: Int -> Int -> String } instance Lambda C where john' = C (\_ _ -> "john'") mary' = C (\_ _ -> "mary'") like' = C (\_ _ -> "like'") own' = C (\_ _ -> "own'") farmer' = C (\_ _ -> "farmer'") donkey' = C (\_ _ -> "donkey'") true = C (\_ _ -> "T") neg (C x) = C (\i p -> paren (p > 10) ("-" ++ x i 11)) conj (C x) (C y) = C (\i p -> paren (p > 3) (x i 4 ++ " & " ++ y i 3)) exists = C (\_ _ -> "E") app (C f) (C x) = C (\i p -> paren (p > 10) (f i 10 ++ " " ++ x i 11)) lam f = C (\i p -> let x = "x" ++ show i body = unC (f (C (\_ _ -> x))) (i + 1) 0 in paren (p > 0) ("L" ++ x ++ ". " ++ body)) instance Show (C a) where show (C x) = x 1 0 paren True text = "(" ++ text ++ ")" paren False text = text -- | We can now see the examples -- lsen1_c = lsen1 :: C Bool lsen2_c = lsen2 :: C (Bool -> Bool) lsen3_c = lsen3 :: C Bool ldisj_c = ldisj :: C (Bool -> Bool -> Bool) -- | The displayed difference between lsen4 and lsen4' -- shows that beta-redices have been reduced. NBE. lsen4_c = lsen4 :: C Bool lsen4'_c = lsen4' :: C Bool lsen5_c = lsen5 :: C Bool -- | Normalizing the terms: performing the apparent redices -- type family Known (lrepr :: * -> *) (a :: *) type instance Known lrepr (a -> b) = P lrepr a -> P lrepr b type instance Known lrepr Bool = [lrepr Bool] data P lrepr a = P { unP :: lrepr a, known :: Maybe (Known lrepr a) } instance (Lambda lrepr) => Lambda (P lrepr) where john' = unknown john' mary' = unknown mary' like' = unknown like' own' = unknown own' farmer' = unknown farmer' donkey' = unknown donkey' true = P true (Just []) neg (P x _) = unknown (neg x) conj x (P _ (Just [])) = x conj x y = let conjuncts (P _ (Just zs)) = zs conjuncts (P z Nothing) = [z] in P (foldr conj (unP y) (conjuncts x)) (Just (conjuncts x ++ conjuncts y)) exists = unknown exists app (P _ (Just f)) x = f x app (P f Nothing ) (P x _) = unknown (app f x) lam f = P (lam (\x -> unP (f (unknown x)))) (Just f) instance (Show (lrepr a)) => Show (P lrepr a) where show (P x _) = show x unknown x = P x Nothing -- | Now we can see beautified terms -- lsen1_pc = lsen1 :: (P C) Bool lsen2_pc = lsen2 :: (P C) (Bool -> Bool) lsen3_pc = lsen3 :: (P C) Bool ldisj_pc = ldisj :: (P C) (Bool -> Bool -> Bool) -- | There is no longer difference between lsen4 and lsen4' lsen4_pc = lsen4 :: (P C) Bool lsen4'_pc = lsen4' :: (P C) Bool lsen5_pc = lsen5 :: (P C) Bool