(* 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")))
*)