packages feed

liboleg 2010.1.7.0 → 2010.1.7.1

raw patch · 16 files changed

+1191/−1 lines, 16 files

Files

+ Lambda/CCG.hs view
@@ -0,0 +1,211 @@+{-# LANGUAGE TypeOperators, EmptyDataDecls, NoMonomorphismRestriction #-}+{-# LANGUAGE TypeFamilies, FlexibleInstances #-}++-- | Combinatorial Categorical Grammar (CCG)+--+-- <http://okmij.org/ftp/gengo/NASSLLI10>+--++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
+ Lambda/CFG.hs view
@@ -0,0 +1,116 @@+{-# LANGUAGE EmptyDataDecls, NoMonomorphismRestriction #-}+{-# LANGUAGE TypeFamilies, FlexibleInstances #-}++-- | Context-free grammars, in the tagless-final style+--+-- <http://okmij.org/ftp/gengo/NASSLLI10/>+--+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+
+ Lambda/CFG1EN.hs view
@@ -0,0 +1,15 @@+--+-- | <http://okmij.org/ftp/gengo/NASSLLI10/>+--++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)
+ Lambda/CFG1Sem.hs view
@@ -0,0 +1,33 @@+--+-- | <http://okmij.org/ftp/gengo/NASSLLI10/>+--++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)
+ Lambda/CFG2EN.hs view
@@ -0,0 +1,30 @@+--+-- | <http://okmij.org/ftp/gengo/NASSLLI10>+--+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+
+ Lambda/CFG2Sem.hs view
@@ -0,0 +1,32 @@+-- | <http://okmij.org/ftp/gengo/NASSLLI10/>++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+-}
+ Lambda/CFG3EN.hs view
@@ -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:+--+-- > <string,features> 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
+ Lambda/CFG3Sem.hs view
@@ -0,0 +1,47 @@+{-# LANGUAGE EmptyDataDecls, FlexibleInstances, TypeFamilies #-}++-- | Type functions: interpretations of the type constants+--+-- <http://okmij.org/ftp/gengo/NASSLLI10/>+--++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.
+ Lambda/CFG4.hs view
@@ -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
+ Lambda/CFGJ.hs view
@@ -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.+--+-- <http://okmij.org/ftp/gengo/NASSLLI10/>+--+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
+ Lambda/Dynamics.hs view
@@ -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.+-- <http://www.inria.fr/rocquencourt/rendez-vous/modele-et-algo/dynamic-logic-a-type-theoretic-view>+--++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
+ Lambda/QCFG.hs view
@@ -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
+ Lambda/QCFGJ.hs view
@@ -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+
+ Lambda/QHCFG.hs view
@@ -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+
+ Lambda/Semantics.hs view
@@ -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
liboleg.cabal view
@@ -1,5 +1,5 @@ name:           liboleg-version:        2010.1.7.0+version:        2010.1.7.1 license:        BSD3 license-file:   LICENSE author:         Oleg Kiselyov