montague.acg 2.33 KB
Newer Older
1 2
(* This files gives an example of how to use the ACG toolkit to illustrate
   Montague's semantics *)
3 4 5 6 7


(* First we define the syntactic categories and the syntactic terms *)
signature syntax =
	(* the np, s and n tpes *)
8
	np, n, s : type;
9

10 11
	(* the syntactic constants that correspond to John and Mary *)
	JOHN, MARY : np;
12 13

	(* the one for loves *)
14
	LOVE : np -> np -> s;
15 16

	(* the one for every and the one for some *)
17
	EVERY, SOME : n -> (np -> s) -> s;
18 19

	(* and the ones for man and woman *)
20
	MAN, WOMAN : n;
21 22 23
end


24
(* Then we define the signature containing the strings that will be used *)
25 26 27 28 29

signature strings =
	string : type;
	
	(* the infix concatenation operator + *)
30
	infix [Right] + : string -> string -> string;
31 32 33 34 35

	(* the empty string e *)
	e : string;

	(* all the other strings *)
36
	John, Mary, loves, every, some, man, woman : string;
37 38 39 40 41 42 43
end


(* The lexicon that associates the string to the syntactic terms *)

lexicon syntactic_realisation (syntax) : strings =
	(* all the syntactic types are interpreted as strings *)
44
	np, n, s := string;
45 46 47 48

	JOHN := John;
	MARY := Mary;

49 50 51 52
	(* 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;
53 54

	EVERY := lambda n P. P (every + n);
55
	SOME := lambda n P. P (some + n);
56 57 58 59 60 61 62 63 64 65 66
	
	MAN := man;
	WOMAN := woman;
end
	

(* Let's now look at the semantics *)

signature logic =

	(* We define the usual types *)
67
	e, t : type;
68

69 70 71 72
	(* Then a few non logical-constants *)
	love : e -> e -> t;
	j, m : e;
	man, woman : e -> t;
73 74 75

	(* And finally, here are the logical constants *)

76
	(* Conjunction *)
77 78
	infix & : t -> t -> t;	
	
79
	(* Implication *)
80 81 82
	infix > : t -> t -> t;

	(* Quantifiers *)
83 84
	binder All : (e => t) -> t;
	binder Ex : (e => t) -> t;
85 86
end

87

88 89 90 91 92 93 94 95 96 97 98 99 100
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;
	
101 102 103
	(* 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 *)
104 105
	LOVE := lambda x y. love y x ;
	
106 107
	EVERY := lambda P Q. All x. (P x) > (Q x); 
	SOME  := lambda P Q. Ex x. (P x) & (Q x);
108
end