Barker (2002): Continuations and the nature of quantification

This file formalizes Barker's continuized grammar. A continuation is what the rest of the sentence does with a constituent's value, and continuizing a grammar hands every constituent its continuation. Noun phrases then come out as generalized quantifiers, everyone and someone can be stated in situ, and they take scope without movement, storage or type-shifting. A rule with two daughters continuizes in two ways, one per priority order of the daughters, which is where scope ambiguity comes from. A scope island hands its continuation the finished clause, and coordination distributes its continuation over the conjuncts.

A derivation is a tree over the direct grammar with each binary node marked for priority. Deriv.continuize is the Continuation Schema, Deriv.direct the meaning the direct grammar assigns, and Deriv.scopeOrder the order in which the quantificational items take scope. The Simulation Theorem (Deriv.continuize_eq_pure) says that a derivation the direct grammar interprets denotes its direct meaning, and Integrity (Deriv.Constituent.scopeOrder_isInfix) that the quantifiers of a constituent are contiguous in the scope order of the sentence.

Implementation notes

• The paper states the schema for rules of any arity, with one continuized rule per permutation of the daughters. Its grammar has rules of arity at most two, and so does Deriv.
• The expository determiners, which apply to the continuized nominal, are Deriv.bind at a generalized-quantifier denotation. The determiners of the final grammar quantify over choice functions.
• Transitive verbs take the object first, so saw m j is John saw Mary.

TODO

The paper calls the four scopings of someone saw a friend of everyone logically distinct. The restrictor of a contains the variable that everyone binds, so by Reference.ChoiceFunction.exists_forall_apply_iff the two scopings that differ in the order of a and everyone are equivalent (a_everyone_iff_everyone_a), and the grammar gives the sentence two truth conditions. A wide-scope a friend common to everyone is not among them.

References

• [Bar02a]
• [PR83]
• [Rei97]

Derivations and the Continuation Schema

inductive Barker2002.Priority : Type

The daughter of a binary rule that takes priority, and with it scope over the other.

• left : Priority
• right : Priority

@[instance_reducible]

instance Barker2002.instDecidableEqPriority : DecidableEq Priority

Equations

• Barker2002.instDecidableEqPriority x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Barker2002.instFintypePriority : Fintype Priority

Equations

• Barker2002.instFintypePriority = { elems := { val := ↑Barker2002.Priority.enumList, nodup := Barker2002.Priority.enumList_nodup }, complete := Barker2002.instFintypePriority._proof_1 }

inductive Barker2002.Deriv (ι : Type) : Type → Type 1

A derivation with quantificational items labelled in ι is a lexical item of the direct grammar, a quantificational item stated only in continuized terms, a rule of arity one or two applied to its daughters, a quantificational item applied to the value of its daughter, a clause closed off as a scope island, or a coordination.

• lex {ι α : Type} (a : α) : Deriv ι α
• quant {ι α : Type} (i : ι) (q : Cont Prop α) : Deriv ι α
• unary {ι α β : Type} (M : α → β) (d : Deriv ι α) : Deriv ι β
• binary {ι α β γ : Type} (M : α → β → γ) (p : Priority) (d₁ : Deriv ι α) (d₂ : Deriv ι β) : Deriv ι γ
• bind {ι α β : Type} (i : ι) (q : α → Cont Prop β) (d : Deriv ι α) : Deriv ι β
• island {ι : Type} (d : Deriv ι Prop) : Deriv ι Prop
• coord {ι α : Type} (d₁ d₂ : Deriv ι α) : Deriv ι α

def Barker2002.Deriv.continuize {ι α : Type} : Deriv ι α → Cont Prop α

The Continuation Schema makes a lexical item a unit and has a rule nest the continuations of its daughters in priority order. An island evaluates its clause, and coordination hands its continuation to each conjunct.

Equations

• (Barker2002.Deriv.lex a).continuize = pure a
• (Barker2002.Deriv.quant i q).continuize = q
• (Barker2002.Deriv.unary M d).continuize = M <$> d.continuize
• (Barker2002.Deriv.binary M Barker2002.Priority.left d₁ d₂).continuize = M <$> d₁.continuize <*> d₂.continuize
• (Barker2002.Deriv.binary M Barker2002.Priority.right d₁ d₂).continuize = flip M <$> d₂.continuize <*> d₁.continuize
• (Barker2002.Deriv.bind i q d).continuize = d.continuize >>= q
• d.island.continuize = ContT.reset d.continuize
• (d₁.coord d₂).continuize = fun (k : x✝ → Id Prop) => d₁.continuize k ∧ d₂.continuize k

def Barker2002.Deriv.eval {ι : Type} (d : Deriv ι Prop) : Prop

The sentence meaning is the continuized meaning at the trivial continuation.

Equations

• d.eval = ContT.eval d.continuize

def Barker2002.Deriv.direct {ι α : Type} : Deriv ι α → Option α

The meaning the direct grammar assigns, where it assigns one.

Equations

• (Barker2002.Deriv.lex a).direct = some a
• (Barker2002.Deriv.unary M d).direct = Option.map M d.direct
• (Barker2002.Deriv.binary M p d₁ d₂).direct = d₁.direct.bind fun (x : α) => Option.map (M x) d₂.direct
• d.island.direct = d.direct
• (Barker2002.Deriv.quant i q).direct = none
• (Barker2002.Deriv.bind i q d).direct = none
• (d₁.coord d₂).direct = none

def Barker2002.Deriv.scopeOrder {ι α : Type} : Deriv ι α → List ι

The quantificational items in the order they take scope. Those of an island are trapped, and those of a coordination are listed together although neither conjunct outscopes the other.

Equations

• (Barker2002.Deriv.lex a).scopeOrder = []
• d.island.scopeOrder = []
• (Barker2002.Deriv.quant i q).scopeOrder = [i]
• (Barker2002.Deriv.unary M d).scopeOrder = d.scopeOrder
• (Barker2002.Deriv.binary M Barker2002.Priority.left d₁ d₂).scopeOrder = d₁.scopeOrder ++ d₂.scopeOrder
• (d₁.coord d₂).scopeOrder = d₁.scopeOrder ++ d₂.scopeOrder
• (Barker2002.Deriv.binary M Barker2002.Priority.right d₁ d₂).scopeOrder = d₂.scopeOrder ++ d₁.scopeOrder
• (Barker2002.Deriv.bind i q d).scopeOrder = d.scopeOrder ++ [i]

Simulation

theorem Barker2002.Deriv.continuize_eq_pure {ι α : Type} {d : Deriv ι α} {a : α} (h : d.direct = some a) : d.continuize = pure a

The lemma behind the Simulation Theorem says that a derivation the direct grammar interprets denotes the unit at its direct meaning.

theorem Barker2002.Deriv.eval_eq_of_direct {ι : Type} {d : Deriv ι Prop} {p : Prop} (h : d.direct = some p) : d.eval = p

The Simulation Theorem says that at the trivial continuation the continuized grammar computes the direct meaning.

@[simp]

theorem Barker2002.Deriv.eval_island {ι : Type} (d : Deriv ι Prop) : d.island.eval = d.eval

Closing a clause off as an island leaves its own meaning alone.

theorem Barker2002.Deriv.continuize_binary_of_direct_left {ι α β γ : Type} (M : α → β → γ) (p : Priority) {d₁ : Deriv ι α} {a : α} (h : d₁.direct = some a) (d₂ : Deriv ι β) : (binary M p d₁ d₂).continuize = M a <$> d₂.continuize

Priority is idle next to a left daughter that the direct grammar interprets.

theorem Barker2002.Deriv.continuize_binary_of_direct_right {ι α β γ : Type} (M : α → β → γ) (p : Priority) (d₁ : Deriv ι α) {d₂ : Deriv ι β} {b : β} (h : d₂.direct = some b) : (binary M p d₁ d₂).continuize = (fun (x : α) => M x b) <$> d₁.continuize

Priority is idle next to a right daughter that the direct grammar interprets.

Integrity

inductive Barker2002.Deriv.Constituent {ι α β : Type} : Deriv ι α → Deriv ι β → Prop

Constituent d' d says that d' is a constituent of d that no island separates from it.

• refl {ι α : Type} (d : Deriv ι α) : d.Constituent d
• unary {ι α β γ : Type} {d' : Deriv ι α} {d : Deriv ι β} (M : β → γ) : d'.Constituent d → d'.Constituent (Deriv.unary M d)
• binaryLeft {ι α β γ δ : Type} {d' : Deriv ι α} {d₁ : Deriv ι β} (M : β → γ → δ) (p : Priority) (d₂ : Deriv ι γ) : d'.Constituent d₁ → d'.Constituent (binary M p d₁ d₂)
• binaryRight {ι α β γ δ : Type} {d' : Deriv ι α} {d₂ : Deriv ι γ} (M : β → γ → δ) (p : Priority) (d₁ : Deriv ι β) : d'.Constituent d₂ → d'.Constituent (binary M p d₁ d₂)
• bind {ι α β γ : Type} {d' : Deriv ι α} {d : Deriv ι β} (i : ι) (q : β → Cont Prop γ) : d'.Constituent d → d'.Constituent (Deriv.bind i q d)
• coordLeft {ι α β : Type} {d' : Deriv ι α} {d₁ : Deriv ι β} (d₂ : Deriv ι β) : d'.Constituent d₁ → d'.Constituent (d₁.coord d₂)
• coordRight {ι α β : Type} {d' : Deriv ι α} {d₂ : Deriv ι β} (d₁ : Deriv ι β) : d'.Constituent d₂ → d'.Constituent (d₁.coord d₂)

theorem Barker2002.Deriv.Constituent.scopeOrder_isInfix {ι α β : Type} {d' : Deriv ι α} {d : Deriv ι β} (h : d'.Constituent d) : d'.scopeOrder <:+: d.scopeOrder

Integrity says that the quantifiers of a constituent are contiguous in the scope order of the whole, so an outside quantifier scopes over all of them or under all of them.

theorem Barker2002.Deriv.Constituent.filter_scopeOrder_isInfix {ι α β : Type} {d' : Deriv ι α} {d : Deriv ι β} [DecidableEq ι] (h : d'.Constituent d) (hd : d.scopeOrder.Nodup) : List.filter (fun (x : ι) => decide (x ∈ d'.scopeOrder)) d.scopeOrder <:+: d.scopeOrder

Integrity is a test on a scope order in which no item occurs twice, since the items of a constituent are then an uninterrupted stretch of the order.

The grammar

def Barker2002.S {ι E : Type} (p : Priority) (np : Deriv ι E) (vp : Deriv ι (E → Prop)) : Deriv ι Prop

S → NP VP, VP(NP).

Equations

• Barker2002.S p np vp = Barker2002.Deriv.binary (fun (x : E) (P : E → Prop) => P x) p np vp

def Barker2002.VP {ι E : Type} (p : Priority) (vt : Deriv ι (E → E → Prop)) (obj : Deriv ι E) : Deriv ι (E → Prop)

VP → Vt NP, Vt(NP).

Equations

• Barker2002.VP p vt obj = Barker2002.Deriv.binary (fun (R : E → E → Prop) (x : E) => R x) p vt obj

def Barker2002.VS {ι E : Type} (p : Priority) (vs : Deriv ι (Prop → E → Prop)) (s : Deriv ι Prop) : Deriv ι (E → Prop)

VP → Vs S, Vs(S).

Equations

• Barker2002.VS p vs s = Barker2002.Deriv.binary (fun (T : Prop → E → Prop) (q : Prop) => T q) p vs s

def Barker2002.NP {ι E : Type} (p : Priority) (det : Deriv ι (Reference.ChoiceFunction E)) (n : Deriv ι (E → Prop)) : Deriv ι E

NP → Det N, Det(N), with determiners denoting choice functions.

Equations

• Barker2002.NP p det n = Barker2002.Deriv.binary (fun (D : Reference.ChoiceFunction E) (P : E → Prop) => D P) p det n

def Barker2002.N {ι E : Type} (p : Priority) (nr : Deriv ι (E → E → Prop)) (pp : Deriv ι E) : Deriv ι (E → Prop)

N → Nr PPof, Nr(PP).

Equations

• Barker2002.N p nr pp = Barker2002.Deriv.binary (fun (R : E → E → Prop) (x : E) => R x) p nr pp

def Barker2002.PPof {ι E : Type} (np : Deriv ι E) : Deriv ι E

PPof → of NP, with a transparent preposition.

Equations

• Barker2002.PPof np = Barker2002.Deriv.unary id np

def Barker2002.everyone {E : Type} : Deriv String E

everyone is a universal over its continuation.

Equations

• Barker2002.everyone = Barker2002.Deriv.quant "everyone" fun (k : E → Id Prop) => ∀ (x : E), k x

def Barker2002.someone {E : Type} : Deriv String E

someone is an existential over its continuation.

Equations

• Barker2002.someone = Barker2002.Deriv.quant "someone" fun (k : E → Id Prop) => ∃ (x : E), k x

def Barker2002.NPgq {E : Type} (w : String) (Q : Quantifier.GQ E) (n : Deriv String (E → Prop)) : Deriv String E

The expository NP → Det N applies a generalized-quantifier determiner to the continuized nominal, so the determiner scopes under whatever the nominal contains.

Equations

• Barker2002.NPgq w Q n = Barker2002.Deriv.bind w (fun (P : E → Prop) => Q P) n

def Barker2002.every {E : Type} : Deriv String (Reference.ChoiceFunction E)

every quantifies universally over choice functions.

Equations

• Barker2002.every = Barker2002.Deriv.quant "every" fun (D : Reference.ChoiceFunction E → Id Prop) => ∀ (f : Reference.ChoiceFunction E), D f

def Barker2002.a {E : Type} : Deriv String (Reference.ChoiceFunction E)

a quantifies existentially over choice functions.

Equations

• Barker2002.a = Barker2002.Deriv.quant "a" fun (D : Reference.ChoiceFunction E → Id Prop) => ∃ (f : Reference.ChoiceFunction E), D f

Scope displacement and scope ambiguity

theorem Barker2002.john_left {ι E : Type} (j : E) (left' : E → Prop) (p : Priority) : (S p (Deriv.lex j) (Deriv.lex left')).eval = left' j

theorem Barker2002.everyone_left {E : Type} (left' : E → Prop) (p : Priority) : (S p everyone (Deriv.lex left')).eval = ∀ (x : E), left' x

theorem Barker2002.john_saw_NPgq {E : Type} (j : E) (man' : E → Prop) (saw' : E → E → Prop) (w : String) (Q : Quantifier.GQ E) (p p' : Priority) : (S p (Deriv.lex j) (VP p' (Deriv.lex saw') (NPgq w Q (Deriv.lex man')))).eval = Q man' fun (x : E) => saw' x j

A quantifier in object position takes scope over the clause, whatever determiner it has, as in John saw every man and John saw most men.

theorem Barker2002.every_man_saw_a_woman_inverse {E : Type} (man' woman' : E → Prop) (saw' : E → E → Prop) (p : Priority) : (S Priority.right (NPgq "every" Quantifier.GQ.every (Deriv.lex man')) (VP p (Deriv.lex saw') (NPgq "a" Quantifier.GQ.some (Deriv.lex woman')))).eval = ∃ (y : E), woman' y ∧ ∀ (x : E), man' x → saw' y x

Every man saw a woman with VP priority has the inverse reading.

theorem Barker2002.every_man_saw_a_woman_surface {E : Type} (man' woman' : E → Prop) (saw' : E → E → Prop) (p : Priority) : (S Priority.left (NPgq "every" Quantifier.GQ.every (Deriv.lex man')) (VP p (Deriv.lex saw') (NPgq "a" Quantifier.GQ.some (Deriv.lex woman')))).eval = ∀ (x : E), man' x → ∃ (y : E), woman' y ∧ saw' y x

With subject priority it has the surface reading.

theorem Barker2002.a_man_thought_everyone_saw_mary {E : Type} (m : E) (man' : E → Prop) (saw' : E → E → Prop) (thought' : Prop → E → Prop) (p₁ p₂ p₃ p₄ : Priority) : (S p₁ (NPgq "a" Quantifier.GQ.some (Deriv.lex man')) (VS p₂ (Deriv.lex thought') (S p₃ everyone (VP p₄ (Deriv.lex saw') (Deriv.lex m))).island)).eval = ∃ (y : E), man' y ∧ thought' (∀ (x : E), saw' m x) y

In a man thought everyone saw Mary the island traps everyone under every priority.

theorem Barker2002.someone_saw_the_friend_of_the_friend_of_everyone {E : Type} (saw' friendOf : E → E → Prop) (the : Reference.ChoiceFunction E) (p : Priority) : (S p someone (VP Priority.left (Deriv.lex saw') (NP Priority.left (Deriv.lex the) (N Priority.left (Deriv.lex friendOf) (PPof (NP Priority.left (Deriv.lex the) (N Priority.left (Deriv.lex friendOf) (PPof everyone)))))))).eval = match p with | Priority.left => ∃ (x : E), ∀ (y : E), saw' (the (friendOf (the (friendOf y)))) x | Priority.right => ∀ (y : E), ∃ (x : E), saw' (the (friendOf (the (friendOf y)))) x

In someone saw the friend of the friend of everyone the embedded quantifier takes scope from any depth, and the priority at S decides between the two scopings.

Choice-function determiners

theorem Barker2002.john_saw_every_man {E : Type} (j : E) (man' : E → Prop) (saw' : E → E → Prop) (p₁ p₂ p₃ : Priority) : (S p₁ (Deriv.lex j) (VP p₂ (Deriv.lex saw') (NP p₃ every (Deriv.lex man')))).eval = ∀ (f : Reference.ChoiceFunction E), saw' (f man') j

John saw every man says that for every way of choosing a man, John saw him.

theorem Barker2002.john_saw_every_man_iff {E : Type} (j : E) (man' : E → Prop) (saw' : E → E → Prop) (hman : ∃ (x : E), man' x) (p₁ p₂ p₃ : Priority) : (S p₁ (Deriv.lex j) (VP p₂ (Deriv.lex saw') (NP p₃ every (Deriv.lex man')))).eval ↔ Quantifier.GQ.every man' fun (x : E) => saw' x j

When there are men, the choice-function every and the generalized-quantifier every give John saw every man the same truth conditions.

theorem Barker2002.john_saw_every_man_iff_of_not_exists {E : Type} (j : E) (man' : E → Prop) (saw' : E → E → Prop) (hman : ¬∃ (x : E), man' x) (p₁ p₂ p₃ : Priority) : (S p₁ (Deriv.lex j) (VP p₂ (Deriv.lex saw') (NP p₃ every (Deriv.lex man')))).eval ↔ ∀ (x : E), saw' x j

When there are no men they come apart, since the choice-function sentence says that John saw everyone and the generalized-quantifier sentence is vacuously true.

The scopings of someone saw a friend of everyone

def Barker2002.someoneSawAFriendOfEveryone {E : Type} (saw' friendOf : E → E → Prop) (pS pVP pNP pN : Priority) : Deriv String Prop

The derivation, with a priority at the S, VP, NP and N nodes.

Equations

• One or more equations did not get rendered due to their size.

theorem Barker2002.scopeOrder_someoneSawAFriendOfEveryone {E : Type} (saw' friendOf : E → E → Prop) (pS pVP pNP pN : Priority) : (someoneSawAFriendOfEveryone saw' friendOf pS pVP pNP pN).scopeOrder = match pS, pNP with | Priority.left, Priority.left => ["someone", "a", "everyone"] | Priority.left, Priority.right => ["someone", "everyone", "a"] | Priority.right, Priority.left => ["a", "everyone", "someone"] | Priority.right, Priority.right => ["everyone", "a", "someone"]

The priorities at S and NP fix the scope order.

theorem Barker2002.eval_someoneSawAFriendOfEveryone {E : Type} (saw' friendOf : E → E → Prop) (pS pVP pNP pN : Priority) : (someoneSawAFriendOfEveryone saw' friendOf pS pVP pNP pN).eval = match pS, pNP with | Priority.left, Priority.left => ∃ (y : E) (f : Reference.ChoiceFunction E), ∀ (x : E), saw' (f (friendOf x)) y | Priority.left, Priority.right => ∃ (y : E), ∀ (x : E), ∃ (f : Reference.ChoiceFunction E), saw' (f (friendOf x)) y | Priority.right, Priority.left => ∃ (f : Reference.ChoiceFunction E), ∀ (x : E), ∃ (y : E), saw' (f (friendOf x)) y | Priority.right, Priority.right => ∀ (x : E), ∃ (f : Reference.ChoiceFunction E) (y : E), saw' (f (friendOf x)) y

The truth conditions follow the scope order.

theorem Barker2002.scopeOrder_object {E : Type} (friendOf : E → E → Prop) (pNP pN : Priority) : (NP pNP a (N pN (Deriv.lex friendOf) (PPof everyone))).scopeOrder = match pNP with | Priority.left => ["a", "everyone"] | Priority.right => ["everyone", "a"]

The priority at NP orders the object's two quantifiers.

theorem Barker2002.constituent_object {E : Type} (saw' friendOf : E → E → Prop) (pS pVP pNP pN : Priority) : (NP pNP a (N pN (Deriv.lex friendOf) (PPof everyone))).Constituent (someoneSawAFriendOfEveryone saw' friendOf pS pVP pNP pN)

The object noun phrase is a constituent of the sentence.

theorem Barker2002.no_split_scoping {E : Type} (saw' friendOf : E → E → Prop) (pS pVP pNP pN : Priority) : (someoneSawAFriendOfEveryone saw' friendOf pS pVP pNP pN).scopeOrder ≠ ["everyone", "someone", "a"] ∧ (someoneSawAFriendOfEveryone saw' friendOf pS pVP pNP pN).scopeOrder ≠ ["a", "someone", "everyone"]

Integrity excludes the orders that split the object's quantifiers around the subject.

theorem Barker2002.a_everyone_iff_everyone_a {E : Type} (saw' friendOf : E → E → Prop) [Nonempty E] (pS pVP pN pVP' pN' : Priority) : (someoneSawAFriendOfEveryone saw' friendOf pS pVP Priority.left pN).eval ↔ (someoneSawAFriendOfEveryone saw' friendOf pS pVP' Priority.right pN').eval

The order of a and everyone makes no difference to the truth conditions, because the restrictor of a contains the variable that everyone binds.

Generalized coordination

theorem Barker2002.coord_VP_subject_priority {ι E : Type} (np : Deriv ι E) (P Q : E → Prop) : (S Priority.left np ((Deriv.lex P).coord (Deriv.lex Q))).eval = (S Priority.left np (Deriv.lex (P ⊓ Q))).eval

With subject priority, coordinated verb phrases denote their pointwise conjunction, as in Partee and Rooth's generalized conjunction.

theorem Barker2002.coord_VP_priority {ι E : Type} (np : Deriv ι E) (P Q : E → Prop) : (S Priority.right np ((Deriv.lex P).coord (Deriv.lex Q))).eval = ((S Priority.right np (Deriv.lex P)).eval ∧ (S Priority.right np (Deriv.lex Q)).eval)

With VP priority the conjunction distributes over the subject.

theorem Barker2002.john_and_mary_left {ι E : Type} (j m : E) (left' : E → Prop) (p : Priority) : (S p ((Deriv.lex j).coord (Deriv.lex m)) (Deriv.lex left')).eval = (left' j ∧ left' m)

Coordinated noun phrases need no conjoinable type, as in John and Mary left.

The paper's examples

def Barker2002.wordsOn (c : Char) (s : String) : List String

The words of a string, split at a separator.

Equations

• One or more equations did not get rendered due to their size.

theorem Barker2002.rows_scopings (e : Datum) : e ∈ Examples.all → e.feature? "derivation" = some "someone saw a friend of everyone" → ∀ r ∈ e.readings, r.2 = Judgment.acceptable ↔ ∃ (pS : Priority) (pVP : Priority) (pNP : Priority) (pN : Priority), (someoneSawAFriendOfEveryone (fun (x x_1 : Unit) => True) (fun (x x_1 : Unit) => True) pS pVP pNP pN).scopeOrder = wordsOn '>' r.1

The readings the paper lists for someone saw a friend of everyone are exactly the scope orders some prioritization of its derivation induces.

theorem Barker2002.rows_integrity (e : Datum) : e ∈ Examples.all → ∀ c ∈ e.feature? "constituent", ∀ r ∈ e.readings, r.2 = Judgment.acceptable ↔ List.filter (fun (x : String) => decide (x ∈ wordsOn ' ' c)) (wordsOn '>' r.1) <:+: wordsOn '>' r.1

Wherever the paper names a constituent holding two of a sentence's quantifiers, the readings it accepts are those that keep the two together, as Deriv.Constituent.filter_scopeOrder_isInfix requires.