msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

rewrote DonkeyEng with RGL and introduced VP category

Browse Source
This commit is contained in:
aarne
2011-09-13 19:52:48 +00:00
parent 604c92bf47
commit 7004770236
3 changed files with 50 additions and 39 deletions
Download Patch File Download Diff File Expand all files Collapse all files

32
examples/typetheory/Donkey.gf
View File

@@ -1,40 +1,48 @@
abstract Donkey = Types ** { abstract Donkey = Types ** {
flags startcat = S ;
cat cat
S ; S ;
CN ; CN ;
NP Set ; NP Set ;
VP Set ;
V2 Set Set ; V2 Set Set ;
V Set ; V Set ;
data data
PredV2 : ({A,B} : Set) -> V2 A B -> NP A -> NP B -> S ; PredVP : ({A} : Set) -> NP A -> VP A -> S ;
PredV : ({A} : Set) -> V A -> NP A -> S ; ComplV2 : ({A,B} : Set) -> V2 A B -> NP B -> VP A ;
If : (A : S) -> (El (iS A) -> S) -> S ; UseV : ({A} : Set) -> V A -> VP A ;
An : (A : CN) -> NP (iCN A) ; If : (A : S) -> (El (iS A) -> S) -> S ;
The : (A : CN) -> El (iCN A) -> NP (iCN A) ; An : (A : CN) -> NP (iCN A) ;
Pron : ({A} : CN) -> El (iCN A) -> NP (iCN A) ; The : (A : CN) -> El (iCN A) -> NP (iCN A) ;
Pron : ({A} : CN) -> El (iCN A) -> NP (iCN A) ;
Man, Donkey : CN ; Man, Donkey : CN ;
Own, Beat : V2 (iCN Man) (iCN Donkey) ; Own, Beat : V2 (iCN Man) (iCN Donkey) ;
Walk, Talk : V (iCN Man) ; Walk, Talk : V (iCN Man) ;
-- Montague semantics in type theory
fun fun
iS : S -> Set ; iS : S -> Set ;
iCN : CN -> Set ; iCN : CN -> Set ;
iNP : ({A} : Set) -> NP A -> (El A -> Set) -> 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) ; iV : ({A} : Set) -> V A -> (El A -> Set) ;
iV2 : ({A,B} : Set) -> V2 A B -> (El A -> El B -> Set) ;
def def
iS (PredV2 A B F Q R) = iNP A Q (\x -> iNP B R (\y -> iV2 A B F x y)) ; iS (PredVP A Q F) = iNP A Q (\x -> iVP A F x) ;
iS (PredV A F Q) = iNP A Q (iV A F) ; iS (If A B) = Pi (iS A) (\x -> iS (B 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 _ (An A) F = Sigma (iCN A) F ;
iNP _ (Pron _ x) F = F x ; iNP _ (Pron _ x) F = F x ;
iNP _ (The _ x) F = F x ; iNP _ (The _ x) F = F x ;
-- for the lexicon
--- for the type-theoretical lexicon
data data
Man', Donkey' : Set ; Man', Donkey' : Set ;

45
examples/typetheory/DonkeyEng.gf
View File

@@ -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 lincat
S = SS ; S = TryEng.S ;
CN = SS ** {g : Gender} ; CN = {s : TryEng.CN ; p : TryEng.Pron} ; -- since English CN has no gender
NP = SS ; NP = TryEng.NP ;
V2 = SS ; VP = TryEng.VP ;
V = SS ; V2 = TryEng.V2 ;
V = TryEng.V ;
param Gender = Masc | Fem | Neutr ;
lin lin
PredV2 _ _ F x y = ss (x.s ++ F.s ++ y.s) ; PredVP _ Q F = mkS (mkCl Q F) ;
PredV _ F x = ss (x.s ++ F.s) ; ComplV2 _ _ F y = mkVP F y ;
If A B = ss ("if" ++ A.s ++ B.s) ; UseV _ F = mkVP F ;
An A = ss ("a" ++ A.s) ; If A B = mkS (mkAdv if_Subj A) (lin S (ss B.s)) ;
The A _ = ss ("the" ++ A.s) ; An A = mkNP a_Det A.s ;
Pron A _ = ss (case A.g of {Masc => "he" ; Fem => "she" ; Neutr => "it"}) ; The A _ = mkNP the_Det A.s ;
Pron A _ = mkNP A.p ;
Man = {s = "man" ; g = Masc} ; Man = {s = mkCN (mkN "man" "men") ; p = he_Pron} ;
Donkey = {s = "donkey" ; g = Neutr} ; Donkey = {s = mkCN (mkN "donkey") ; p = it_Pron} ;
Own = ss "owns" ; Own = mkV2 "own" ;
Beat = ss "beats" ; Beat = mkV2 beat_V ;
Walk = ss "walks" ; Walk = mkV "walk" ;
Talk = ss "talks" ; Talk = mkV "talk" ;
-- for the lexicon -- for the lexicon in type theory
lin lin
Man' = ss "man'" ; Man' = ss "man'" ;
@@ -33,4 +35,5 @@ lin
Beat' = apply "beat'" ; Beat' = apply "beat'" ;
Walk' = apply "walk'" ; Walk' = apply "walk'" ;
Talk' = apply "talk'" ; Talk' = apply "talk'" ;
} }

12
examples/typetheory/README
View File

@@ -38,7 +38,8 @@ Example 2: parse and interpret a sentence, also showing the nice formula.
> import DonkeyEng.gf > import DonkeyEng.gf
Donkey> p -cat=S -tr "a man owns a donkey " | pt -transfer=iS -tr | l -unlexcode 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)) 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 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" 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
Donkey> p -cat=S "if a man owns a donkey the man beats the donkey" 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 The sentence is not complete