From 8d05fa5cc7464935eef31a67bb05ef8a4fc3e292 Mon Sep 17 00:00:00 2001 From: aarne Date: Wed, 14 Sep 2011 15:56:19 +0000 Subject: [PATCH] Donkey: Det and Conj added, as well as negative sentences --- examples/typetheory/Donkey.gf | 82 +++++++++++++++++++++----------- examples/typetheory/DonkeyEng.gf | 37 +++++++++++--- examples/typetheory/README | 23 +++------ examples/typetheory/TypesSymb.gf | 2 +- 4 files changed, 93 insertions(+), 51 deletions(-) diff --git a/examples/typetheory/Donkey.gf b/examples/typetheory/Donkey.gf index 6dd77ba97..6268a7846 100644 --- a/examples/typetheory/Donkey.gf +++ b/examples/typetheory/Donkey.gf @@ -4,58 +4,84 @@ flags startcat = S ; cat S ; + Cl ; CN ; + Det ; + Conj ; NP Set ; VP Set ; V2 Set Set ; V Set ; AP Set ; PN Set ; + RC Set ; data - PredVP : ({A} : Set) -> NP A -> VP A -> S ; - ComplV2 : ({A,B} : Set) -> V2 A B -> NP B -> VP A ; - UseV : ({A} : Set) -> V A -> VP A ; - UseAP : ({A} : Set) -> AP A -> VP A ; - If : (A : S) -> (El (iS A) -> S) -> S ; - An : (A : CN) -> NP (iCN A) ; - Every : (A : CN) -> NP (iCN A) ; - The : (A : CN) -> El (iCN A) -> NP (iCN A) ; - Pron : ({A} : CN) -> El (iCN A) -> NP (iCN A) ; - UsePN : ({A} : Set) -> PN A -> NP A ; - ModCN : (A : CN) -> AP (iCN A) -> CN ; + IfS : (A : S) -> (El (iS A) -> S) -> S ; -- if A B + ConjS : Conj -> S -> S -> S ; -- A and B ; A or B + PosCl : Cl -> S ; -- John walks + NegCl : Cl -> S ; -- John doesn't walk + PredVP : ({A} : Set) -> NP A -> VP A -> Cl ; -- John (walks / doesn't walk) + ComplV2 : ({A,B} : Set) -> V2 A B -> NP B -> VP A ; -- loves John + UseV : ({A} : Set) -> V A -> VP A ; -- walks + UseAP : ({A} : Set) -> AP A -> VP A ; -- is old + DetCN : Det -> (A : CN) -> NP (iCN A) ; -- every man + ConjNP : Conj -> ({A} : Set) -> NP A -> NP A -> NP A ; -- John and every man + The : (A : CN) -> El (iCN A) -> NP (iCN A) ; -- the donkey + Pron : ({A} : CN) -> El (iCN A) -> NP (iCN A) ; -- he/she/it + UsePN : ({A} : Set) -> PN A -> NP A ; -- John + ModAP : (A : CN) -> AP (iCN A) -> CN ; -- old man + ModRC : (A : CN) -> RC (iCN A) -> CN ; -- man that walks + RelVP : ({A} : CN) -> VP (iCN A) -> RC (iCN A) ; -- that walks + An : Det ; + Every : Det ; + And : Conj ; + Or : Conj ; Man, Donkey, Woman : CN ; Own, Beat : V2 (iCN Man) (iCN Donkey) ; - Love : ({A,B} : Set) -> V2 A B ; - Walk, Talk : V (iCN Man) ; - Old : ({A} : Set) -> AP A ; - Pregnant : AP (iCN Woman) ; + Love : ({A,B} : Set) -> V2 A B ; -- polymorphic verb + Walk, Talk : V (iCN Man) ; -- monomorphic verbs + Old : ({A} : Set) -> AP A ; -- polymorphic adjective + Pregnant : AP (iCN Woman) ; -- monomorphic adjective John : PN (iCN Man) ; -- Montague semantics in type theory fun - iS : S -> Set ; - iCN : CN -> Set ; - iNP : ({A} : Set) -> NP A -> (El A -> Set) -> Set ; - iVP : ({A} : Set) -> VP A -> (El A -> Set) ; - iAP : ({A} : Set) -> AP A -> (El A -> Set) ; - iV : ({A} : Set) -> V A -> (El A -> Set) ; - iV2 : ({A,B} : Set) -> V2 A B -> (El A -> El B -> Set) ; - iPN : ({A} : Set) -> PN A -> El A ; + iS : S -> Set ; + iCl : Cl -> Set ; + iCN : CN -> Set ; + iDet : Det -> ({A} : Set) -> (El A -> Set) -> Set ; + iConj : Conj -> Set -> Set -> Set ; + iNP : ({A} : Set) -> NP A -> (El A -> Set) -> Set ; + iVP : ({A} : Set) -> VP A -> (El A -> Set) ; + iAP : ({A} : Set) -> AP A -> (El A -> Set) ; + iRC : ({A} : Set) -> RC A -> (El A -> Set) ; + iV : ({A} : Set) -> V A -> (El A -> Set) ; + iV2 : ({A,B} : Set) -> V2 A B -> (El A -> El B -> Set) ; + iPN : ({A} : Set) -> PN A -> El A ; def - iS (PredVP A Q F) = iNP A Q (\x -> iVP A F x) ; - iS (If A B) = Pi (iS A) (\x -> iS (B x)) ; + iS (PosCl A) = iCl A ; + iS (NegCl A) = Neg (iCl A) ; + iS (IfS A B) = Pi (iS A) (\x -> iS (B x)) ; + iS (ConjS C A B) = iConj C (iS A) (iS B) ; + iCl (PredVP A Q F) = iNP A Q (\x -> iVP A F x) ; iVP _ (ComplV2 A B F R) x = iNP B R (\y -> iV2 A B F x y) ; iVP _ (UseV A F) x = iV A F x ; iVP _ (UseAP A F) x = iAP A F x ; - iNP _ (An A) F = Sigma (iCN A) F ; - iNP _ (Every A) F = Pi (iCN A) F ; + iNP _ (DetCN D A) F = iDet D (iCN A) F ; + iNP _ (ConjNP C A Q R) F = iConj C (iNP A Q F) (iNP A R F) ; iNP _ (Pron _ x) F = F x ; iNP _ (The _ x) F = F x ; iNP _ (UsePN A a) F = F (iPN A a) ; - iCN (ModCN A F) = Sigma (iCN A) (\x -> iAP (iCN A) F x) ; + iDet An A F = Sigma A F ; + iDet Every A F = Pi A F ; + iCN (ModAP A F) = Sigma (iCN A) (\x -> iAP (iCN A) F x) ; + iCN (ModRC A F) = Sigma (iCN A) (\x -> iRC (iCN A) F x) ; + iRC _ (RelVP A F) x = iVP (iCN A) F x ; + iConj And = Prod ; + iConj Or = Plus ; --- for the type-theoretical lexicon diff --git a/examples/typetheory/DonkeyEng.gf b/examples/typetheory/DonkeyEng.gf index 927f453ff..51f5c32ca 100644 --- a/examples/typetheory/DonkeyEng.gf +++ b/examples/typetheory/DonkeyEng.gf @@ -1,9 +1,12 @@ --# -path=.:present -concrete DonkeyEng of Donkey = TypesSymb ** open TryEng, IrregEng, Prelude in { +concrete DonkeyEng of Donkey = TypesSymb ** open TryEng, IrregEng, (E = ExtraEng), Prelude in { lincat S = TryEng.S ; + Cl = TryEng.Cl ; + Det = TryEng.Det ; + Conj = TryEng.Conj ; CN = {s : TryEng.CN ; p : TryEng.Pron} ; -- since English CN has no gender NP = TryEng.NP ; VP = TryEng.VP ; @@ -11,19 +14,29 @@ lincat V2 = TryEng.V2 ; V = TryEng.V ; PN = TryEng.PN ; + RC = TryEng.RS ; lin - PredVP _ Q F = mkS (mkCl Q F) ; + IfS A B = mkS (mkAdv if_Subj A) (lin S (ss B.s)) ; + ConjS C A B = mkS C A B ; + PosCl A = mkS A ; + NegCl A = mkS negativePol A ; + PredVP _ Q F = mkCl Q F ; ComplV2 _ _ F y = mkVP F y ; UseV _ F = mkVP F ; UseAP _ F = mkVP F ; - If A B = mkS (mkAdv if_Subj A) (lin S (ss B.s)) ; - An A = mkNP a_Det A.s ; - Every A = mkNP every_Det A.s ; + An = mkDet a_Quant ; + Every = every_Det ; + DetCN D A = mkNP D A.s ; The A r = mkNP the_Det A.s | mkNP (mkNP the_Det A.s) (lin Adv (parenss r)) ; -- variant showing referent: he ( john' ) Pron A r = mkNP A.p | mkNP (mkNP A.p) (lin Adv (parenss r)) ; UsePN _ a = mkNP a ; - ModCN A F = {s = mkCN F A.s ; p = A.p} ; + ConjNP C _ Q R = mkNP C Q R ; + ModAP A F = {s = mkCN F A.s ; p = A.p} ; + ModRC A F = {s = mkCN A.s F ; p = A.p} ; + RelVP A F = mkRS (mkRCl (relPron A) F) ; + And = and_Conj ; + Or = or_Conj ; Man = {s = mkCN (mkN "man" "men") ; p = he_Pron} ; Woman = {s = mkCN (mkN "woman" "women") ; p = she_Pron} ; @@ -37,6 +50,18 @@ lin Pregnant = mkAP (mkA "pregnant") ; John = mkPN "John" ; +oper + relPron : {s : CN ; p : Pron} -> RP = \cn -> case isHuman cn.p of { +--- True => who_RP ; +--- False => which_RP + _ => E.that_RP + } ; + isHuman : Pron -> Bool = \p -> case p.a of { +--- AgP3Sg Neutr => False ; + _ => True + } ; + + -- for the lexicon in type theory lin diff --git a/examples/typetheory/README b/examples/typetheory/README index 75a3ee422..7d77e41b7 100644 --- a/examples/typetheory/README +++ b/examples/typetheory/README @@ -46,22 +46,13 @@ Example 2: parse and interpret a sentence, also showing the nice formula. (Σ v0 : man')(Σ v1 : donkey')own' (v0 , v1) -Example 3: (to be revisited) parse of "the donkey sentence" fails, but should succeed +Example 3: (to be revisited) parse of "the donkey sentence" returns some metavariables - Donkey> p -cat=S "if a man owns a donkey he beats it" + Donkey> dc interpret p ?0 | pt -transfer=iS | l -unlexcode + + Donkey> %interpret "if a man owns a donkey he beats it" + + (Π v0 : (Σ v0 : man')(Σ v1 : donkey')own' (v0 , v1))beat' (?16 , ?22) + - The sentence is not complete - Donkey> p -cat=S "if a man owns a donkey the man beats the donkey" - - The sentence is not complete - - -Example 4: problem that appears with CN's modified by polymorphic AP's (old), but not with monomorphic ones (pregnant) - - Donkey> p "an old man walks" - src/runtime/haskell/PGF/TypeCheck.hs:(528,4)-(550,67): Non-exhaustive patterns in function occurCheck - -- this should build (ModCN Man (Old Man')) - - Donkey> p "a pregnant woman loves John " | pt -transfer=iS | l -unlexcode - (Σ v0 : (Σ v0 : woman')pregnant' (v0))love' (v0 , john') diff --git a/examples/typetheory/TypesSymb.gf b/examples/typetheory/TypesSymb.gf index 1c0cc5fae..3ace7e158 100644 --- a/examples/typetheory/TypesSymb.gf +++ b/examples/typetheory/TypesSymb.gf @@ -23,7 +23,7 @@ lin Plus A B = parenss (infixSS "+" A B) ; Pi A B = ss (paren (capPi ++ B.$0 ++ ":" ++ A.s) ++ B.s) ; Sigma A B = ss (paren (capSigma ++ B.$0 ++ ":" ++ A.s) ++ B.s) ; - Falsum = ss "_|_" ; + Falsum = ss "Ø" ; Nat = ss "N" ; Id A a b = apply "I" A a b ;