(* 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.
Our examples are scope ambiguity in quantified phrases with conjunction
and verbal ellipsis.
Sec 4.4 from
http://www.loria.fr/equipes/calligramme/acg/publications/esslli-09/2009-esslli-acg-week-2-part-2.pdf
*)
(* 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 sm (* Complete sentence, the matrix *)
val john : np (* constants *)
val bill : np
val man : n
val woman : n
val kid : n
val see : np -> np -> s
val love : np -> np -> s
val ran : np -> s
val every : n -> np
val some : n -> np
val a : n -> np
val and_ : np -> np -> np
val didnt : (np -> s) -> np -> s (* Should've introduced the type vp,
to keep the signature low order.
But we follow the ESSLLI notes literally.
*)
val that : n -> (np -> s) -> n (* Restrictive relative clauses *)
val dot : s -> sm (* Terminating dot *)
end;;
(* Sample phrases in the abstract language *)
(* Example from Sec 4.3 of the ESSLLI Advanced ACG course. *)
module Ex43(A: Abstract) = struct
open A
let term = dot (love (some woman) (every man))
end;;
(* Example (2) from Sec 4.4 of the ESSLLI Advanced ACG course. *)
(* The encoding is exactly t3 of Sec 4.4
*)
module Ex442(A: Abstract) = struct
open A
let term = dot (ran (and_ john (every kid)))
end;;
(* Example (3c) from Sec 4.4 of the ESSLLI Advanced ACG course. *)
(* The encoding is exactly t11 of Sec 4.4.3
*)
module Ex443c(A: Abstract) = struct
open A
let term = dot (didnt ran (every kid))
end;;
(* Example (4) from Sec 4.4.4 of the ESSLLI Advanced ACG course. *)
(* The example can't be handled with ACG at present
*)
module Ex444(A: Abstract) = struct
open A
let term = dot (ran (a (that man (fun np -> see np (every woman)))))
end;;
(* An interpretation of the abstract signature as the surface form: strings *)
(* This is literally L_syntax in Sec 4.4, only written in OCaml *)
module Syntax = struct
type n = string
type np = string
type s = string
type sm = string
let john = "John"
let bill = "Bill"
let man = "man"
let woman = "woman"
let kid = "kid"
let every = fun x -> "every " ^ x
let some = fun x -> "some " ^ x
let a = fun x -> "a " ^ x
let ran = fun x -> x ^ " ran"
let see = fun o s -> s ^ " saw " ^ o
let love = fun o s -> s ^ " loves " ^ o
let and_ = fun np1 np2 -> np1 ^ " and " ^ np2
let didnt = fun vp -> fun x -> x ^ " didn't" ^ (vp "")
let that = fun n -> fun cl -> n ^ " that " ^ (cl "")
let dot = fun s -> s ^ "."
end;;
(* Surface forms of sample terms *)
let module Ex43S = Ex43(Syntax) in Ex43S.term;;
(*
- : Syntax.sm = "every man loves some woman."
*)
let module Ex442S = Ex442(Syntax) in Ex442S.term;;
(*
- : Syntax.sm = "John and every kid ran."
*)
let module Ex443cS = Ex443c(Syntax) in Ex443cS.term;;
(*
- : Syntax.sm = "every kid didn't ran."
*)
let module Ex444S = Ex444(Syntax) in Ex444S.term;;
(*
- : Syntax.sm = "a man that every woman saw ran."
*)
(* ------------------------------------------------------------------------ *)
(* Semantic forms *)
(* The domain of truth values *)
module type Logic = sig
type t
type varname
type var
type quant_t = varname -> t -> t (* Quantified formula *)
val conj : t -> t -> t
val impl : t -> t -> t
val not : t -> t
val exists : quant_t
val forall : quant_t
val quantify : quant_t -> (var -> t) -> t
end;;
(* This is literally Sig_sem of Sec 4.3 *)
module type Meaning = sig
include Logic
type e
val ind : string -> e
val indvar : var -> e
val man' : e -> t
val woman' : e -> t
val kid' : e -> t
val run' : e -> t
val see' : e -> e -> t
val love' : e -> e -> t
val make_ind_quant : quant_t -> (e -> t) -> t
end;;
(* We can interpret meanings in several ways: for example, we
can evaluate propositions in a particular world.
For now, we are most interested in one particular interpretations:
printing out the formulas in a nice way.
*)
(* We interpret all semantic types as strings, as text formulas *)
(* As we show formulas, we check that all variables are bound in the
environment. The function show_closed_fml makes sure that only
closed formulas can be shown.
The current implementation is a bit of a hack. The scope extrusion
can be detected well ahead of showing formulas. We need to pass the env
to every formula, so the type of formulas in the Logic signature
should be [varname] -> t rather than t.
*)
module ShowLogic = struct
type prec = int
type varname = string
type env = varname list
type var = env -> string
type t = env -> prec -> string
type quant_t = varname -> t -> t
let paren cond text = if cond then "(" ^ text ^ ")" else text
let conj e1 e2 = fun env p -> paren (p > 3) (e1 env 4 ^ " & " ^ e2 env 3)
let impl e1 e2 = fun env p -> paren (p > 2) (e1 env 3 ^ " => " ^ e2 env 2)
let not e1 = fun env p -> paren (p > 10) ("~" ^ e1 env 11)
let exists v e = fun env p ->
paren (p > 0) ("E" ^ v ^ ". " ^ e (v::env) 0)
let forall v e = fun env p ->
paren (p > 0) ("A" ^ v ^ ". " ^ e (v::env) 0)
let app1 op arg1 = fun env p ->
paren (p > 10) (op env 10 ^ " " ^ arg1 env 11)
let app2 op arg1 arg2 = fun env p ->
paren (p > 10) (op env 10 ^ " " ^ arg1 env 11 ^ " " ^ arg2 env 11)
let gensym =
let counter = ref 0 in
fun () -> incr counter; "x" ^ string_of_int !counter
let quantify quant body =
let vname = gensym () in
let v = fun env ->
if List.mem vname env then vname else
(ignore (Printf.printf "%s\n"
("\n!!!Unbound var " ^ vname ^ " in the env [" ^
List.fold_left (fun acc vn ->
if acc = "" then vn else ", " ^ vn)
"" env ^ "]")); vname) in
let body' = body v in
quant vname body'
let show_closed_fml e = e [] 0
end;;
let show_closed_fml = ShowLogic.show_closed_fml;; (* Useful abbreviation *)
module ShowMeaning = struct
include ShowLogic
type e = env -> prec -> string
let ind name = fun env p -> name
let indvar var = fun env p -> var env
let man' = app1 (fun _ p -> "man")
let woman' = app1 (fun _ p -> "woman")
let kid' = app1 (fun _ p -> "kid")
let run' = app1 (fun _ p -> "run")
let see' = app2 (fun _ p -> "see")
let love' = app2 (fun _ p -> "love")
let make_ind_quant quant body =
quantify quant (fun var -> body (indvar var))
end;;
(* ------------------------------------------------------------------------ *)
(* Syntax-Semantics interface *)
open Delimcc;; (* Load the library of multi-prompt shift *)
(* We now build the semantic signature and the lexicon -- stepwise *)
module Sem1(S: Meaning) = struct
open S
type np = unit -> e
(* The following type for n describes Nbar, or ``complex common nouns''
with complements such as prepositional phrases.
*)
type n = unit -> (unit -> e) -> t
type s = unit -> t
type sm = t
let psen = new_prompt ()
let puni = new_prompt ()
let pexi = new_prompt ()
let john = fun () -> ind "John'"
let bill = fun () -> ind "Bill'"
let man = fun () x -> man' (x ())
let woman = fun () x -> woman' (x ())
let kid = fun () x -> kid' (x ())
let ran = fun x () -> run' (x ())
let love = fun o s () -> let sv = s () in
let ov = o () in love' ov sv
let see = fun o s () -> let sv = s () in
let ov = o () in see' ov sv
let every = fun n () ->
let nv = n () in (* evaluate Nbar first *)
shift puni (fun k ->
make_ind_quant forall (fun x ->
impl (nv (fun () -> x)) (k x)))
let some = fun n () ->
let nv = n () in (* evaluate Nbar first *)
shift pexi (fun k ->
make_ind_quant exists (fun x ->
conj (nv (fun () -> x)) (k x)))
let a = some
let dot s =
push_prompt psen (fun () ->
push_prompt puni (fun () ->
push_prompt pexi (fun () ->
s ())))
let and_ = fun (np1:np) np2 () -> shift psen (fun k ->
conj (k np1) (k np2)) ()
let didnt = fun (vp:np->s) np () -> shift psen (fun k ->
not (k (vp np))) ()
let that = fun (n:n) clause () ->
let nv = n () in
fun (x:np) -> conj (nv x) (dot (clause x))
end;;
(* A different semantic signature, a refinement of SemBasic specifying
a different sequence of prompts.
*)
module Sem2(S: Meaning) = struct
include Sem1(S)
let dot s =
push_prompt psen (fun () ->
push_prompt pexi (fun () ->
push_prompt puni (fun () ->
s ())))
end;;
(* The result is identical to that at the end of Sec 4.3 *)
let module Ex43L1 = Ex43(Sem1(ShowMeaning)) in show_closed_fml Ex43L1.term;;
(*
- : string = "Ax3. man x3 => (Ex4. woman x4 & love x4 x3)"
*)
let module Ex43L1 = Ex43(Sem2(ShowMeaning)) in show_closed_fml Ex43L1.term;;
(*
- : string = "Ex6. woman x6 & (Ax5. man x5 => love x6 x5)"
*)
let module Ex442L = Ex442(Sem1(ShowMeaning)) in show_closed_fml Ex442L.term;;
(*
- : string = "run John' & (Ax11. kid x11 => run x11)"
*)
(* We have just reproduced the logical form L(t12) of Sec 4.4.3 *)
let module Ex443cL = Ex443c(Sem1(ShowMeaning)) in show_closed_fml Ex443cL.term;;
(*
- : string = "~(Ax12. kid x12 => run x12)"
*)
(* Quantifier scopes wider: We have just reproduced the logical form L(t13)
of Sec 4.4.3 *)
let module Ex443cL2 = Ex443c(
struct
include Sem1(ShowMeaning)
let didnt = fun (vp:np->s) np () -> ShowMeaning.not ((vp np) ())
end) in show_closed_fml Ex443cL2.term;;
(*
- : string = "Ax13. kid x13 => ~(run x13)"
*)
let module Ex444L = Ex444(Sem1(ShowMeaning)) in show_closed_fml Ex444L.term;;
(*
- : string = "Ex14. (man x14 & (Ax15. woman x15 => see x14 x15)) & run x14"
*)
(* Here, the universal cannot scope over the existential because a
relative clause, like `dot', restricts the scope of all
embedded quantifiers.
In our analysis, we assume that all quantifiers within a clause cannot
take scope outside of the clause.
Of course, this is an approximation: Some quantifiers do take scope
wider than the scope of the containing clause; for example, `each'.
But we can deal with them by defining a new prompt p_each and differentiating
the clause boundary from the sentence boundary. Whereas the sentence
boundary sets all the prompts (nothing can take the wider scope than
that of a sentence), the relative clause's `that' does not set the
p_each prompt and so does not restrict the scope for `each'.
*)