(* ACG with a more expressive semantic lexicon that includes multi-prompt delimited continuations and the notion of evaluation. Types are considered as a mere approximation rather than the complete specification of grammatical composition. In this file, we analyze the following examples posed by Carl Pollard: (1) A donkey enters. It brays. (2) Every donkey enters. *It brays. (3) It-is-not-the-case-that a donkey enters. *It brays. (4) A donkey and a mule enter. *It brays. (5) A donkey and a mule enter. The donkey brays. (6) A donkey enters. It-is-not-the-case-that it brays. (7) Every donkey denies it brays. *) (* The abstract form, to be interpreted in several ways. *) (* Abstract signature, which defines base types, constants and their types *) module type Abstract = sig type n (* base types *) type np type s type d (* The complete discourse *) (* constants and their types *) val donkey : n val mule : n val deny : s -> np -> s val enter : np -> s val bray : np -> s val every : n -> np val a : n -> np val the : n -> np val it : np val and_ : np -> np -> np val no_way : s -> s val dot : s -> s -> s (* A period combines two sentences *) val par : s -> d (* The end of the discourse mark *) end;; (* Sample phrases in the abstract language *) (* Example (1) *) module Ex1(A: Abstract) = struct open A let term = par ( dot (enter (a donkey)) (bray it)) end;; (* Example (2), first sentence only *) module Ex21(A: Abstract) = struct open A let sentence = enter (every donkey) let term = par sentence end;; (* Example (2), both sentences *) module Ex22(A: Abstract) = struct open A module S1 = Ex21(A) let sentence2 = bray it let term = par (dot S1.sentence sentence2) end;; (* Example (3) *) module Ex31(A: Abstract) = struct open A let term = par (no_way (enter (a donkey))) end;; module Ex3(A: Abstract) = struct open A let term = par ( dot (no_way (enter (a donkey))) (bray it)) end;; module Ex4(A: Abstract) = struct open A let term = par ( dot (enter (and_ (a donkey) (a mule))) (bray it)) end;; module Ex5(A: Abstract) = struct open A let term = par ( dot (enter (and_ (a donkey) (a mule))) (bray (the donkey))) end;; module Ex6(A: Abstract) = struct open A let term = par ( dot (enter (a donkey)) (no_way (bray it))) end;; module Ex7(A: Abstract) = struct open A let term = par ( (deny (bray it) (every donkey))) end;; (* An interpretation of the abstract signature as the surface form: strings *) (* This is literally L_syntax in Sec 4.4 of the ESSLLI Advanced ACG course, only written in OCaml *) module Syntax = struct type n = string (* All types are interpreted as *) type np = string (* strings *) type s = string type d = string let donkey = "donkey" let mule = "mule" let deny = fun o s -> s ^ " denied " ^ o let enter = fun x -> x ^ " entered" let bray = fun x -> x ^ " brayed" let every = fun x -> "every " ^ x let a = fun x -> "a " ^ x let the = fun x -> "the " ^ x let it = "it" let and_ = fun np1 np2 -> np1 ^ " and " ^ np2 let no_way = fun x -> "It-is-not-the-case-that " ^ x let dot = fun s1 s2 -> s1 ^ ". " ^ s2 let par = fun s -> s ^ "." end;; (* Surface forms of sample terms *) let module Ex1S = Ex1(Syntax) in Ex1S.term;; (* - : Syntax.d = "a donkey entered. it brayed." *) let module Ex21S = Ex21(Syntax) in Ex21S.term;; (* - : Syntax.d = "every donkey entered." *) let module Ex22S = Ex22(Syntax) in Ex22S.term;; (* - : Syntax.d = "every donkey entered. it brayed." *) let module Ex31S = Ex31(Syntax) in Ex31S.term;; (* - : Syntax.d = "It-is-not-the-case-that a donkey entered." *) let module Ex3S = Ex3(Syntax) in Ex3S.term;; (* - : Syntax.d = "It-is-not-the-case-that a donkey entered. it brayed." *) let module Ex4S = Ex4(Syntax) in Ex4S.term;; (* - : Syntax.d = "a donkey and a mule entered. it brayed." *) let module Ex5S = Ex5(Syntax) in Ex5S.term;; (* - : Syntax.d = "a donkey and a mule entered. the donkey brayed." *) let module Ex6S = Ex6(Syntax) in Ex6S.term;; (* - : Syntax.d = "a donkey entered. It-is-not-the-case-that it brayed." *) let module Ex7S = Ex7(Syntax) in Ex7S.term;; (* - : Syntax.d = "every donkey denied it brayed." *) (* ------------------------------------------------------------------------ *) (* Semantic forms *) (* Hypotheses: -- Universals cannot scope wider than an individual sentence (matrix). In jargon: the prompt puni is set at the sentence boundary. -- Existentials and indefinites can scope discourse-wide, wider than an individual sentence (matrix). In jargon: the prompt pexi is not set at the sentence boundary. -- Pronouns can bind discourse-wide, wider than a sentence. In jargon: a sentence boundary does not set the `pit' prompt and the corresponding pit interpreter. -- Coordinator AND limits the scope of quantification and binding. In jargon: AND sets the puni, pexi and pit prompts for each branch of the coordination. -- It-is-not-the-case limits the scope of indefinites (at least). In jargon: It-is-not-the-case sets the pexi prompt. -- Quantifiers store the quantified variable for future reference. Strictly speaking, we could have been more specific and use the `store' operation explicitly. It seems the implicit `store' suffices for the examples at hand. -- Quantifiers generate a new binding locus at the point of quantification. The initial value is not empty: rather, it inherits whatever binding existed (at the point of quantification? or at the point of QP? For the present examples, either works. We need more examples to be able to tell the difference). The insertion of the binding locus is the necessity, to prevent the bound variable from `leaking out' (so-called `scope extrusion' in partial evaluation). *) open Delimcc;; (* Load the library of multi-prompt shift *) (* The following defines the language of logic forms: first-order logic formulas that describe meanings. *) type e = | Ind of string | Iota of (varname * t) and t = | Donkey of e | Mule of e | Enter of e | Bray of e | Deny of t * e (* Standard FOL *) | And of t * t | Imply of t * t | Not of t | Exists of (varname * t) | Forall of (varname * t) and varname = string ;; (* Generator of variable names, which we need to build higher-order terms. *) let gensym = let counter = ref 0 in fun () -> incr counter; "x" ^ string_of_int !counter ;; let make_ind_quant quant body = let v = gensym () in quant (v, body (Ind v)) ;; (* Auxiliary functions to support binding. We associate with each locus of binding a `storage cell', initially empty. *) (* `Store' an entity at the place marked by pit for future reference *) let store pit e = shift pit (fun sk -> fun _ -> (sk e) (Some e)) ;; (* Retrieve entity from the storage cell associated with pit. This function is partial! If the storage cell is empty -- nothing was bound -- the reference operation fails, reporting an error. No denotation is computed then. So, "It entered." as a single sentence of the discourse is meaningless. *) let refer pit = shift pit (fun sk -> function | (Some x) as v -> (sk x) v | _ -> failwith "It is not bound.") ;; let bind_locus pit thunk = (push_prompt pit (fun () -> let v = thunk () in fun _ -> v)) None ;; let bind_locus_inherit pit thunk = let cell = shift pit (fun sk v -> sk v v) in (push_prompt pit (fun () -> let v = thunk () in fun _ -> v)) cell ;; (* We now build the semantic signature and the lexicon -- stepwise *) module Sem = struct (* Interpretations of base types *) (* `unit' is for technical reasons: our *) (* calculus is call-by-value rather than*) (* call-by-name *) type np = unit -> e type n = (unit -> e) -> (unit -> t) type s = unit -> t type d = t (* Prompts, or context marks *) let psen = new_prompt () let puni = new_prompt () (* Place for the universal *) let pexi = new_prompt () (* Place for the existential *) let pit = new_prompt () (* Locus of binding *) let donkey = fun x () -> Donkey (x ()) let mule = fun x () -> Mule (x ()) let enter = fun x () -> Enter (x ()) let bray = fun x () -> Bray (x ()) let deny = fun o s () -> let sv = s () in let ov = o () in Deny (ov,sv) let no_way = fun x () -> Not (push_prompt pexi x) let every = fun pred () -> shift puni (fun k -> bind_locus_inherit pit (fun () -> make_ind_quant (fun b -> Forall b) (fun x -> Imply (pred (fun () -> x) (),k (store pit x))))) let a = fun pred () -> shift pexi (fun k -> bind_locus_inherit pit (fun () -> make_ind_quant (fun b -> Exists b) (fun x -> And (pred (fun () -> x) (),k (store pit x))))) let it = fun () -> refer pit (* The prompt pexi is not set at the sentence boundary *) let dot s1 s2 () = let s1v = push_prompt psen (fun () -> push_prompt puni s1) in let s2v = push_prompt psen (fun () -> push_prompt puni s2) in And (s1v, s2v) (* The order is important! In the order below, existentials scope under universals *) let set_scoping s = bind_locus pit (fun () -> push_prompt puni (fun () -> push_prompt pexi (fun () -> s ()))) let par s = push_prompt psen (fun () -> set_scoping s) let and_ = fun (np1:np) np2 () -> shift psen (fun k -> And (set_scoping (fun () -> k np1), set_scoping (fun () -> k np2))) () let the = fun x () -> make_ind_quant (fun b -> Iota b) (fun e -> x (fun () -> e) ()) end;; let module Ex1L = Ex1(Sem) in Ex1L.term;; (* Exists ("x1", And (Donkey (Ind "x1"), And (Enter (Ind "x1"), Bray (Ind "x1")))) *) let module Ex21L = Ex21(Sem) in Ex21L.term;; (* - : Sem.d = Forall ("x2", Imply (Donkey (Ind "x2"), Enter (Ind "x2"))) *) try let module Ex22L = Ex22(Sem) in assert false with e -> e ;; (* - : exn = Failure "It is not bound." *) let module Ex31L = Ex31(Sem) in Ex31L.term;; (* - : Sem.d = Not (Exists ("x5", And (Donkey (Ind "x5"), Enter (Ind "x5")))) *) try let module Ex3 = Ex3(Sem) in assert false with e -> e ;; (* - : exn = Failure "It is not bound." *) try let module Ex4 = Ex4(Sem) in assert false with e -> e ;; (* - : exn = Failure "It is not bound." *) let module Ex5L = Ex5(Sem) in Ex5L.term;; (* And (And (Exists ("x10", And (Donkey (Ind "x10"), Enter (Ind "x10"))), Exists ("x9", And (Mule (Ind "x9"), Enter (Ind "x9")))), Bray (Iota ("x11", Donkey (Ind "x11")))) *) let module Ex6L = Ex6(Sem) in Ex6L.term;; (* - : Sem.d = Exists ("x12", And (Donkey (Ind "x12"), And (Enter (Ind "x12"), Not (Bray (Ind "x12"))))) *) let module Ex7L = Ex7(Sem) in Ex7L.term;; (* - : Sem.d = Forall ("x13", Imply (Donkey (Ind "x13"), Deny (Bray (Ind "x13"), Ind "x13"))) *)