(* This files gives an example of how to use the ACG toolkit to illustrate
Montague's semantics *)
(* First we define the syntactic categories and the syntactic terms *)
signature syntax =
(* the np, s and n tpes *)
np, n, s : type;
(* the syntactic constants that correspond to John and Mary *)
JOHN, MARY : np;
(* the one for loves *)
LOVE : np -> np -> s;
(* the one for every and the one for some *)
EVERY, SOME : n -> (np -> s) -> s;
(* and the ones for man and woman *)
MAN, WOMAN : n;
end
(* Then we define the signature containing the strings that will be used *)
signature strings =
string : type;
(* the infix concatenation operator + *)
infix + : string -> string -> string;
(* the empty string e *)
e : string;
(* all the other strings *)
John, Mary, loves, every, some, man, woman : string;
end
(* The lexicon that associates the string to the syntactic terms *)
lexicon syntactic_realisation (syntax) : strings =
(* all the syntactic types are interpreted as strings *)
np, n, s := string;
JOHN := John;
MARY := Mary;
(* LOVE is interpreted as a function taking two arguments. The
first one is the object and the second one is the subject. It
returns the concatenation subject+loves+object *)
LOVE := lambda o s. s + loves + o;
EVERY := lambda n P. P (every + n);
SOME := lambda n P. P (some + n);
MAN := man;
WOMAN := woman;
end
(* Let's now look at the semantics *)
signature logic =
(* We define the usual types *)
e, t : type;
(* Then a few non logical-constants *)
love : e -> e -> t;
j, m : e;
man, woman : e -> t;
(* And finally, here are the logical constants *)
(* Conjunction *)
infix & : t -> t -> t;
(* Implication *)
infix > : t -> t -> t;
(* Quantifiers *)
binder All : (e => t) -> t;
binder Ex : (e => t) -> t;
end
lexicon semantics (syntax) : logic =
(* We interpret np as entity, n as properties (s -> t) and of course s as propositions (truth values) *)
np := e;
n := e -> t;
s := t;
JOHN := j;
MARY := m;
MAN := man;
WOMAN := woman;
(* Note that we interpret LOVE whose first argument is the object
and the second one is the subject using the predicate "love" for
which love x y is true whenever x loves y *)
LOVE := lambda x y. love y x ;
EVERY := lambda P Q. All x. (P x) > (Q x);
SOME := lambda P Q. Ex x. (P x) & (Q x);
end