blob: d3afc73cfd3d2c2fe5917c9a6085bfea56b5d615 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
|
abstract NLG = Logic ** {
flags
startcat = Utt;
cat
N (Ind -> Prop);
A (Ind -> Prop);
CN (Ind -> Prop);
Det ((Ind -> Prop) -> (Ind -> Prop) -> Prop);
PN Ind;
NP ((Ind -> Prop) -> Prop);
AP (Ind -> Prop);
VP (Ind -> Prop);
VPSlash (Ind -> Ind -> Prop);
V (Ind -> Prop);
V2 (Ind -> Ind -> Prop);
Comp (Ind -> Prop);
Pol (Prop -> Prop);
Cl Prop;
ClSlash (Ind -> Prop);
S Prop;
Utt;
Conj (Prop -> Prop -> Prop) ;
ListNP ((Prop -> Prop -> Prop) -> (Ind -> Prop) -> Prop) ;
ListS ((Prop -> Prop -> Prop) -> Prop) ;
fun
PredVP : ({np} : (Ind -> Prop) -> Prop) ->
({vp} : Ind -> Prop) ->
NP np -> VP vp -> Cl (np vp) ;
UseV : ({v} : Ind -> Prop) ->
V v -> VP v ;
ComplSlash : ({v2} : Ind -> Ind -> Prop) ->
({np} : (Ind -> Prop) -> Prop) ->
VPSlash v2 -> NP np -> VP (\i -> np (v2 i)) ;
SlashV2a : ({v2} : Ind -> Ind -> Prop) ->
V2 v2 -> VPSlash v2 ;
SlashVP : ({np} : (Ind -> Prop) -> Prop) ->
({v2} : Ind -> Ind -> Prop) ->
NP np -> VPSlash v2 -> ClSlash (\x -> np (v2 x));
ComplClSlash : ({sl} : Ind -> Prop) ->
({np} : (Ind -> Prop) -> Prop) ->
ClSlash sl -> NP np -> Cl (np sl);
UseComp : ({c} : Ind -> Prop) ->
Comp c -> VP c ;
CompAP : ({ap} : Ind -> Prop) ->
AP ap -> Comp ap ;
CompNP : ({np} : (Ind -> Prop) -> Prop) ->
NP np -> Comp (\x -> np (\y -> eq x y)) ;
UsePN : ({i} : Ind) -> PN i -> NP (\f -> f i) ;
DetCN : ({det} : (Ind -> Prop) -> (Ind -> Prop) -> Prop) ->
({cn} : Ind -> Prop) ->
Det det -> CN cn -> NP (\f -> det cn f);
AdjCN : ({ap,cn} : Ind -> Prop) ->
AP ap -> CN cn -> CN (\x -> and (ap x) (cn x)) ;
PositA : ({a} : Ind -> Prop) ->
A a -> AP a ;
UseN : ({n} : Ind -> Prop) -> N n -> CN n;
BaseNP : ({np1,np2} : (Ind -> Prop) -> Prop) ->
NP np1 -> NP np2 -> ListNP (\conj,f -> conj (np1 f) (np2 f)) ;
ConsNP : ({np1} : (Ind -> Prop) -> Prop) ->
({lst} : (Prop -> Prop -> Prop) -> (Ind -> Prop) -> Prop) ->
NP np1 -> ListNP lst -> ListNP (\conj,f -> conj (np1 f) (lst conj f)) ;
ConjNP : ({cnj} : Prop -> Prop -> Prop) ->
({lst} : (Prop -> Prop -> Prop) -> (Ind -> Prop) -> Prop) ->
Conj cnj -> ListNP lst -> NP (lst cnj) ;
BaseS : ({s1,s2} : Prop) ->
S s1 -> S s2 -> ListS (\conj -> conj s1 s2) ;
ConsS : ({s1} : Prop) ->
({lst} : (Prop -> Prop -> Prop) -> Prop) ->
S s1 -> ListS lst -> ListS (\conj -> conj s1 (lst conj)) ;
ConjS : ({cnj} : Prop -> Prop -> Prop) ->
({lst} : (Prop -> Prop -> Prop) -> Prop) ->
Conj cnj -> ListS lst -> S (lst cnj) ;
john_PN : PN john;
mary_PN : PN mary;
boy_N : N boy;
somebody_NP : NP exists;
everybody_NP : NP forall;
love_V2 : V2 love ;
leave_V : V leave ;
smart_A : A smart ;
a_Det : Det (\d,f -> exists (\x -> and (d x) (f x)));
every_Det : Det (\d,f -> forall (\x -> impl (d x) (f x)));
some_Det : Det (\d,f -> exists (\x -> and (d x) (f x)));
PPos : Pol (\t -> t) ;
PNeg : Pol (\t -> not t) ;
and_Conj : Conj and ;
or_Conj : Conj or ;
UseCl : ({cl} : Prop) ->
({p} : Prop -> Prop) ->
Pol p -> Cl cl -> S (p cl);
UttS : (s : Prop) -> S s -> Utt;
}
|
