Barker (2002): Continuations and the Nature of Quantification

Formalizes the continuized grammar of [Bar02a]: quantificational NPs denote functions on their own continuations, so continuizing an ordinary grammar derives generalized quantifiers, in-situ scope displacement, and scope ambiguity, with no movement, storage, or type-shifting. The file states the Continuation Schema at arity 2, the fragment with its worked derivations, the scope-island rule with clause boundedness, generalized coordination, and the Simulation Theorem, following the paper's own proof. Barker's transitive verbs take the object first: saw m j is "John saw Mary".

The fragment's determiners quantify over choice functions, as in the paper's appendix; the generalized-quantifier pair the paper introduces for exposition is kept for the derivations whose printed formulas need it. The the friend of chains are not formalized.

The grammar

def Barker2002.sRuleVP {E : Type} (np : Cont Prop E) (vp : Cont Prop (E → Prop)) : Cont Prop Prop

The S rule with priority to the VP.

Equations

• Barker2002.sRuleVP np vp = vp <*> np

def Barker2002.sRuleNP {E : Type} (np : Cont Prop E) (vp : Cont Prop (E → Prop)) : Cont Prop Prop

The S rule with priority to the subject.

Equations

• Barker2002.sRuleNP np vp = (fun (x : E) (P : E → Prop) => P x) <$> np <*> vp

def Barker2002.vpRule {E : Type} (vt : Cont Prop (E → E → Prop)) (obj : Cont Prop E) : Cont Prop (E → Prop)

The VP rule, verb priority.

Equations

• Barker2002.vpRule vt obj = vt <*> obj

def Barker2002.everyone {E : Type} : Quantification.Quantifier E

everyone: a universal over the continuation.

Equations

• Barker2002.everyone k = ∀ (x : E), k x

def Barker2002.someone {E : Type} : Quantification.Quantifier E

someone: an existential over the continuation.

Equations

• Barker2002.someone k = ∃ (x : E), k x

def Barker2002.everyCF {E : Type} : Cont Prop ((E → Prop) → E)

every quantifies over choice functions; Barker leaves the restriction to proper choice functions to the choice-function literature, and so do we.

Equations

• Barker2002.everyCF D = ∀ (f : (E → Prop) → E), D f

def Barker2002.aCF {E : Type} : Cont Prop ((E → Prop) → E)

a as an existential over choice functions.

Equations

• Barker2002.aCF D = ∃ (f : (E → Prop) → E), D f

def Barker2002.npRuleDet {E : Type} (det : Cont Prop ((E → Prop) → E)) (n : Cont Prop (E → Prop)) : Cont Prop E

The NP rule, determiner priority.

Equations

• Barker2002.npRuleDet det n = det <*> n

def Barker2002.npRuleN {E : Type} (det : Cont Prop ((E → Prop) → E)) (n : Cont Prop (E → Prop)) : Cont Prop E

The NP rule, nominal priority.

Equations

• Barker2002.npRuleN det n = (fun (P : E → Prop) (D : (E → Prop) → E) => D P) <$> n <*> det

def Barker2002.everyGQ {E : Type} (n : Cont Prop (E → Prop)) : Quantification.Quantifier E

The paper's expository every, typed as a generalized quantifier.

Equations

• Barker2002.everyGQ n k = n fun (P : E → Prop) => ∀ (x : E), P x → k x

def Barker2002.aGQ {E : Type} (n : Cont Prop (E → Prop)) : Quantification.Quantifier E

The paper's expository a.

Equations

• Barker2002.aGQ n k = n fun (P : E → Prop) => ∃ (x : E), P x ∧ k x

The worked derivations

theorem Barker2002.john_left {E : Type} (j : E) (left' : E → Prop) : ContT.eval (sRuleVP (Quantification.individual j) (pure left')) = left' j

John left.

theorem Barker2002.everyone_left {E : Type} (left' : E → Prop) : ContT.eval (sRuleVP everyone (pure left')) = ∀ (x : E), left' x

Everyone left.

theorem Barker2002.john_saw_everyone {E : Type} (j : E) (saw' : E → E → Prop) : ContT.eval (sRuleVP (Quantification.individual j) (vpRule (pure saw') everyone)) = ∀ (x : E), saw' x j

John saw everyone, in situ.

theorem Barker2002.every_man_saw_a_woman_inverse {E : Type} (man' woman' : E → Prop) (saw' : E → E → Prop) : ContT.eval (sRuleVP (everyGQ (pure man')) (vpRule (pure saw') (aGQ (pure woman')))) = ∃ (y : E), woman' y ∧ ∀ (x : E), man' x → saw' y x

Every man saw a woman, VP priority: the inverse reading.

theorem Barker2002.every_man_saw_a_woman_surface {E : Type} (man' woman' : E → Prop) (saw' : E → E → Prop) : ContT.eval (sRuleNP (everyGQ (pure man')) (vpRule (pure saw') (aGQ (pure woman')))) = ∀ (x : E), man' x → ∃ (y : E), woman' y ∧ saw' y x

Every man saw a woman, subject priority: the surface reading.

theorem Barker2002.john_saw_every_man {E : Type} (j : E) (man' : E → Prop) (saw' : E → E → Prop) : ContT.eval (sRuleVP (Quantification.individual j) (vpRule (pure saw') (npRuleDet everyCF (pure man')))) = ∀ (f : (E → Prop) → E), saw' (f man') j

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

theorem Barker2002.someone_saw_a_friend_of_everyone_yfx {E : Type} (saw' friendOf : E → E → Prop) : ContT.eval (sRuleNP someone (vpRule (pure saw') (npRuleDet aCF (pure friendOf <*> everyone)))) = ∃ (y : E) (f : (E → Prop) → E), ∀ (x : E), saw' (f (friendOf x)) y

Someone saw a friend of everyone: subject wide, determiner over nominal.

theorem Barker2002.someone_saw_a_friend_of_everyone_yxf {E : Type} (saw' friendOf : E → E → Prop) : ContT.eval (sRuleNP someone (vpRule (pure saw') (npRuleN aCF (pure friendOf <*> everyone)))) = ∃ (y : E), ∀ (x : E), ∃ (f : (E → Prop) → E), saw' (f (friendOf x)) y

Subject wide, nominal over determiner.

theorem Barker2002.someone_saw_a_friend_of_everyone_fxy {E : Type} (saw' friendOf : E → E → Prop) : ContT.eval (sRuleVP someone (vpRule (pure saw') (npRuleDet aCF (pure friendOf <*> everyone)))) = ∃ (f : (E → Prop) → E), ∀ (x : E), ∃ (y : E), saw' (f (friendOf x)) y

Object wide, determiner over nominal.

theorem Barker2002.someone_saw_a_friend_of_everyone_xfy {E : Type} (saw' friendOf : E → E → Prop) : ContT.eval (sRuleVP someone (vpRule (pure saw') (npRuleN aCF (pure friendOf <*> everyone)))) = ∀ (x : E), ∃ (f : (E → Prop) → E) (y : E), saw' (f (friendOf x)) y

Object wide, nominal over determiner.

Bounding scope displacement

def Barker2002.sRuleIsland {E : Type} (np : Cont Prop E) (vp : Cont Prop (E → Prop)) : Cont Prop Prop

The island-adjusted S rule: evaluate the clause, then re-lift.

Equations

• Barker2002.sRuleIsland np vp = ContT.reset (Barker2002.sRuleVP np vp)

def Barker2002.vsRule {E : Type} (vs : Cont Prop (Prop → E → Prop)) (s : Cont Prop Prop) : Cont Prop (E → Prop)

The clausal-complement rule, verb priority.

Equations

• Barker2002.vsRule vs s = vs <*> s

theorem Barker2002.a_man_thought_everyone_saw_mary {E : Type} (m : E) (man' : E → Prop) (saw' : E → E → Prop) (thought' : Prop → E → Prop) : ContT.eval (sRuleVP (aGQ (pure man')) (vsRule (pure thought') (sRuleIsland everyone (vpRule (pure saw') (Quantification.individual m))))) = ∃ (y : E), man' y ∧ thought' (∀ (x : E), saw' m x) y

A man thought everyone saw Mary: everyone is trapped in the complement.

theorem Barker2002.sRule_priority_inert {E : Type} (np : Cont Prop E) (P : E → Prop) : sRuleNP np (pure P) = sRuleVP np (pure P)

A unit VP makes the matrix priority choice inert: "all scopings are logically equivalent".

Generalized coordination

def Barker2002.coord {α : Type} (l r : Cont Prop α) : Cont Prop α

Coordination at any category: the continuation distributes across the conjuncts.

Equations

• Barker2002.coord l r k = (l k ∧ r k)

theorem Barker2002.john_left_and_slept {E : Type} (j : E) (left' slept' : E → Prop) : ContT.eval (sRuleVP (Quantification.individual j) (coord (pure left') (pure slept'))) = (left' j ∧ slept' j)

John left and slept.

theorem Barker2002.john_and_mary_left {E : Type} (j m : E) (left' : E → Prop) : ContT.eval (sRuleVP (coord (Quantification.individual j) (Quantification.individual m)) (pure left')) = (left' j ∧ left' m)

John and Mary left.

The Simulation Theorem

theorem Barker2002.simulating_iff {α : Type} {c : Cont Prop α} {a : α} : (∀ (g : α → Id Prop), c g = g a) ↔ c = pure a

Simulating in the paper's sense is being a unit.

theorem Barker2002.simulation_orders_agree {α β γ : Type} (M : α → β → γ) (a : α) (c : Cont Prop β) : M <$> pure a <*> c = flip M <$> c <*> pure a

"The result is the same, in the absence of quantification": a unit daughter makes the priority choice inert.

theorem Barker2002.simulation {α β : Type} (M : α → β → Prop) (m₁ : α) (m₂ : β) : (M <$> pure m₁ <*> pure m₂).eval = M m₁ m₂

A schema-derived sentence evaluates at the trivial continuation to its direct meaning.