Commit 5cea1797 authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

Examples for cinjunction and neg-raising in TAG

parent 7261b38d
(*signature abstract_syntax=
QNP,NP,S:type;
AND:QNP -> QNP -> ((NP ->S) => S);
JOHN,MARY: NP;
EVERYONE,SOMEONE:QNP;
LOVE: NP -> NP -> S;
SLEEP: NP -> S;
raise:NP -> QNP;
infix @:QNP -> (NP -> S) -> S;
end
*)
signature intermediate_syntax=
NP,S:type;
AND:((NP ->S) -> S) -> ((NP ->S) -> S) -> ((NP ->S) -> S);
AND_itv_el : ((NP ->S) -> S) -> ((NP ->S) -> S) -> ((NP ->S) -> S);
JOHN,MARY,BILL,SUE: NP;
EVERYONE,SOMEONE:(NP -> S)->S;
LOVE: NP -> NP -> S;
SLEEP: NP -> S;
end
(*lexicon abstract2intermediate(abstract_syntax):intermediate_syntax=
NP:=NP;
S:=S;
QNP := (NP ->S) -> S;
AND := AND;
JOHN := JOHN;
MARY := MARY;
SLEEP := SLEEP;
LOVE:=LOVE;
EVERYONE := EVERYONE;
SOMEONE := SOMEONE;
raise:=lambda x r .r x;
@ := lambda q r.q r;
end
*)
signature simple_syntax=
NP,S:type;
AND: NP -> NP -> NP;
AND_itv_el: ((NP ->S) -> S) -> ((NP ->S) -> S) -> ((NP ->S) -> S);
JOHN,MARY,BILL,SUE: NP;
(* DEL : NP -> S;*)
EVERYONE,SOMEONE:NP;
SLEEP: NP -> S;
LOVE: NP -> NP -> S;
end
lexicon intermediate2simple(intermediate_syntax):simple_syntax=
S:=S;
NP:=NP;
AND:=lambda P Q .lambda r.P(lambda x.Q(lambda y.r(AND x y)));
AND_itv_el := AND_itv_el;
JOHN:= JOHN;
MARY := MARY;
BILL := BILL;
SUE := SUE;
SLEEP := SLEEP;
LOVE:=LOVE;
EVERYONE := lambda P.P EVERYONE;
SOMEONE := lambda P.P SOMEONE;
end
(*lexicon abstract2simple(abstract_syntax):simple_syntax=
QNP := (NP->S)->S;
S:=S;
NP:=NP;
AND:=lambda P Q .Lambda r.P(lambda x.Q(lambda y.r(AND x y)));
JOHN:= JOHN;
MARY := MARY;
SLEEP := SLEEP;
LOVE:=LOVE;
EVERYONE := lambda P.P EVERYONE;
SOMEONE := lambda P.P SOMEONE;
raise := lambda n r.r n;
end
*)
signature strings=
string:type;
and,loves,sleeps,John,Mary,Bill,Sue,someone,everyone:string;
infix +:string-> string->string;
epsilon:string;
end
lexicon syntax2strings(simple_syntax):strings=
NP,S:=string;
AND:=lambda x y.x+and+y;
AND_itv_el:= lambda P Q r. (P (lambda x.x)) + and + ((Q r) );
JOHN:=John;
MARY:=Mary;
BILL:=Bill;
SUE:=Sue;
EVERYONE:=everyone;
SOMEONE:=someone;
SLEEP:=lambda s.s+sleeps;
LOVE:=lambda o s.s+loves+ o;
end
(*signature logic =
e,t:type;
sleep : e->t;
love:e -> e -> t;
j,m:e;
infix & : t -> t -> t;
infix > : t -> t -> t;
binder All : (e=>t) -> t;
binder Ex : (e=>t) -> t;
end
lexicon semantics (intermediate_syntax):logic=
NP:= e;
S:=t;
AND := lambda P Q.Lambda r.(P r) & (Q r);
JOHN := j;
MARY := m;
EVERYONE := lambda P.All x.P x;
SOMEONE := lambda P.Ex x.P x;
SLEEP:=sleep;
LOVE:= lambda o s.love s o;
end
*)
\ No newline at end of file
load d conjunction.acg;
compose syntax2strings intermediate2simple as intermediate2strings;
compose intermediate2strings abstract2intermediate as abstract2strings;
compose semantics abstract2intermediate as abstract2semantics;
abstract2intermediate abstract2strings abstract2semantics analyse AND (raise JOHN) EVERYONE SLEEP:S;
abstract2intermediate abstract2strings abstract2semantics analyse AND SOMEONE EVERYONE SLEEP:S;
intermediate2strings semantics analyse EVERYONE (lambda x.SOMEONE (lambda y.AND (lambda P.P y)(lambda P.P x) SLEEP)):S;
intermediate2strings semantics analyse SOMEONE (lambda y.EVERYONE (lambda x.AND (lambda P.P y)(lambda P.P x) SLEEP)):S;
intermediate2strings semantics analyse AND SOMEONE EVERYONE SLEEP:S;
abstract2intermediate abstract2strings abstract2semantics analyse SOMEONE @ (lambda y.EVERYONE @ (lambda x.AND (raise x)(raise y) SLEEP)):S;
\ No newline at end of file
signature abstract_syntax=
QNP,NP,S:type;
AND:QNP -> QNP -> ((NP ->S) => S);
JOHN,MARY: NP;
EVERYONE,SOMEONE:QNP;
LOVE: NP -> NP -> S;
SLEEP: NP -> S;
raise:NP -> QNP;
infix @:QNP -> (NP -> S) -> S;
end
signature intermediate_syntax=
NP,S:type;
AND:((NP ->S) -> S) -> ((NP ->S) -> S) -> ((NP ->S) => S);
JOHN,MARY: NP;
EVERYONE,SOMEONE:(NP -> S)->S;
LOVE: NP -> NP -> S;
SLEEP: NP -> S;
end
lexicon abstract2intermediate(abstract_syntax):intermediate_syntax=
NP:=NP;
S:=S;
QNP := (NP ->S) -> S;
AND := AND;
JOHN := JOHN;
MARY := MARY;
SLEEP := SLEEP;
LOVE:=LOVE;
EVERYONE := EVERYONE;
SOMEONE := SOMEONE;
raise:=lambda x r .r x;
@ := lambda q r.q r;
end
signature simple_syntax=
NP,S:type;
AND: NP -> NP -> NP;
JOHN,MARY: NP;
EVERYONE,SOMEONE:NP;
SLEEP: NP -> S;
LOVE: NP -> NP -> S;
end
lexicon intermediate2simple(intermediate_syntax):simple_syntax=
S:=S;
NP:=NP;
AND:=lambda P Q .Lambda r.P(lambda x.Q(lambda y.r(AND x y)));
JOHN:= JOHN;
MARY := MARY;
SLEEP := SLEEP;
LOVE:=LOVE;
EVERYONE := lambda P.P EVERYONE;
SOMEONE := lambda P.P SOMEONE;
end
(*lexicon abstract2simple(abstract_syntax):simple_syntax=
QNP := (NP->S)->S;
S:=S;
NP:=NP;
AND:=lambda P Q .Lambda r.P(lambda x.Q(lambda y.r(AND x y)));
JOHN:= JOHN;
MARY := MARY;
SLEEP := SLEEP;
LOVE:=LOVE;
EVERYONE := lambda P.P EVERYONE;
SOMEONE := lambda P.P SOMEONE;
raise := lambda n r.r n;
end
*)
signature strings=
string:type;
and,loves,sleeps,John,Mary,someone,everyone:string;
infix +:string-> string->string;
epsilon:string;
end
lexicon syntax2strings(simple_syntax):strings=
NP,S:=string;
AND:=lambda x y.x+and+y;
JOHN:=John;
MARY:=Mary;
EVERYONE:=everyone;
SOMEONE:=someone;
SLEEP:=lambda s.s+sleeps;
LOVE:=lambda o s.s+loves+ o;
end
signature logic =
e,t:type;
sleep : e->t;
love:e -> e -> t;
j,m:e;
infix & : t -> t -> t;
infix > : t -> t -> t;
binder All : (e=>t) -> t;
binder Ex : (e=>t) -> t;
end
lexicon semantics (intermediate_syntax):logic=
NP:= e;
S:=t;
AND := lambda P Q.Lambda r.(P r) & (Q r);
JOHN := j;
MARY := m;
EVERYONE := lambda P.All x.P x;
SOMEONE := lambda P.Ex x.P x;
SLEEP:=sleep;
LOVE:= lambda o s.love s o;
end
\ No newline at end of file
load d neg-raising.acg;
read interpretation_3 analyse
c_ira_a_Dax (c_croit_1 (c_pense_1 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul:P;
read interpretation_3 analyse
c_ira_a_Dax (c_croit_1 (c_pense_2 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul:P;
read interpretation_3 analyse
c_ira_a_Dax (c_croit_2 (c_pense_1 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul:P;
read interpretation_3 analyse
c_ira_a_Dax (c_croit_2 (c_pense_2 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul:P;
read interpretation_3 analyse
c_ira_a_Dax (c_croit_1 (c_pense_1 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul:P;
read interpretation_3 analyse
c_ira_a_Dax (c_croit_1 (c_pense_2 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul:P;
read interpretation_3 analyse
c_ira_a_Dax (c_croit_2 (c_pense_1 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul:P;
read interpretation_3 analyse
c_ira_a_Dax (c_croit_2 (c_pense_2 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul:P;
read interpretation_3 analyse
c_ira_a_Dax (c_croit_1 (c_pense_1 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul:P;
read interpretation_3 analyse
c_ira_a_Dax (c_croit_1 (c_pense_2 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul:P;
read interpretation_3 analyse
c_ira_a_Dax (c_croit_2 (c_pense_1 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul:P;
read interpretation_3 analyse
c_ira_a_Dax (c_croit_2 (c_pense_2 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul:P;
signature derivations =
P_a, V_a, V, P, N:type;
c_croit_1, c_pense_1, c_croit_2, c_pense_2 : P_a -> V_a -> N -> P_a;
c_ira_a_Dax: P_a -> V_a -> N -> P;
I_p:P_a;
I_v:V_a;
c_Marie,c_Paul,c_Jane:N;
NEG : V_a;
end
signature derived =
tree:type;
P2:tree -> tree -> tree;
P3:tree -> tree -> tree -> tree;
V2:tree -> tree -> tree;
N,V:tree -> tree;
croit,pense,que,Paul,Marie,Jane,ira,a_Dax,pas:tree;
end
lexicon read (derivations) : derived =
P_a, V_a:=tree -> tree;
V,P,N:=tree;
c_croit_1,c_croit_2 := lambda p v s x.p(P3 s (v (V croit)) (P2 que x));
c_pense_1,c_pense_2 := lambda p v s x.p(P3 s (v (V pense)) (P2 que x));
c_ira_a_Dax := lambda p v s .p(P3 (N s) (v (V ira)) (a_Dax));
I_p,I_v:=lambda x.x;
c_Marie:= N Marie;
c_Paul:= N Paul;
c_Jane:= N Jane;
NEG := lambda x. V2 x pas;
end
signature logic =
ind,prop: type;
croire,penser: prop -> ind -> prop;
aller_a_Dax: ind -> prop;
M,P,J:ind;
report_1=lambda V. lambda p v s c. p ( v (V c s)): (prop -> ind -> prop)
-> (prop -> prop) -> (prop -> prop) -> ind -> (prop -> prop) ;
report_2=lambda V. lambda p v s c. p ( V (v c) s): (prop -> ind -> prop)
-> (prop -> prop) -> (prop -> prop) -> ind -> (prop -> prop) ;
prefix - : prop -> prop;
ID = lambda x.x : prop -> prop;
end
lexicon interpretation (derivations):logic =
P_a := prop -> prop;
V_a := prop -> prop;
V := ind -> prop;
P := prop;
N := ind;
I_p:=lambda x.x;
I_v:= lambda x.x;
c_ira_a_Dax := lambda p v s. p (v (aller_a_Dax s));
c_Marie:=M;
c_Paul:=P;
c_Jane:=J;
c_croit_1 := report_1 croire;
c_pense_1 := report_1 penser;
c_croit_2 := report_2 croire;
c_pense_2 := report_2 penser;
NEG := lambda p. - p;
end
lexicon interpretation_2 (derivations):logic =
P_a := ((prop -> prop) -> prop) -> (prop -> prop) -> prop;
V_a := prop -> prop;
V := ind -> prop;
P := (prop -> prop) -> prop;
N := ind;
I_p:=lambda x.x;
I_v:= lambda x.x;
c_ira_a_Dax := lambda p v s. p (lambda f . f (v (aller_a_Dax s)));
c_Marie:=M;
c_Paul:=P;
c_Jane:=J;
c_croit_1 := lambda p v s c. p (lambda f. f (v (croire ( c (lambda x.x)) s)));
c_pense_1 := lambda p v s c. p (lambda f. f (v (penser ( c (lambda x.x)) s)));
c_croit_2 := lambda p v s c. p (lambda f. (croire ( f(c v)) s));
c_pense_2 := lambda p v s c. p (lambda f. (penser ( f(c v)) s));
NEG := lambda p. - p;
end
lexicon interpretation_3 (derivations):logic =
P_a := ((prop -> prop) -> prop) -> (prop -> prop) -> prop;
V_a := prop -> prop;
V := ind -> prop;
P := prop;
N := ind;
I_p:=lambda x.x;
I_v:= lambda x.x;
c_ira_a_Dax := lambda p v s. p (lambda f . f (v (aller_a_Dax s))) (lambda x.x);
c_Marie:=M;
c_Paul:=P;
c_Jane:=J;
c_croit_1 := lambda p v s c. p (lambda f. f (v (croire ( c ID ) s)));
c_pense_1 := lambda p v s c. p (lambda f. f (v (penser ( c ID) s)));
c_croit_2 := lambda p v s c. p (lambda f. (croire ( f(c v )) s));
c_pense_2 := lambda p v s c. p (lambda f. (penser ( f(c v)) s));
NEG := lambda p. - p;
end
Welcome to the ACG toplevel
Version 20110607
INRIA 2008
Please send your comments or bug reports or featrure requests to sylvain.pogodalla@loria.fr
Type
help ;
to get help.
# load d neg-raising.acg;
Parsing "neg-raising.acg"...
Done.
# read interpretation_3 analyse c_ira_a_Dax (c_croit_1 (c_pense_1 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul:P;
In derivations:
c_ira_a_Dax (c_croit_1 (c_pense_1 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul : P
c_ira_a_Dax (c_croit_1 (c_pense_1 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul : P
Interpreted by read in derived as:
P3 (N Marie) (V2 (V pense) pas) (P2 que (P3 (N Jane) (V croit) (P2 que (P3 (N (N Paul)) (V ira) a_Dax)))) : tree
Interpreted by interpretation_3 in logic as:
- (penser (croire (aller_a_Dax P) J) M) : prop
# read interpretation_3 analyse c_ira_a_Dax (c_croit_1 (c_pense_2 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul:P;
In derivations:
c_ira_a_Dax (c_croit_1 (c_pense_2 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul : P
c_ira_a_Dax (c_croit_1 (c_pense_2 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul : P
Interpreted by read in derived as:
P3 (N Marie) (V2 (V pense) pas) (P2 que (P3 (N Jane) (V croit) (P2 que (P3 (N (N Paul)) (V ira) a_Dax)))) : tree
Interpreted by interpretation_3 in logic as:
penser (- (croire (aller_a_Dax P) J)) M : prop
# read interpretation_3 analyse c_ira_a_Dax (c_croit_2 (c_pense_1 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul:P;
In derivations:
c_ira_a_Dax (c_croit_2 (c_pense_1 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul : P
c_ira_a_Dax (c_croit_2 (c_pense_1 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul : P
Interpreted by read in derived as:
P3 (N Marie) (V2 (V pense) pas) (P2 que (P3 (N Jane) (V croit) (P2 que (P3 (N (N Paul)) (V ira) a_Dax)))) : tree
Interpreted by interpretation_3 in logic as:
- (penser (croire (aller_a_Dax P) J) M) : prop
# read interpretation_3 analyse c_ira_a_Dax (c_croit_2 (c_pense_2 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul:P;
In derivations:
c_ira_a_Dax (c_croit_2 (c_pense_2 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul : P
c_ira_a_Dax (c_croit_2 (c_pense_2 I_p NEG c_Marie) I_v c_Jane) I_v c_Paul : P
Interpreted by read in derived as:
P3 (N Marie) (V2 (V pense) pas) (P2 que (P3 (N Jane) (V croit) (P2 que (P3 (N (N Paul)) (V ira) a_Dax)))) : tree
Interpreted by interpretation_3 in logic as:
penser (croire (- (aller_a_Dax P)) J) M : prop
# read interpretation_3 analyse c_ira_a_Dax (c_croit_1 (c_pense_1 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul:P;
In derivations:
c_ira_a_Dax (c_croit_1 (c_pense_1 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul : P
c_ira_a_Dax (c_croit_1 (c_pense_1 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul : P
Interpreted by read in derived as:
P3 (N Marie) (V pense) (P2 que (P3 (N Jane) (V2 (V croit) pas) (P2 que (P3 (N (N Paul)) (V ira) a_Dax)))) : tree
Interpreted by interpretation_3 in logic as:
penser (- (croire (aller_a_Dax P) J)) M : prop
# read interpretation_3 analyse c_ira_a_Dax (c_croit_1 (c_pense_2 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul:P;
In derivations:
c_ira_a_Dax (c_croit_1 (c_pense_2 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul : P
c_ira_a_Dax (c_croit_1 (c_pense_2 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul : P
Interpreted by read in derived as:
P3 (N Marie) (V pense) (P2 que (P3 (N Jane) (V2 (V croit) pas) (P2 que (P3 (N (N Paul)) (V ira) a_Dax)))) : tree
Interpreted by interpretation_3 in logic as:
penser (- (croire (aller_a_Dax P) J)) M : prop
# read interpretation_3 analyse c_ira_a_Dax (c_croit_2 (c_pense_1 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul:P;
In derivations:
c_ira_a_Dax (c_croit_2 (c_pense_1 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul : P
c_ira_a_Dax (c_croit_2 (c_pense_1 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul : P
Interpreted by read in derived as:
P3 (N Marie) (V pense) (P2 que (P3 (N Jane) (V2 (V croit) pas) (P2 que (P3 (N (N Paul)) (V ira) a_Dax)))) : tree
Interpreted by interpretation_3 in logic as:
penser (croire (- (aller_a_Dax P)) J) M : prop
# read interpretation_3 analyse c_ira_a_Dax (c_croit_2 (c_pense_2 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul:P;
In derivations:
c_ira_a_Dax (c_croit_2 (c_pense_2 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul : P
c_ira_a_Dax (c_croit_2 (c_pense_2 I_p I_v c_Marie) NEG c_Jane) I_v c_Paul : P
Interpreted by read in derived as:
P3 (N Marie) (V pense) (P2 que (P3 (N Jane) (V2 (V croit) pas) (P2 que (P3 (N (N Paul)) (V ira) a_Dax)))) : tree
Interpreted by interpretation_3 in logic as:
penser (croire (- (aller_a_Dax P)) J) M : prop
# read interpretation_3 analyse c_ira_a_Dax (c_croit_1 (c_pense_1 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul:P;
In derivations:
c_ira_a_Dax (c_croit_1 (c_pense_1 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul : P
c_ira_a_Dax (c_croit_1 (c_pense_1 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul : P
Interpreted by read in derived as:
P3 (N Marie) (V pense) (P2 que (P3 (N Jane) (V croit) (P2 que (P3 (N (N Paul)) (V2 (V ira) pas) a_Dax)))) : tree
Interpreted by interpretation_3 in logic as:
penser (croire (- (aller_a_Dax P)) J) M : prop
# read interpretation_3 analyse c_ira_a_Dax (c_croit_1 (c_pense_2 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul:P;
In derivations:
c_ira_a_Dax (c_croit_1 (c_pense_2 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul : P
c_ira_a_Dax (c_croit_1 (c_pense_2 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul : P
Interpreted by read in derived as:
P3 (N Marie) (V pense) (P2 que (P3 (N Jane) (V croit) (P2 que (P3 (N (N Paul)) (V2 (V ira) pas) a_Dax)))) : tree
Interpreted by interpretation_3 in logic as:
penser (croire (- (aller_a_Dax P)) J) M : prop
# read interpretation_3 analyse c_ira_a_Dax (c_croit_2 (c_pense_1 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul:P;
In derivations:
c_ira_a_Dax (c_croit_2 (c_pense_1 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul : P
c_ira_a_Dax (c_croit_2 (c_pense_1 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul : P
Interpreted by read in derived as:
P3 (N Marie) (V pense) (P2 que (P3 (N Jane) (V croit) (P2 que (P3 (N (N Paul)) (V2 (V ira) pas) a_Dax)))) : tree
Interpreted by interpretation_3 in logic as:
penser (croire (- (aller_a_Dax P)) J) M : prop
# read interpretation_3 analyse c_ira_a_Dax (c_croit_2 (c_pense_2 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul:P;
In derivations:
c_ira_a_Dax (c_croit_2 (c_pense_2 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul : P
c_ira_a_Dax (c_croit_2 (c_pense_2 I_p I_v c_Marie) I_v c_Jane) NEG c_Paul : P
Interpreted by read in derived as:
P3 (N Marie) (V pense) (P2 que (P3 (N Jane) (V croit) (P2 que (P3 (N (N Paul)) (V2 (V ira) pas) a_Dax)))) : tree
Interpreted by interpretation_3 in logic as:
penser (croire (- (aller_a_Dax P)) J) M : prop
#
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment