diff --git a/Lambda/CCG.hs b/Lambda/CCG.hs new file mode 100644 --- /dev/null +++ b/Lambda/CCG.hs @@ -0,0 +1,211 @@ +{-# LANGUAGE TypeOperators, EmptyDataDecls, NoMonomorphismRestriction #-} +{-# LANGUAGE TypeFamilies, FlexibleInstances #-} + +-- | Combinatorial Categorical Grammar (CCG) +-- +-- +-- + +module Lambda.CCG where + +import Prelude hiding ((/)) + +import Lambda.Semantics + +-- Abstract and concrete syntax + +-- | Syntactic categories: non-terminals of CCG +-- +data S -- clause +data NP -- noun phrase +data b :/ a +data b :\\ a + +-- | This class defines the syntax of our fragment (the grammar, +-- essentially). Its instances will show interpretations +-- of the grammar, or `semantics' +-- +class Symantics repr where + john :: repr NP + mary :: repr NP + like :: repr ((NP :\\ S) :/ NP) + (/) :: repr (b :/ a) -> repr a -> repr b + (\\) :: repr a -> repr (a :\\ b) -> repr b + +-- | show the inferred types, as well as the inferred types for +-- phrases like +phrase1 = like / mary +-- phrase1 :: (Symantics repr) => repr (S :\\ NP) + +-- show the type errors from like \\ mary +{- +err1 = like \\ mary + + Couldn't match expected type `b :\\ (NP :/ (S :\\ NP))' + against inferred type `NP' + Expected type: repr (b :\\ (NP :/ (S :\\ NP))) + Inferred type: repr NP + In the second argument of `(\\)', namely `mary' + In the expression: like \\ mary +-} + + + +-- | The first sample sentence, or CCG derivation +-- The inferred type is S. So, sen1 is a derivations of +-- a complete sentence. +sen1 = john \\ (like / mary) + +-- | We now define the first interpretation of a CCG derivations: +-- We interpret the derivation to give the parsed string. +-- That is, we generate a yield of a CCG derivation, +-- in English. +-- +-- We represent each node in the derivation tree +-- by an English phrase +data EN a = EN{unEN:: String} + +instance Symantics EN where + john = EN "John" + mary = EN "Mary" + like = EN "likes" + (EN f) / (EN x) = EN (f ++ " " ++ x) + (EN x) \\ (EN f) = EN (x ++ " " ++ f) + +instance Show (EN a) where + show = unEN + +-- | Show the English form of sen1 +sen1_en = sen1 :: EN S + +-- Try phonetic (using IPA) + +-- | We now define semantics of a phrase represented +-- by a derivation. It is a different interpretation +-- of the phrase and its types. +-- +-- We first interpret syntactic types (NP, slashes, etc) +-- in terms of the types of the language of +-- logic formulas. +-- The type class Lambda defines the language +-- of logic formulas (STT, or higher-order logic) +-- with types Entity, Bool, and the arrows. +-- +type family Tr (synt :: *) :: * +type instance Tr S = Bool +type instance Tr NP = Entity +type instance Tr (b :/ a) = Tr a -> Tr b +type instance Tr (a :\\ b) = Tr a -> Tr b + +data Sem lrepr a = Sem { unSem :: lrepr (Tr a) } + +instance (Lambda lrepr) => Symantics (Sem lrepr) where + john = Sem john' + mary = Sem mary' + like = Sem like' + (Sem f) / (Sem x) = Sem (app f x) + (Sem x) \\ (Sem f) = Sem (app f x) + +instance Show (Sem C a) where + show (Sem x) = show x + +instance Show (Sem (P C) a) where + show (Sem x) = show x + +-- | We can now see the semantics of sen1 +sen1_sem = sen1 :: Sem C S + +-- | Computing the yield in Japanese +-- +-- The type family TJ defines the types of +-- sentential forms corresponding to syntactic categories. +-- +-- We represent each node in the derivation tree +-- by a Japanese phrase or a Japanese "sentential form" +-- (that is, a phrase with holes). Contrast with the EN +-- interpreter above. +-- +data JA a = JA { unJA :: TJ a } + +type family TJ (a :: *) :: * +type instance TJ S = String +type instance TJ NP = String +type instance TJ (b :/ a) = TJ a -> TJ b +type instance TJ (a :\\ b) = TJ a -> TJ b + +-- | The following works but is unsatisfactory: we wish +-- slashes to be interpreted only as concatenation! +instance Symantics JA where + john = JA "ジョンさん" + mary = JA "メリさん" + like = JA (\o s -> s ++ "は" ++ o ++ "のことが" ++ "好きだ") + (JA f) / (JA x) = JA (f x) + (JA x) \\ (JA f) = JA (f x) + +instance Show (JA S) where + show = unJA + +-- | The translation is certainly different: "like" corresponds +-- to an adjective in Japanese. +sen1_ja = sen1 :: JA S + + +-- | Adding quantification; one way +-- +type QNP = (S :/ (NP :\\ S)) -- Quantified noun phrase + +-- | We extend our earlier fragment with quantifiers everyone, someone +-- We also add a combinator for raising the first argument of a TV +-- +class (Symantics repr) => Quantifier repr where + everyone :: repr QNP + someone :: repr QNP + lift_vt :: repr ((NP :\\ S) :/ NP) -> repr ((NP :\\ S) :/ QNP) + +sen2 = everyone / (like / mary) +-- sen2 :: (Quantifier repr) => repr S + +-- | But how to put a quantifier in an object position? +sen3 = john \\ ((lift_vt like) / someone) + +sen4 = everyone / ((lift_vt like) / someone) + +instance Quantifier EN where + everyone = EN "everyone" + someone = EN "someone" + lift_vt (EN f) = EN f + + +sen2_en = sen2 :: EN S + +sen3_en = sen3 :: EN S + +sen4_en = sen4 :: EN S + +instance (Lambda lrepr) => Quantifier (Sem lrepr) where + everyone = Sem forall + someone = Sem exists + lift_vt (Sem verb) = Sem (lam (\q -> lam (\s -> + app q (lam $ \obj -> app (app verb obj) s)))) + +sen2_sem = sen2 :: Sem C S -- The result is not normalized +sen3_sem = sen3 :: Sem C S +sen4_sem = sen4 :: Sem C S + +sen2_semp = sen2 :: Sem (P C) S -- We need normalization +sen3_semp = sen3 :: Sem (P C) S +sen4_semp = sen4 :: Sem (P C) S + + +-- | Japanese is challenging: like semantics +-- +-- The expression for quantifiers ensures that no +-- inverse reading is possible. Only linear reading. +instance Quantifier JA where + everyone = JA (\k -> k "みんな") + someone = JA (\k -> k "ある人") + lift_vt (JA verb) = JA (\q s -> q (\obj -> verb obj s)) + +sen2_ja = sen2 :: JA S +sen3_ja = sen3 :: JA S +sen4_ja = sen4 :: JA S diff --git a/Lambda/CFG.hs b/Lambda/CFG.hs new file mode 100644 --- /dev/null +++ b/Lambda/CFG.hs @@ -0,0 +1,116 @@ +{-# LANGUAGE EmptyDataDecls, NoMonomorphismRestriction #-} +{-# LANGUAGE TypeFamilies, FlexibleInstances #-} + +-- | Context-free grammars, in the tagless-final style +-- +-- +-- +module Lambda.CFG where + +import Lambda.Semantics + +-- | Syntactic categories: non-terminals of CFG +-- +data S -- clause +data NP -- noun phrase +data VP -- verb phrase +data TV -- transitive verb + +-- | This class defines the syntax of our fragment (the grammar, +-- essentially). Its instances will show interpretations +-- of the grammar, or `semantics' +-- +-- The names r1, r2, etc. are the labels of CFG rules. +-- These names are evocative of Montague +-- +class Symantics repr where + john :: repr NP + mary :: repr NP + like :: repr TV + own :: repr TV + r2 :: repr TV -> repr NP -> repr VP + r1 :: repr NP -> repr VP -> repr S + +-- | show the inferred types, as well as the inferred types for +-- the phrases like +phrase1 = r2 like mary +{- +*CFG> :t phrase1 +phrase1 :: (Symantics repr) => repr VP +-} + +-- show the type errors from +{- +err1 = r1 like mary + Couldn't match expected type `NP' against inferred type `TV' + Expected type: repr NP + Inferred type: repr TV + In the first argument of `r1', namely `like' + In the expression: r1 like mary +-} + +-- | The first sample sentence, or CFG derivation +-- The inferred type is S. So, sen1 is a derivations of +-- a complete sentence. +-- +sen1 = r1 john (r2 like mary) + +-- | We now define the first interpretation of a CFG derivations: +-- We interpret the derivation to give the parsed string. +-- That is, we generate a yield of a CFG derivation, +-- in English. +-- +-- We represent each node in the derivation tree +-- by an English phrase +data EN a = EN { unEN :: String } + +instance Symantics EN where + john = EN "John" + mary = EN "Mary" + like = EN "likes" + own = EN "owns" + r2 (EN f) (EN x) = EN (f ++ " " ++ x) + r1 (EN x) (EN f) = EN (x ++ " " ++ f) + +instance Show (EN a) where + show = unEN + +-- | Show the English form of sen1 +sen1_en = sen1 :: EN S + +-- | We now define semantics of a phrase represented +-- by a derivation. It is a different interpretation +-- of the phrase and its types. +-- +-- We first interpret syntactic types (NP, VP, etc) +-- in terms of the types of the language of +-- logic formulas. +-- The type class Lambda defines the language +-- of logic formulas (STT, or higher-order logic) +-- with types Entity, Bool, and the arrows. +-- +type family Tr (a :: *) :: * +type instance Tr S = Bool +type instance Tr NP = Entity +type instance Tr VP = Entity -> Bool +type instance Tr TV = Entity -> Entity -> Bool + +data Sem lrepr a = Sem { unSem :: lrepr (Tr a) } + +instance (Lambda lrepr) => Symantics (Sem lrepr) where + john = Sem john' + mary = Sem mary' + like = Sem like' + own = Sem own' + r2 (Sem f) (Sem x) = Sem (app f x) + r1 (Sem x) (Sem f) = Sem (app f x) + +instance Show (Sem C a) where + show (Sem x) = show x + +instance Show (Sem (P C) a) where + show (Sem x) = show x + +-- | We can now see the semantics of sen1 +sen1_sem = sen1 :: Sem C S + diff --git a/Lambda/CFG1EN.hs b/Lambda/CFG1EN.hs new file mode 100644 --- /dev/null +++ b/Lambda/CFG1EN.hs @@ -0,0 +1,15 @@ +-- +-- | +-- + +module Lambda.CFG1EN where + +-- | Definitions (or, bookmarks) and CFG-like derivations +-- +john = "John" +mary = "Mary" +like = "likes" +r2 f x = f ++ " " ++ x +r1 x f = x ++ " " ++ f + +sentence = r1 john (r2 like mary) diff --git a/Lambda/CFG1Sem.hs b/Lambda/CFG1Sem.hs new file mode 100644 --- /dev/null +++ b/Lambda/CFG1Sem.hs @@ -0,0 +1,33 @@ +-- +-- | +-- + +module Lambda.CFG1Sem where + +-- | Semantic interpretation of a CFG derivation +-- +-- In conventional notation: +-- +-- > D_e = {John, Mary} +-- +data Entity = John | Mary + deriving (Eq, Show) + +john = John +mary = Mary + +like o s = (o == John && s == Mary ) || + (o == Mary && s == John ) + +-- | A different way of writing it: by cases +like' Mary John = True +like' John Mary = True +like' _ _ = False + +r2 f x = f x +r1 x f = f x + +-- | sentence has the same form as in CFG1.hs, +-- but a different value (interpretation) +-- +sentence = r1 john (r2 like mary) diff --git a/Lambda/CFG2EN.hs b/Lambda/CFG2EN.hs new file mode 100644 --- /dev/null +++ b/Lambda/CFG2EN.hs @@ -0,0 +1,30 @@ +-- +-- | +-- +module Lambda.CFG2EN where + +-- | Type annotations +-- +john, mary :: String +like :: String +r2 :: String -> String -> String +r1 :: String -> String -> String + +john = "John" +mary = "Mary" +like = "likes" +r2 f x = f ++ " " ++ x +r1 x f = x ++ " " ++ f + +sentence :: String +sentence = r1 john (r2 like mary) + +-- | Unfortunately, the following sentence is, too, +-- accepted by the type checker. +-- +-- We shall later see how to build terms that correspond to +-- all and only valid derivations. +-- Invalid derivations will become ill-typed. +bad_sentence :: String +bad_sentence = r2 (r2 like mary) john + diff --git a/Lambda/CFG2Sem.hs b/Lambda/CFG2Sem.hs new file mode 100644 --- /dev/null +++ b/Lambda/CFG2Sem.hs @@ -0,0 +1,32 @@ +-- | + +module Lambda.CFG2Sem where + +-- | CFG1Sem with type annotations +-- +data Entity = John | Mary + deriving (Eq, Show) + +john, mary :: Entity +like :: Entity -> Entity -> Bool +r2 :: (Entity -> Entity -> Bool) -> Entity -> (Entity -> Bool) +r1 :: Entity -> (Entity -> Bool) -> Bool + +john = John +mary = Mary + +-- | A new notation for `like' (which will be convenient later) +like = \o s -> elem (s,o) [(John,Mary), (Mary,John)] + +r2 f x = f x +r1 x f = f x + +sentence :: Bool +sentence = r1 john (r2 like mary) + +-- In the Sem interpretation, the bad_sentence +-- is ill-typed, as it should. Note the error message +{- +bad_sentence :: Bool +bad_sentence = r2 (r2 like mary) john +-} diff --git a/Lambda/CFG3EN.hs b/Lambda/CFG3EN.hs new file mode 100644 --- /dev/null +++ b/Lambda/CFG3EN.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE EmptyDataDecls #-} + +-- | Introducing type constants +-- +-- We wish to outlaw terms such as bad_sentence in CFG2EN.hs, +-- even though there may be an interpretation that accepts +-- these bad terms. +-- We really wish our terms represent all and only +-- valid CFG derivations. We accomplish this goal here. +-- Our approach is reminiscent of LCF. + +module Lambda.CFG3EN where + +data S -- clause +data NP -- noun phrase +data VP -- verb phrase +data TV -- transitive verb + +-- | Parameterized types: cf notation: +-- +-- > in +-- +-- the Minimalist Grammar +-- +data EN a = EN { unEN :: String } + +-- | One may think of the above data declaration as defining an +-- isomorphism between EN values and Strings. The functions +-- EN and unEN (what is their type?) witness the isomorphism. +-- It helps to look at their composition. +-- +-- +john, mary :: EN NP +like :: EN TV +r2 :: EN TV -> EN NP -> EN VP +r1 :: EN NP -> EN VP -> EN S + +john = EN "John" +mary = EN "Mary" +like = EN "likes" +r2 (EN f) (EN x) = EN (f ++ " " ++ x) +r1 (EN x) (EN f) = EN (x ++ " " ++ f) + +instance Show (EN a) where + show = unEN + +sentence :: EN S +sentence = r1 john (r2 like mary) + +-- Now the bad_sentence is rejected already in +-- the EN interpretation, in contrast to CFG2EN.hs. +-- The type error message clearly describes the error, +-- in the CFG terms. +-- bad_sentence = r2 (r2 like mary) john diff --git a/Lambda/CFG3Sem.hs b/Lambda/CFG3Sem.hs new file mode 100644 --- /dev/null +++ b/Lambda/CFG3Sem.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE EmptyDataDecls, FlexibleInstances, TypeFamilies #-} + +-- | Type functions: interpretations of the type constants +-- +-- +-- + +module Lambda.CFG3Sem where + +data S -- clause +data NP -- noun phrase +data VP -- verb phrase +data TV -- transitive verb + +type family Tr (a :: *) :: * +type instance Tr S = Bool +type instance Tr NP = Entity +type instance Tr VP = Entity -> Bool +type instance Tr TV = Entity -> Entity -> Bool + +data Sem a = Sem { unSem :: Tr a } + +data Entity = John | Mary + deriving (Eq, Show) + +john, mary :: Sem NP +like :: Sem TV +r2 :: Sem TV -> Sem NP -> Sem VP +r1 :: Sem NP -> Sem VP -> Sem S + +john = Sem John +mary = Sem Mary +like = Sem (\o s -> elem (s,o) [(John,Mary), (Mary,John)]) +r2 (Sem f) (Sem x) = Sem (f x) +r1 (Sem x) (Sem f) = Sem (f x) + +instance Show (Sem S) where + show (Sem x) = show x + +sentence :: Sem S +sentence = r1 john (r2 like mary) + +-- How to tell if the result of evaluating the sentence +-- shows that John likes Mary or that Mary likes John? +-- We could trace the evaluation. +-- A better idea is to display the denotation as a formula +-- rather than as its value in one particular world. diff --git a/Lambda/CFG4.hs b/Lambda/CFG4.hs new file mode 100644 --- /dev/null +++ b/Lambda/CFG4.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE EmptyDataDecls, NoMonomorphismRestriction #-} +{-# LANGUAGE TypeFamilies, FlexibleInstances #-} + +-- | Unifying syntax with semantics +-- +module Lambda.CFG4 where + +data S -- clause +data NP -- noun phrase +data VP -- verb phrase +data TV -- transitive verb + +class Symantics repr where + john, mary :: repr NP + like :: repr TV + r2 :: repr TV -> repr NP -> repr VP + r1 :: repr NP -> repr VP -> repr S + +sentence = r1 john (r2 like mary) + +data EN a = EN { unEN :: String } + +instance Symantics EN where + john = EN "John" + mary = EN "Mary" + like = EN "likes" + r2 (EN f) (EN x) = EN (f ++ " " ++ x) + r1 (EN x) (EN f) = EN (x ++ " " ++ f) + +instance Show (EN a) where + show = unEN + +sentence_en = sentence :: EN S + +type family Tr (a :: *) :: * +type instance Tr S = Bool +type instance Tr NP = Entity +type instance Tr VP = Entity -> Bool +type instance Tr TV = Entity -> Entity -> Bool + +data Sem a = Sem { unSem :: Tr a } + +data Entity = John | Mary + deriving (Eq, Show) + +instance Symantics Sem where + john = Sem John + mary = Sem Mary + like = Sem (\o s -> elem (s,o) [(John,Mary), (Mary,John)]) + r2 (Sem f) (Sem x) = Sem (f x) + r1 (Sem x) (Sem f) = Sem (f x) + +instance Show (Sem S) where + show (Sem x) = show x + +sentence_sem = sentence :: Sem S diff --git a/Lambda/CFGJ.hs b/Lambda/CFGJ.hs new file mode 100644 --- /dev/null +++ b/Lambda/CFGJ.hs @@ -0,0 +1,68 @@ +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE TypeFamilies, FlexibleInstances #-} + +-- | Interpreting a CFG derivation as a string in Japanese. +-- That is, we generate a yield of a CFG derivation, +-- this time in Japanese. +-- +-- +-- +module Lambda.CFGJ where + +import Lambda.CFG -- we shall re-use our earlier work + +-- | We represent each node in the derivation tree +-- by a Japanese phrase or a Japanese "sentential form" +-- (that is, a phrase with holes). Contrast with the EN +-- interpreter in CFG.hs +-- +data JA a = JA { unJA :: TJ a } + +-- | A verb or a verb-like word (e.g., an i-adjective) require +-- arguments of particular cases. We need a way for a verb +-- to specify the desired case of its arguments. +-- +data Case = Nom | NomStrong | Acc +case_particle :: Case -> String +case_particle Nom = "は" +case_particle NomStrong = "のことが" +case_particle Acc = "を" + + +-- | The type family TJ defines the types of +-- sentential forms corresponding to syntactic categories. +-- +-- As we shall see in QCFGJ.hs, we are going to need +-- high (raised) types of our NP. +-- A verb will ask its argument to turn itself to the +-- desired case. +type SK = (String -> String) -> String + +type family TJ (a :: *) :: * +type instance TJ S = String +type instance TJ NP = Case -> SK +type instance TJ VP = (Case -> SK) -> String +type instance TJ TV = (Case -> SK) -> (Case -> SK) -> String + +-- | Auxiliary functions for the code below +make_np :: String -> (Case -> SK) +make_np str cas k = k (str ++ case_particle cas) + +make_tv :: String -> Case -> Case -> (Case -> SK) -> (Case -> SK) -> String +make_tv str co cs o s = + s cs (\sv -> o co (\ov -> sv ++ ov ++ str)) + +instance Symantics JA where + john = JA (make_np "ジョンさん") + mary = JA (make_np "メリさん") + like = JA (make_tv "好きだ" NomStrong Nom) + own = JA (make_tv "飼っている" Acc Nom) + r2 (JA f) (JA x) = JA (f x) + r1 (JA x) (JA f) = JA (f x) + +instance Show (JA S) where + show = unJA + +-- | The translation is certainly different: "like" corresponds +-- to an adjective in Japanese. +sen1_ja = sen1 :: JA S diff --git a/Lambda/Dynamics.hs b/Lambda/Dynamics.hs new file mode 100644 --- /dev/null +++ b/Lambda/Dynamics.hs @@ -0,0 +1,99 @@ +{-# OPTIONS -W #-} +{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #-} +{-# LANGUAGE NoMonomorphismRestriction #-} + +-- | Philippe de Groote. 2010. Dynamic logic: a type-theoretic view. +-- Talk slides at `Le modèle et l'algorithme', Rocquencourt. +-- +-- + +module Lambda.Dynamics where + +import Lambda.Semantics +import Lambda.CFG +import Lambda.QCFG + +-- | We extend the Lambda language with state (of the type State) +type State = [Entity] +class (Lambda lrepr) => States lrepr where + update :: lrepr Entity -> lrepr State -> lrepr State + select :: lrepr State -> lrepr Entity + +-- | We correspondingly extend our R, C, P intrepreters of Lambda +instance States R where + update (R x) (R e) = R (x:e) + select (R (x:_)) = R x + select (R []) = error "who?" + +instance States C where + update (C x) (C e) = C (\i p -> paren (p > 5) (x i 6 ++ "::" ++ e i 5)) + select (C e) = C (\i p -> paren (p > 10) ("sel " ++ e i 11)) + +instance (States lrepr) => States (P lrepr) where + update (P x _) (P e _) = unknown (update x e) + select (P e _) = unknown (select e) + +type family Dynamic (a :: *) +type instance Dynamic (a -> b) = Dynamic a -> Dynamic b +type instance Dynamic Entity = Entity +type instance Dynamic Bool = State -> (State -> Bool) -> Bool +data D c a = D { unD :: c (Dynamic a) } +instance (States c) => Lambda (D c) where + app (D f) (D x) = D (app f x) + lam f = D (lam (\x -> unD (f (D x)))) + john' = D john' + mary' = D mary' + like' = D (dynamic (\_ -> like')) + own' = D (dynamic (\_ -> own')) + farmer' = D (dynamic (\_ -> farmer')) + donkey' = D (dynamic (\_ -> donkey')) + true = D (dynamic (\_ -> true)) + neg (D x) = D (dynamic (\e -> neg (static x e))) + conj (D x) (D y) = D (lam (\e -> lam (\phi -> app (app x e) + (lam (\e -> app (app y e) phi))))) + exists = D (lam (\p -> lam (\e -> lam (\phi -> app exists + (lam (\x -> app (app (app p x) (update x e)) phi)))))) +instance Show (Sem (D C) S) where + show = show . unSem +instance Show (Sem (D (P C)) S) where + show = show . unSem +instance Show (D C Bool) where + show (D x) = show x +instance Show (D (P C) Bool) where + show (D x) = show x +class Predicate a where + dynamic :: (Lambda lrepr) => (lrepr State -> lrepr a) -> lrepr (Dynamic a) + static :: (Lambda lrepr) => lrepr (Dynamic a) -> lrepr State -> lrepr a +instance Predicate Bool where + dynamic f = lam (\e -> lam (\phi -> conj (f e) (app phi e))) + static x e = app (app x e) (lam (\_ -> true)) +instance (Predicate a) => Predicate (Entity -> a) where + dynamic f = lam (\o -> dynamic (\e -> app (f e) o)) + static x e = lam (\o -> static (app x o) e) + +class (Lambda lrepr) => Dynamics lrepr where + it' :: lrepr ((Entity -> Bool) -> Bool) + +instance (States lrepr) => Dynamics (D lrepr) where + it' = D (lam (\p -> lam (\e -> lam (\phi -> + app (app (app p (select e)) e) phi)))) + +instance Dynamics C where + it' = C (\_ _ -> "it") + +instance (Dynamics lrepr) => Dynamics (P lrepr) where + it' = unknown it' + +class (Quantifier repr) => Pronoun repr where + it_ :: repr QNP + +instance Pronoun EN where + it_ = EN "it" + +instance (Dynamics lrepr) => Pronoun (Sem lrepr) where + it_ = Sem it' + +sentence = r4 (every (who (r5 own (a donkey)) farmer)) (r5 like it_) +sentence_en = sentence :: EN S +sentence_sem = sentence :: Sem (D C) S +sentence_semp = sentence :: Sem (D (P C)) S diff --git a/Lambda/QCFG.hs b/Lambda/QCFG.hs new file mode 100644 --- /dev/null +++ b/Lambda/QCFG.hs @@ -0,0 +1,108 @@ +{-# LANGUAGE EmptyDataDecls, NoMonomorphismRestriction #-} +{-# LANGUAGE TypeFamilies #-} + +-- | Context-free grammar with quantifiers +-- +-- We extend CFG.hs to add quantified noun phrases +-- in the tradition of Montague +-- +module Lambda.QCFG where + +import Lambda.Semantics +import Lambda.CFG -- we shall re-use our earlier work + +-- | Additional syntactic categories +-- +data CN -- Common noun +data QNP -- Quantified noun phrase + +-- | We extend our earlier fragment with common nouns farmer and donkey, +-- and quantifiers everyone, someone, every farmer, a donkey, etc. +-- Since we added two new categories (CN and QNP), we need to add rules +-- to our CFG to be able to use the categories in derivations. +-- +-- The numbers 4 and 5 are due to Montague +class (Symantics repr) => Quantifier repr where + farmer :: repr CN + donkey :: repr CN + everyone :: repr QNP + someone :: repr QNP + every :: repr CN -> repr QNP + a :: repr CN -> repr QNP + who :: repr VP -> repr CN -> repr CN + r5 :: repr TV -> repr QNP -> repr VP + r4 :: repr QNP -> repr VP -> repr S + +-- | Sample sentences (or, CFG derivations) +-- We stress that the inferred type of sen2-sen4 +-- is S. So, these are the derivations of +-- complete sentences. +sen2 = r4 everyone (r2 like mary) + +sen3 = r1 john (r5 like someone) + +sen4 = r4 everyone (r5 like someone) + +sen5 = r4 (every (who (r5 own (a donkey)) farmer)) (r5 like (a donkey)) + +-- | We extend our EN interpreter (interpreter of +-- derivations as English phrases) to deal +-- with QNP. +instance Quantifier EN where + farmer = EN "farmer" + donkey = EN "donkey" + everyone = EN "everyone" + someone = EN "someone" + every (EN n) = EN ("every " ++ n) + a (EN n) = EN ("a " ++ n) + who (EN r) (EN q) = EN (q ++ " who " ++ r) + r5 (EN f) (EN x) = EN (f ++ " " ++ x) + r4 (EN x) (EN f) = EN (x ++ " " ++ f) + +-- | We can now see the English sentences that +-- correspond to the derivations sen2-sen4. +sen2_en = sen2 :: EN S +sen3_en = sen3 :: EN S +sen4_en = sen4 :: EN S +sen5_en = sen5 :: EN S + +-- | We also extend the semantics interpreter: +-- the interpreter of a derivation into a +-- formula of STT, or Lambda-calculus. +-- +-- We add the interpretation of the categories CN and QNP, +-- following Montague +type instance Tr CN = Entity -> Bool +type instance Tr QNP = (Entity -> Bool) -> Bool + +instance (Lambda lrepr) => Quantifier (Sem lrepr) where + farmer = Sem farmer' + donkey = Sem donkey' + everyone = Sem forall + someone = Sem exists + every (Sem cn) = Sem (forall_ cn) + a (Sem cn) = Sem (exists_ cn) + who (Sem r) (Sem q) = Sem (lam (\x -> conj (app q x) (app r x))) + r5 (Sem tv) (Sem qnp) = Sem (lam (\s -> app qnp + (lam (\o -> app (app tv o) s)))) + r4 (Sem qnp) (Sem vp) = Sem (app qnp vp) + +-- | We can see the semantic yield of our derivations, +-- but the formulas are not reduced! +-- +sen2_sem = sen2 :: Sem C S +sen3_sem = sen3 :: Sem C S +sen4_sem = sen4 :: Sem C S +sen5_sem = sen5 :: Sem C S + +-- | the shown result of sen3_sem is a formula with +-- an apparent beta-redex. The formula can be simplified +-- (reduced) so it reads better. That's why we need the +-- partial evaluator. +sen3_semp = sen3 :: Sem (P C) S +sen5_semp = sen5 :: Sem (P C) S + +-- The shown result of sen4_sem shows the linear reading +-- (linear reading) of the quantifiers? +-- How to get an inverse reading? Montague shown +-- a general approach: see QHCFG.hs diff --git a/Lambda/QCFGJ.hs b/Lambda/QCFGJ.hs new file mode 100644 --- /dev/null +++ b/Lambda/QCFGJ.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE TypeFamilies, FlexibleInstances #-} + +-- | Interpreting a CFG derivation with quantifiers +-- as a string in Japanese. +-- That is, we generate a yield of a CFG derivation, +-- this time in Japanese. +-- +module Lambda.QCFGJ where + +import Lambda.QCFG -- we shall re-use our earlier work +import Lambda.CFGJ +import Lambda.CFG + +-- | We extend our JA interpreter (interpreter of +-- derivations as Japanese phrases) to deal +-- with QNP. +-- +type instance TJ CN = String + +-- | Quantifiers get the high type +-- In fact, the same type as TJ NP +-- +type instance TJ QNP = Case -> SK + +-- | The expression for quantifiers ensures that no +-- inverse reading is possible. Only linear reading. +instance Quantifier JA where + farmer = JA "農家" + donkey = JA "ロバ" + +-- every (JA n) = JA (\cas k -> k ("どの" ++ n ++ "も")) + every (JA n) = JA (\cas k -> k (n ++ case_particle cas ++ "みな")) + a (JA n) = JA (\cas k -> k ("ある" ++ n ++ case_particle cas)) + who (JA vp) (JA n) = JA (vp (\cas k -> k "") ++ n) + + everyone = JA (\cas k -> "みんな" ++ case_particle cas ++ k "") + someone = JA (\cas k -> "ある人" ++ case_particle cas ++ k "") + r5 (JA f) (JA x) = JA (f x) -- the same as r2 + r4 (JA x) (JA f) = JA (f x) -- the same as r1 + +-- | We can now see the English sentences that +-- correspond to the derivations sen2-sen5 in +-- QCFG.hs +sen2_ja = sen2 :: JA S +sen3_ja = sen3 :: JA S +sen4_ja = sen4 :: JA S +sen5_ja = sen5 :: JA S + diff --git a/Lambda/QHCFG.hs b/Lambda/QHCFG.hs new file mode 100644 --- /dev/null +++ b/Lambda/QHCFG.hs @@ -0,0 +1,80 @@ +{-# LANGUAGE EmptyDataDecls, NoMonomorphismRestriction #-} +{-# LANGUAGE TypeFamilies #-} + +-- | Context-free grammar with quantifiers +-- A different ways to add quantification, via +-- Higher-Order abstract syntax (HOAS). +-- This is a "rational reconstruction" of Montague's +-- general approach of `administrative pronouns', which +-- later gave rise to the Quantifier Raising (QR) +-- +module Lambda.QHCFG where + +import Lambda.Semantics +import Lambda.CFG -- we shall re-use our earlier work + +-- | No longer any need in a new syntactic category QNP +-- We leave out CN as an exercise +-- +-- > data CN -- Common noun +-- +-- We extend our earlier fragment with quantifiers everyone, someone. +-- In contrast to QCFG.hs, we do not add any new syntactic category, +-- so we don't need to add any rules to our CFG. +-- +class (Symantics repr) => Quantifier repr where + everyone :: (repr NP -> repr S) -> repr S + someone :: (repr NP -> repr S) -> repr S + +-- | Sample sentences (or, CFG derivations): +-- compare with those in QCFG.hs +-- We stress that the inferred type of sen2-sen4 +-- is S. So, these are the derivations of +-- complete sentences. +-- +sen2 = everyone (\he -> r1 he (r2 like mary)) + +sen3 = someone (\she -> r1 john (r2 like she)) + +sen4 = everyone (\he -> someone (\she -> r1 he (r2 like she))) + +-- | We extend our EN interpreter (interpreter of +-- derivations as English phrases) to deal +-- with quantifiers. +-- +instance Quantifier EN where + everyone f = f (EN "everyone") + someone f = f (EN "someone") + +-- | We can now see the English sentences that +-- correspond to the derivations sen2-sen4. +sen2_en = sen2 :: EN S +sen3_en = sen3 :: EN S +sen4_en = sen4 :: EN S + +-- | We also extend the semantics interpreter: +-- the interpreter of a derivation into a +-- formula of STT, or Lambda-calculus. +-- We reconstruct Montague's ``pronoun trick'' +instance (Lambda lrepr) => Quantifier (Sem lrepr) where + everyone f = Sem (app forall (lam (\he -> unSem (f (Sem he))))) + someone f = Sem (app exists (lam (\she -> unSem (f (Sem she))))) + +-- | We can see the semantic yield of our derivations +sen2_sem = sen2 :: Sem (P C) S -- We encode universal via existential +sen3_sem = sen3 :: Sem C S -- now reduced! +sen4_sem = sen4 :: Sem (P C) S + +-- | As in QCFG.hs, sen4_sem demonstrates the linear reading. +-- Now however we can get the inverse reading of the phrase. +-- +-- We build the following derivation +sen4' = someone (\she -> everyone (\he -> r1 he (r2 like she))) + +-- | which corresponds to the same English phrase +sen4'_en = sen4' :: EN S +-- everyone likes someone + +-- | The semantics shows the inverse reading +sen4'_sem = sen4' :: Sem (P C) S + diff --git a/Lambda/Semantics.hs b/Lambda/Semantics.hs new file mode 100644 --- /dev/null +++ b/Lambda/Semantics.hs @@ -0,0 +1,192 @@ +{-# 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 diff --git a/liboleg.cabal b/liboleg.cabal --- a/liboleg.cabal +++ b/liboleg.cabal @@ -1,5 +1,5 @@ name: liboleg -version: 2010.1.7.0 +version: 2010.1.7.1 license: BSD3 license-file: LICENSE author: Oleg Kiselyov