From 7004770236db6a27bde4c736e0f0d32e89c2af0a Mon Sep 17 00:00:00 2001
From: aarne <aarne@chalmers.se>
Date: Tue, 13 Sep 2011 19:52:48 +0000
Subject: [PATCH] rewrote DonkeyEng with RGL and introduced VP category

---
 examples/typetheory/Donkey.gf    | 32 ++++++++++++++---------
 examples/typetheory/DonkeyEng.gf | 45 +++++++++++++++++---------------
 examples/typetheory/README       | 12 ++++-----
 3 files changed, 50 insertions(+), 39 deletions(-)

diff --git a/examples/typetheory/Donkey.gf b/examples/typetheory/Donkey.gf
index 5ed296e30..5be8b526c 100644
--- a/examples/typetheory/Donkey.gf
+++ b/examples/typetheory/Donkey.gf
@@ -1,40 +1,48 @@
 abstract Donkey = Types ** {
 
+flags startcat = S ;
+
 cat 
   S ; 
   CN ;
   NP Set ;
+  VP Set ;
   V2 Set Set ;
   V  Set ;
 
 data
-  PredV2 : ({A,B} : Set) -> V2 A B -> NP A -> NP B -> S ;
-  PredV  : ({A} : Set)   -> V A -> NP A -> S ;
-  If     : (A : S) -> (El (iS A) -> S) -> S ;
-  An     : (A : CN) -> NP (iCN A) ;
-  The    : (A : CN)   -> El (iCN A) -> NP (iCN A) ;
-  Pron   : ({A} : CN) -> El (iCN A) -> NP (iCN A) ;
+  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 ;
+  If      : (A : S) -> (El (iS A) -> S) -> S ;
+  An      : (A : CN) -> NP (iCN A) ;
+  The     : (A : CN)   -> El (iCN A) -> NP (iCN A) ;
+  Pron    : ({A} : CN) -> El (iCN A) -> NP (iCN A) ;
 
   Man, Donkey : CN ;
   Own, Beat : V2 (iCN Man) (iCN Donkey) ;
   Walk, Talk : V (iCN Man) ;
 
+-- Montague semantics in type theory
+
 fun
   iS  : S -> Set ;
   iCN : CN -> Set ;
   iNP : ({A} : Set) -> NP A -> (El A -> Set) -> Set ;
-  iV2 : ({A,B} : Set) -> V2 A B -> (El A -> El B -> Set) ;
+  iVP : ({A} : Set) -> VP A -> (El A -> Set) ;
   iV  : ({A} : Set) -> V A -> (El A -> Set) ;
-
+  iV2 : ({A,B} : Set) -> V2 A B -> (El A -> El B -> Set) ;
 def
-  iS (PredV2 A B F Q R) = iNP A Q (\x -> iNP B R (\y -> iV2 A B F x y)) ;
-  iS (PredV A F Q) = iNP A Q (iV A F) ;
-  iS (If A B) = Pi (iS A) (\x -> iS (B x)) ;
+  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 ;
   iNP _ (An A) F = Sigma (iCN A) F ;
   iNP _ (Pron _ x) F = F x ;
   iNP _ (The _ x) F = F x ;
 
--- for the lexicon
+
+--- for the type-theoretical lexicon
 
 data
   Man', Donkey' : Set ;
diff --git a/examples/typetheory/DonkeyEng.gf b/examples/typetheory/DonkeyEng.gf
index ec80285f0..524f8e880 100644
--- a/examples/typetheory/DonkeyEng.gf
+++ b/examples/typetheory/DonkeyEng.gf
@@ -1,30 +1,32 @@
-concrete DonkeyEng of Donkey = TypesSymb ** open Prelude in {
+--# -path=.:present
+
+concrete DonkeyEng of Donkey = TypesSymb ** open TryEng, IrregEng, Prelude in {
 
 lincat 
-  S  = SS ; 
-  CN = SS ** {g : Gender} ;
-  NP = SS ;
-  V2 = SS ;
-  V  = SS ;
-
-param Gender = Masc | Fem | Neutr ;
+  S  = TryEng.S ; 
+  CN = {s : TryEng.CN ; p : TryEng.Pron} ; -- since English CN has no gender
+  NP = TryEng.NP ;
+  VP = TryEng.VP ;
+  V2 = TryEng.V2 ;
+  V  = TryEng.V ;
 
 lin
-  PredV2 _ _ F x y = ss (x.s ++ F.s ++ y.s) ;
-  PredV _ F x = ss (x.s ++ F.s) ;
-  If A B = ss ("if" ++ A.s ++ B.s) ;
-  An A = ss ("a" ++ A.s) ;
-  The A _ = ss ("the" ++ A.s) ;
-  Pron A _ = ss (case A.g of {Masc => "he" ; Fem => "she" ; Neutr => "it"}) ;
+  PredVP _ Q F = mkS (mkCl Q F) ;
+  ComplV2 _ _ F y = mkVP F y ;
+  UseV _ 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 ;
 
-  Man = {s = "man" ; g = Masc} ;
-  Donkey = {s = "donkey" ; g = Neutr} ;
-  Own = ss "owns" ;
-  Beat = ss "beats" ;
-  Walk = ss "walks" ;
-  Talk = ss "talks" ;
+  Man = {s = mkCN (mkN "man" "men") ; p = he_Pron} ;
+  Donkey = {s = mkCN (mkN "donkey") ; p = it_Pron} ;
+  Own = mkV2 "own" ;
+  Beat = mkV2 beat_V ;
+  Walk = mkV "walk" ;
+  Talk = mkV "talk" ;
 
--- for the lexicon
+-- for the lexicon in type theory
 
 lin
   Man' = ss "man'" ;
@@ -33,4 +35,5 @@ lin
   Beat' = apply "beat'" ;
   Walk' = apply "walk'" ;
   Talk' = apply "talk'" ;
+
 }
\ No newline at end of file
diff --git a/examples/typetheory/README b/examples/typetheory/README
index 0ed6df0d7..61ac296ed 100644
--- a/examples/typetheory/README
+++ b/examples/typetheory/README
@@ -38,7 +38,8 @@ Example 2: parse and interpret a sentence, also showing the nice formula.
   > import DonkeyEng.gf
 
   Donkey> p -cat=S -tr "a man owns a donkey " | pt -transfer=iS -tr | l -unlexcode
-  PredV2 {Man'} {Donkey'} Own (An Man) (An Donkey)
+
+  PredVP {Man'} (An Man) (ComplV2 {Man'} {Donkey'} Own (An Donkey))
 
   Sigma Man' (\v0 -> Sigma Donkey' (\v1 -> Own' v0 v1))
 
@@ -48,11 +49,10 @@ Example 2: parse and interpret a sentence, also showing the nice formula.
 Example 3: (to be revisited) parse of "the donkey sentence" fails, but should succeed
 
   Donkey> p -cat=S "if a man owns a donkey he beats it"
-  The parsing is successful but the type checking failed with error(s):
-    Couldn't match expected type NP Man'
-           against inferred type NP (iCN Donkey)
-    In the expression: Pron {Donkey} ?13
-  
+
+  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