Commit 8142636c authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

A variant of DRT modelling added

parent 2fece03f
signature syntax =
NP,S,NP_S_S : type;
G_q : NP_S_S -> (NP -> S) -> S;
CHRIS,KIM,DANA,SANDY:NP;
EV,SO:NP_S_S;
LIKE:NP -> NP -> S;
end
signature simple_syntax =
NP,S:type;
everybody,somebody:NP;
liked:NP -> NP -> S;
Chris,Kim,Dana,Sandy : NP;
end
lexicon CVG_syntax (syntax) : simple_syntax =
NP := NP;
S := S;
NP_S_S := NP;
G_q := lambda n r.r n;
EV := everybody;
SO := somebody;
LIKE := liked;
SANDY := Sandy;
DANA := Dana;
KIM := Kim;
CHRIS := Chris;
end
lexicon CVG_strings (simple_syntax) : strings =
NP,S:= string;
everybody := everyone;
somebody := someone;
liked := lambda o s . s + liked + o ;
Chris := Chris ;
Kim := Kim;
Dana := Dana ;
Sandy := Sandy ;
end
signature semantics =
e,t:type;
everybody',somebody': (e -> t) -> t;
chris',kim',dana',sandy':e;
like' : e -> e -> t;
end
lexicon CVG_semantics (syntax) : semantics =
NP := e;
S := t;
NP_S_S := (e ->t) -> t;
G_q := lambda q r.q r;
EV := everybody';
SO := somebody';
CHRIS := chris';
KIM := kim';
DANA := dana';
SANDY := sandy';
LIKE := lambda o s .like' s o;
end
signature ty_n =
e,t:type;
person',thing' : e -> t;
binder All : (e =>t) -> t;
binder Ex : (e =>t) -> t;
infix & : t -> t -> t;
infix > : t -> t -> t;
everybody' = lambda P.All x. (person' x) > (P x): (e->t) -> t;
somebody' = lambda P. Ex x. (person' x) & (P x): (e->t) -> t;
chris',kim',dana',sandy':e;
like' : e -> e -> t;
end
lexicon RC_ty (semantics) : ty_n =
e := e;
t :=t;
everybody':= everybody';
somebody' := somebody';
chris':= chris';
kim':= kim';
dana':= dana';
sandy':= sandy';
like' := like' ;
end
\ No newline at end of file
load d ../data/drt2.acg;
select drt;
analyse connait Marie Jean:s;
analyse connait (une fille) Jean:s;
analyse (connait (une fille) Jean) ! (salue la Jean) :s;
analyse (connait (une fille) Jean) ! (salue la il) :s;
drt analyse ((ne_pas (connait (une fille))) Jean) ! (salue la il) :s;
drt analyse ((ne_pas (connait (une fille))) Jean) ! (salue la Jean) :s;
drt analyse ((ne_pas (connait (une fille))) Jean) :s;
signature syntax =
np,n,s:type;
Jean,Marie:np;
connait,salue:np => np => s;
ne_pas : (np => s) => np => s;
fille:n;
il,la:np;
une:n=>np;
infix ! : s => s => s;
end
signature semantics =
e,t,g:type;
sel:g=>e;
infix + : e => g => g;
infix @ : g => g => g;
J,M:e;
connait,salue:e => e => t;
fille:e=>t;
Top,Bot:t;
infix & : t => t => t;
infix | : t => t => t;
binder Ex : (e => t) => t ;
binder All : (e => t) => t ;
prefix - : t => t ;
o = g => ( g => t =>t ) => t:type ;
vt = Lambda v O S.S(Lambda x.O(Lambda y.Lambda e phi. phi e (v x y))) : (e => e => t) => ((e =>o ) => o) => ((e =>o ) => o) => o ;
n = Lambda n .Lambda x.Lambda e phi. phi e (n x) : (e => t) => e => o;
end
lexicon drt (syntax):semantics =
s := o;
np := (e => o) => o;
n := e => o;
! := Lambda s1 s2 e phi. s1 e (Lambda e' b'. s2 e' (Lambda e'' b''. phi e'' (b' & b''))) ;
Jean := Lambda P e phi. P J (J+e) phi ;
Marie := Lambda P e phi. P M (M+e) phi ;
connait := vt connait;
ne_pas := Lambda P S e phi. phi e (-((P S) e (Lambda e b. b)));
(* ne_pas := Lambda P S e phi. (P S) e (Lambda e' b .phi e (- b)) ; *)
salue := vt salue;
fille := n fille;
il,la := Lambda P e phi.P (sel e) e phi;
une := Lambda P Q e phi. Ex x. phi (x+e) ((P x e (Lambda e' b.b)) & (Q x e (Lambda e' b.b)));
end
load d ../data/drt3.acg;
drt analyse ((ne_pas (connait (une fille))) Jean) ! (salue la Jean) :s;
drt analyse (connait (une fille) Jean) ! (salue la Jean) :s;
drt analyse ((ne_pas (connait (une fille))) Jean) ! (salue la il) :s;
drt analyse (connait (une fille) Jean) ! (salue la il) :s;
drt analyse (connait (une fille) Jean) ! (dort Marie) :s;
drt analyse ((ne_pas (connait (une fille))) Jean) ! (dort Marie) :s;
drt analyse (((ne_pas (connait (une fille))) Jean) ! (dort Marie))!(dort Jean) :s;
drt analyse (((ne_pas (connait (une fille))) Jean) ! (dort il))!(dort il) :s;
drt analyse ((connait (une fille) Jean) ! (dort Marie))!(dort Jean) :s;
drt analyse ((connait (une fille) Jean) ! (dort il))!(dort Jean) :s;
drt analyse (((ne_pas (connait (une fille))) Jean) ! (dort il))!(dort Jean) :s;
signature syntax =
np,n,s:type;
Jean,Marie:np;
connait,salue:np => np => s;
dort : np => s;
ne_pas : (np => s) => np => s;
fille:n;
il,la:np;
une:n=>np;
infix ! : s => s => s;
end
signature semantics =
e,t,g:type;
sel:g=>e;
infix + : e => g => g;
infix @ : g => g => g;
J,M:e;
connait,salue:e => e => t;
dort: e=>t;
fille:e=>t;
Top,Bot:t;
infix & : t => t => t;
infix | : t => t => t;
binder Ex : (e => t) => t ;
binder All : (e => t) => t ;
prefix - : t => t ;
k = t => t => t :type ;
o = k => g => g => ( k => g => g => t =>t ) => t:type ;
vt = Lambda v O S.S(Lambda x.O(Lambda y.Lambda c e1 e2 phi. phi c e1 e2 (v x y))) : (e => e => t) => ((e =>o ) => o) => ((e =>o ) => o) => o ;
vi = Lambda v S.S (Lambda x c e1 e2 phi. phi c e1 e2 (v x)) : (e => t) => ((e =>o ) => o) => o ;
n = Lambda n .Lambda x.Lambda c e1 e2 phi. phi c e1 e2 (n x) : (e => t) => e => o;
neg = Lambda P x y.- (P x y): (t => t => t) => t => t => t;
end
lexicon drt (syntax):semantics =
s := o;
np := (e => o) => o;
n := e => o;
! := Lambda s1 s2 c e1 e2 phi. s1 c e1 e2 (Lambda c' e1' e2' b'. s2 c' e1' e2' (Lambda c'' e1'' e2'' b''. phi c'' e1'' e2'' (c b' b''))) ;
Jean := Lambda P c e1 e2 phi. P J c (J+e1) e2 phi ;
Marie := Lambda P c e1 e2 phi. P M c (M+e1) e2 phi ;
connait := vt connait;
dort := vi dort;
(* ne_pas := Lambda P S c e1 e2 phi. phi (Lambda x y .- (c x y)) e1 e2 (-((P S) c e1 e2 (Lambda c' e1 e2 b. b))); *)
ne_pas := Lambda P S c e1 e2 phi. - ( (P S) (neg c) e1 e2 (Lambda c' e1' e2' b' . phi (neg c) e1' e2 b'));
salue := vt salue;
fille := n fille;
il,la := Lambda P c e1 e2 phi.P (sel (e1@e2)) c e1 e2 phi;
une := Lambda P Q c e1 e2 phi. Ex x. phi c e1 (x+e2) (c (P x c e1 e2 (Lambda c' e1' e2' b.b)) (Q x c e1 (x+e2) (Lambda c' e1' e2' b.b)));
end
signature syntax =
np,n,s:type;
Jean,Marie:np;
connait,salue:np => np => s;
ne_pas : (np => s) => np => s;
fille:n;
il,la:np;
une:n=>np;
infix ! : s => s => s;
end
signature semantics =
e,t,g:type;
sel:g=>e;
infix + : e => g => g;
infix @ : g => g => g;
J,M:e;
connait,salue:e => e => t;
fille:e=>t;
Top,Bot:t;
infix & : t => t => t;
infix | : t => t => t;
binder Ex : (e => t) => t ;
binder All : (e => t) => t ;
prefix - : t => t ;
k = t => t => t :type ;
o = g => g => ( g => g => t =>t ) => t:type ;
vt = Lambda v O S.S(Lambda x.O(Lambda y.Lambda e1 e2 phi. phi e1 e2 (v x y))) : (e => e => t) => ((e =>o ) => o) => ((e =>o ) => o) => o ;
n = Lambda n .Lambda x.Lambda c e1 e2 phi. phi e1 e2 (n x) : (e => t) => e => o;
end
lexicon drt (syntax):semantics =
s := o;
np := (e => o) => o;
n := e => o;
! := Lambda s1 s2 e1 e2 phi. s1 e1 e2 (Lambda e1' e2' b'. s2 e1' e2' (Lambda e1'' e2'' b''. phi e1'' e2'' (b' & b''))) ;
Jean := Lambda P e1 e2 phi. P J (J+e1) e2 phi ;
Marie := Lambda P e1 e2 phi. P M (M+e1) e2 phi ;
connait := vt connait;
ne_pas := Lambda P S e1 e2 phi. phi e1 e2 (-((P S) c e1 e2 (Lambda e1 e2 b. b)));
(* ne_pas := Lambda P S c e1 e2 phi. - ( (P S) (Lambda x y. - (c x y)) e1 e2 (Lambda c' e1' e2' b' . phi (Lambda x y. - (c x y)) e1' e2 b')); *)
salue := vt salue;
fille := n fille;
il,la := Lambda P c e1 e2 phi.P (sel (e1@e2)) c e1 e2 phi;
une := Lambda P Q c e1 e2 phi. Ex x. phi c e1 (x+e2) (c (P x c e1 e2 (Lambda c' e1' e2' b.b)) (Q x c e1 e2 (Lambda c' e1' e2' b.b)));
end
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