diff options
| -rw-r--r-- | examples/typetheory/Donkey.gf | 33 | ||||
| -rw-r--r-- | examples/typetheory/DonkeyEng.gf | 20 | ||||
| -rw-r--r-- | examples/typetheory/README | 9 |
3 files changed, 55 insertions, 7 deletions
diff --git a/examples/typetheory/Donkey.gf b/examples/typetheory/Donkey.gf index 5be8b526c..6dd77ba97 100644 --- a/examples/typetheory/Donkey.gf +++ b/examples/typetheory/Donkey.gf @@ -9,19 +9,29 @@ cat VP Set ; V2 Set Set ; V Set ; + AP Set ; + PN Set ; data - PredVP : ({A} : Set) -> NP A -> VP A -> S ; + 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 ; - Man, Donkey : CN ; + 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) ; + John : PN (iCN Man) ; -- Montague semantics in type theory @@ -30,31 +40,44 @@ fun 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 ; 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)) ; 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 _ (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) ; --- for the type-theoretical lexicon data - Man', Donkey' : Set ; + Man', Donkey', Woman' : Set ; Own', Beat' : El Man' -> El Donkey' -> Set ; + Love' : ({A,B} : Set) -> El A -> El B -> Set ; + Old' : ({A} : Set) -> El A -> Set ; Walk', Talk' : El Man' -> Set ; - + Pregnant' : El Woman' -> Set ; + John' : El Man' ; def iCN Man = Man' ; + iCN Woman = Woman' ; iCN Donkey = Donkey' ; iV2 _ _ Beat = Beat' ; iV2 _ _ Own = Own' ; + iV2 _ _ (Love A B) = Love' A B ; iV _ Walk = Walk' ; iV _ Talk = Talk' ; + iAP _ (Old A) = Old' A ; + iAP _ Pregnant = Pregnant' ; + iPN _ John = John' ; }
\ No newline at end of file diff --git a/examples/typetheory/DonkeyEng.gf b/examples/typetheory/DonkeyEng.gf index 524f8e880..927f453ff 100644 --- a/examples/typetheory/DonkeyEng.gf +++ b/examples/typetheory/DonkeyEng.gf @@ -7,33 +7,49 @@ lincat CN = {s : TryEng.CN ; p : TryEng.Pron} ; -- since English CN has no gender NP = TryEng.NP ; VP = TryEng.VP ; + AP = TryEng.AP ; V2 = TryEng.V2 ; V = TryEng.V ; + PN = TryEng.PN ; lin PredVP _ Q F = mkS (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 ; - The A _ = mkNP the_Det A.s ; - Pron A _ = mkNP A.p ; + Every A = mkNP every_Det 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} ; Man = {s = mkCN (mkN "man" "men") ; p = he_Pron} ; + Woman = {s = mkCN (mkN "woman" "women") ; p = she_Pron} ; Donkey = {s = mkCN (mkN "donkey") ; p = it_Pron} ; Own = mkV2 "own" ; Beat = mkV2 beat_V ; + Love _ _ = mkV2 "love" ; Walk = mkV "walk" ; Talk = mkV "talk" ; + Old _ = mkAP (mkA "old") ; + Pregnant = mkAP (mkA "pregnant") ; + John = mkPN "John" ; -- for the lexicon in type theory lin Man' = ss "man'" ; + Woman' = ss "woman'" ; Donkey' = ss "donkey'" ; Own' = apply "own'" ; Beat' = apply "beat'" ; + Love' _ _ = apply "love'" ; Walk' = apply "walk'" ; Talk' = apply "talk'" ; + Old' _ = apply "old'" ; + Pregnant' = apply "pregnant'" ; + John' = ss "john'" ; }
\ No newline at end of file diff --git a/examples/typetheory/README b/examples/typetheory/README index 61ac296ed..75a3ee422 100644 --- a/examples/typetheory/README +++ b/examples/typetheory/README @@ -56,3 +56,12 @@ Example 3: (to be revisited) parse of "the donkey sentence" fails, but should su 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') |