GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-09 04:59:31 -06:00
Code Issues Packages Projects Releases Wiki Activity

Donkey: Det and Conj added, as well as negative sentences

Browse Source
This commit is contained in:
aarne
2011-09-14 15:56:19 +00:00
parent f2786ca0a0
commit 8d05fa5cc7
4 changed files with 93 additions and 51 deletions
Download Patch File Download Diff File Expand all files Collapse all files

82
examples/typetheory/Donkey.gf
View File

@@ -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

37
examples/typetheory/DonkeyEng.gf
View File

@@ -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

23
examples/typetheory/README
View File

@@ -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')

2
examples/typetheory/TypesSymb.gf
View File

@@ -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 ;