Charlow 2014: on the semantics of exceptional scope

Charlow treats exceptional scope as side effects taking scope after evaluation. Dekker's stack-based dynamic semantics becomes a monad, StateT (Stack E) Set, output stacks of discourse referents plus nondeterminism, the monad transformer of Liang, Hudak and Jones over Set, and scope-taking becomes the continuation transformer over it, as in Wadler, with Lift identified with monadLift and Lower with ContT.eval. A scope island is a constituent that must be evaluated: Danvy and Filinski's ContT.reset discharges quantifiers but leaves nondeterministic and state-changing effects intact, so indefinites, disjunctions (after Rooth and Partee), the drefs of proper names and the maximal drefs of dynamic quantifiers all scope out of islands and feed binding, obeying Brasoveanu and Farkas's Binder Roof Constraint, while every and no do not escape. The paper's examples are rows in Data/Examples/Charlow2014.json, cited from the theorems deriving them.

The grammar is Shan's monadic application: combine sequences its daughters left to right in any monad, and its per-monad unfoldings are the thesis's application rules, functional, state-sensitive, nondeterministic (Kratzer and Shimoyama's rule), and their combinations. The Identity, Reader, Set, Reader.Set, State and State.Set monads are Lean's Id, ReaderT, Set, ReaderT _ Set, StateT _ Id and StateT _ Set; the Focus monad, Shan's pointed powerset for Rooth's alternatives, is the library's WithAlternatives. Continuation results are Prop-valued, so "some output is true" is holds. The stack is List E.

Main definitions

• combine: monadic application, the thesis's overloaded rule of use
• Stack, StateSet, indef, pro, dref, holds, neg, cond, det, every, no: the State.Set fragment
• Tower, liftValue, bindShift, everyDP, noDP, eval₂: scope-takers over it
• distr, or, dynGQ: distributivity, program disjunction, dynamic generalized quantifiers
• Focus.fmark, Focus.only, Focus.also: F-marking and the focus particles over WithAlternatives, only and the additive of Focus.Particles on the identity scale
• ReaderSet and its fragment: the Reader.Set variant

Main results

• combine_bind: Rebracket: side effects propagate in linear order whatever the bracketing
• dref_bind, bind_pro: dref introduction and binding in State.Set
• neg_dref_indef, neg_pro, cond_dref_indef, every_dref_indef: negation and the operators built on it discharge nondeterminism and drefs but not pronouns
• eval_combine_monadLift: scopal application subsumes monadic application
• reset_combine_monadLift: side effects survive evaluation, in any monad
• reset_every, reset_indef_every, reset_every_indef, reset_every_pro: what survives evaluation: indefinites and pronouns, not quantifiers, and not an indefinite an inverse-scoped quantifier discharged
• exceptional_neg, exceptional_cond, exceptional_feeds_binding, brc_derivation — exceptional scope over negation and conditionals, feeding anaphora, and the Binder Roof Constraint
• monadLift_layered, indef_visits_indef_layered: selective exceptional scope via layering
• or_over_every, or_or_names: disjunction over a universal whose indefinites stay under it, and higher-order disjunctive programs
• name_dref_inverse, dynGQ_neg: name drefs and maximal drefs escape islands
• Focus.only_iff, Focus.also_iff: the particles are those of Def. 5.10
• Focus.only_focus_layered, Focus.also_only_focus_layered: selective association with focus
• island_cond_every: a universal does not scope out of a Reset antecedent
• ReaderSet.no_exceptional_binding, ReaderSet.run_monadLift: Reader.Set continuations see the input stack only, so the variant hosts exceptional scope but not exceptional binding
• cf_exceptional_cond, cf_no_candidate_iff, cf_same_restrictor_iff, cf_layered_iff, cf_disjunction_iff: the choice-functional rival (section 4.7.1) matches exceptional scope but closes choice functions over bound-into restrictors into unattested readings

Implementation notes

• A pronoun on the empty stack has no value in the thesis; here pro has no output there, so failure is the empty set. A negation over an unbound pronoun is then true where the thesis leaves it undefined, and the thesis's Facts 3.3 and 4.7 (neg_pro, reset_every_pro) carry a nonempty-stack hypothesis.
• The thesis excludes the empty set from the pluralities and treats an empty reference set as a presupposition failure; Set A admits it, and dynGQ pushes it as a dref. Quantifiers range over atoms A while the stack holds pluralities Set A, where the thesis identifies an atom with its singleton.
• combine parameterizes the thesis's overloaded application by the value-level mode of combination; it is f <$> m <*> n (combine_eq_seq).
• The un-indexed pronoun retrieving the last dref is the thesis's own simplification, "an extremely crude measure of topicality".
• The choice-function theorems assume that distinct values of the bound variable give distinct restrictors, which the thesis states for (4.37) and leaves implicit for (4.35) and (4.38).

TODO

• Relative-clause islands (Examples.ex4_2a), the second Binder Roof datum with layered DPs (Examples.ex4_6), donkey disjunction (Examples.ex4_25b), the restrictor drefs of dynamic generalized quantifiers (Examples.ex5_22), and selective association with focus across islands.
• Determiners composed as tripartite towers need an indexed continuation transformer, and the cross-categorial drefs of sloppy readings need a polymorphic Bind and pronoun over an untyped stack.
• The thesis's grammar enforces evaluation at islands (a scope island is the sister of fin); here ContT.reset is inserted by hand.
• The comparison with Independence-Friendly Logic (section 4.7.2).

References

• [Cha14b]
• [Dek94]
• [LHJ95]
• [Wad94]
• [DF90]
• [RP82]
• [Roo85]
• [BF11]
• [Sch01]
• [Geu00]
• [Sha02a]
• [Sha04]
• [KS17]
• [BS14]

Monadic application and Rebracket

def Charlow2014.combine {M : Type u → Type u} [Monad M] {α β γ : Type u} (f : α → β → γ) (m : M α) (n : M β) : M γ

combine f m n is monadic application over a value-level combination f, which runs m, then n, and combines the values. Forward application is combine (· ·) and backward combine (fun x f ↦ f x), the thesis's overloaded A.

Equations

• Charlow2014.combine f m n = do let x ← m let y ← n pure (f x y)

theorem Charlow2014.combine_eq_seq {M : Type u → Type u} [Monad M] [LawfulMonad M] {α β γ : Type u} (f : α → β → γ) (m : M α) (n : M β) : combine f m n = f <$> m <*> n

theorem Charlow2014.combine_bind {M : Type u → Type u} [Monad M] [LawfulMonad M] {α β γ δ : Type u} (f : α → β → γ) (m : M α) (n : M β) (k : γ → M δ) : combine f m n >>= k = do let x ← m let y ← n k (f x y)

Sequencing a combined node is sequencing its daughters in linear order, whatever the bracketing, which is Rebracket.

theorem Charlow2014.combine_pure_left {M : Type u → Type u} [Monad M] [LawfulMonad M] {α β γ : Type u} (f : α → β → γ) (a : α) (n : M β) : combine f (pure a) n = f a <$> n

theorem Charlow2014.combine_pure_right {M : Type u → Type u} [Monad M] [LawfulMonad M] {α β γ : Type u} (f : α → β → γ) (m : M α) (b : β) : combine f m (pure b) = (fun (x : α) => f x b) <$> m

Truth values as propositions

theorem Charlow2014.forall_iff_imp {q : Prop} {P : Prop → Prop} : (∀ (p : Prop), (p ↔ q) → P p) ↔ P q

Truth values are Props, so a value pinned by a biconditional substitutes away like one pinned by an equation.

theorem Charlow2014.exists_iff_and {q : Prop} {P : Prop → Prop} : (∃ (p : Prop), (p ↔ q) ∧ P p) ↔ P q

The monads of Chapter 2

Application in each monad (Facts 2.2–2.5, 2.8, 2.11): functional application, state-sensitive (SSA), nondeterministic (NA), state-sensitive nondeterministic (SSNA, the rule of [KS17]), stateful, and stateful nondeterministic application.

theorem Charlow2014.combine_id {σ α β : Type} (f : α → β → σ) (m : Id α) (n : Id β) : combine f m n = f m n

theorem Charlow2014.combine_readerT {σ α β : Type} (f : α → β → σ) (m : ReaderT σ Id α) (n : ReaderT σ Id β) : combine f m n = fun (s : σ) => f (m s) (n s)

theorem Charlow2014.combine_set {σ α β : Type} (f : α → β → σ) (m : Set α) (n : Set β) : combine f m n = {c : σ | ∃ x ∈ m, ∃ y ∈ n, c = f x y}

theorem Charlow2014.combine_readerT_set {σ α β : Type} (f : α → β → σ) (m : ReaderT σ Set α) (n : ReaderT σ Set β) : combine f m n = fun (s : σ) => {c : σ | ∃ x ∈ m s, ∃ y ∈ n s, c = f x y}

theorem Charlow2014.combine_stateT {σ α β : Type} (f : α → β → σ) (m : StateT σ Id α) (n : StateT σ Id β) : combine f m n = fun (s : σ) => (f (m s).1 (n (m s).2).1, (n (m s).2).2)

theorem Charlow2014.combine_stateT_set {σ α β : Type} (f : α → β → σ) (m : StateT σ Set α) (n : StateT σ Set β) : combine f m n = fun (s : σ) => {c : σ × σ | ∃ x ∈ m s, ∃ y ∈ n x.2, c = (f x.1 y.1, y.2)}

Stacks and the State.Set monad

Discourse referents live on a stack; pronouns retrieve the most recent one (List.getLast?). A sentence denotes a StateSet E Prop: from an input stack to a set of value–output-stack pairs.

@[reducible, inline]

abbrev Charlow2014.Stack (E : Type) : Type

The reference stack lists drefs in order of introduction.

Equations

• Charlow2014.Stack E = List E

@[reducible, inline]

abbrev Charlow2014.StateSet (E α : Type) : Type

The State.Set monad is StateT over the Set monad.

Equations

• Charlow2014.StateSet E = StateT (Charlow2014.Stack E) Set

def Charlow2014.indef {E : Type} (P : E → Prop) : StateSet E E

indef P is an indefinite, a nondeterministic individual satisfying P, with the stack unchanged.

Equations

• Charlow2014.indef P s = {q : E × Charlow2014.Stack E | P q.1 ∧ q.2 = s}

def Charlow2014.pro {E : Type} : StateSet E E

pro is a pronoun, the topical (most recent) dref, with the stack unchanged.

Equations

• Charlow2014.pro s = {q : E × Charlow2014.Stack E | List.getLast? s = some q.1 ∧ q.2 = s}

def Charlow2014.dref {E : Type} (m : StateSet E E) : StateSet E E

dref m introduces a dref, running m and pushing its value onto the stack.

Equations

• Charlow2014.dref m = do let a ← m fun (s : Charlow2014.Stack E) => {(a, s ++ [a])}

def Charlow2014.holds {E : Type} (m : StateSet E Prop) (s : Stack E) : Prop

A dynamic proposition holds at s when some output carries a true value.

Equations

• Charlow2014.holds m s = ∃ q ∈ m s, q.1

def Charlow2014.neg {E : Type} (m : StateSet E Prop) : StateSet E Prop

neg m is dynamic negation, a test on the input stack that returns it unchanged.

Equations

• Charlow2014.neg m s = {(¬Charlow2014.holds m s, s)}

def Charlow2014.cond {E : Type} (m n : StateSet E Prop) : StateSet E Prop

The conditional, from negation via p → q ↔ ¬(p ∧ ¬q).

Equations

• Charlow2014.cond m n = Charlow2014.neg do let p ← m let q ← Charlow2014.neg n pure (p ∧ q)

def Charlow2014.det {E : Type} (c : E → StateSet E Prop) : StateSet E E

det c is the indefinite determiner, the individuals whose restrictor holds, with the restrictor's output stacks.

Equations

• Charlow2014.det c s = {q : E × Charlow2014.Stack E | ∃ (p : Prop), (p, q.2) ∈ c q.1 s ∧ p}

def Charlow2014.every {E : Type} (c k : E → StateSet E Prop) : StateSet E Prop

every c k is the universal, a scope-taker over dynamic properties defined by ∀x. P x ⇒ Q x ↔ ¬∃x. P x ∧ ¬Q x.

Equations

• Charlow2014.every c k = Charlow2014.neg do let x ← Charlow2014.det c Charlow2014.neg (k x)

def Charlow2014.no {E : Type} (c k : E → StateSet E Prop) : StateSet E Prop

no c k is every without the inner negation.

Equations

• Charlow2014.no c k = Charlow2014.neg (Charlow2014.det c >>= k)

@[simp]

theorem Charlow2014.pure_apply {E α : Type} (a : α) (s : Stack E) : pure a s = {(a, s)}

@[simp]

theorem Charlow2014.mem_indef {E : Type} (P : E → Prop) (s : Stack E) (q : E × Stack E) : q ∈ indef P s ↔ P q.1 ∧ q.2 = s

@[simp]

theorem Charlow2014.mem_pro {E : Type} (s : Stack E) (q : E × Stack E) : q ∈ pro s ↔ List.getLast? s = some q.1 ∧ q.2 = s

@[simp]

theorem Charlow2014.mem_dref {E : Type} (m : StateSet E E) (s : Stack E) (q : E × Stack E) : q ∈ dref m s ↔ ∃ r ∈ m s, q = (r.1, r.2 ++ [r.1])

@[simp]

theorem Charlow2014.neg_apply {E : Type} (m : StateSet E Prop) (s : Stack E) : neg m s = {(¬holds m s, s)}

@[simp]

theorem Charlow2014.mem_det {E : Type} (c : E → StateSet E Prop) (s : Stack E) (q : E × Stack E) : q ∈ det c s ↔ ∃ (p : Prop), (p, q.2) ∈ c q.1 s ∧ p

@[simp]

theorem Charlow2014.holds_pure {E : Type} (p : Prop) (s : Stack E) : holds (pure p) s ↔ p

@[simp]

theorem Charlow2014.holds_singleton {E : Type} (p : Prop) (f : Stack E → Stack E) (s : Stack E) : holds (fun (s : Stack E) => {(p, f s)}) s ↔ p

@[simp]

theorem Charlow2014.holds_bind {E α : Type} (m : StateSet E α) (k : α → StateSet E Prop) (s : Stack E) : holds (m >>= k) s ↔ ∃ q ∈ m s, holds (k q.1) q.2

@[simp]

theorem Charlow2014.holds_map {E α : Type} (f : α → Prop) (m : StateSet E α) (s : Stack E) : holds (f <$> m) s ↔ ∃ q ∈ m s, f q.1

@[simp]

theorem Charlow2014.holds_neg {E : Type} (m : StateSet E Prop) (s : Stack E) : holds (neg m) s ↔ ¬holds m s

@[simp]

theorem Charlow2014.det_pure {E : Type} (P : E → Prop) : (det fun (x : E) => pure (P x)) = indef P

theorem Charlow2014.dref_bind {E α : Type} (m : StateSet E E) (π : E → StateSet E α) : dref m >>= π = do let a ← m fun (s : Stack E) => π a (s ++ [a])

Dref introduction simplifies away, since what follows sees the stack extended with the value (Fact 2.12).

theorem Charlow2014.bind_pro {E α : Type} (m : StateSet E E) (π : E → E → StateSet E α) : (do let ν ← dref m let u ← pro π ν u) = do let ν ← dref m π ν ν

A pronoun in the immediate scope of a dref-introducing program evaluates to that program's value, which is binding (Fact 2.13).

theorem Charlow2014.indef_met_name {E : Type} (man : E → Prop) (met : E → E → Prop) (p : E) : combine (fun (x : E) (f : E → Prop) => f x) (dref (indef man)) (combine (fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (pure met) (pure p)) = fun (s : List E) => {q : Prop × List E | ∃ (x : E), man x ∧ q = (met p x, s ++ [x])}

A man met Polly leaves a nondeterministic man on the output stack.

theorem Charlow2014.indef_left_pro_tired {E : Type} (man left tired : E → Prop) : combine (fun (x : Prop) (f : Prop → Prop) => f x) (combine (fun (x : E) (f : E → Prop) => f x) (dref (indef man)) (pure left)) (combine (fun (x1 : Prop → Prop → Prop) (x2 : Prop) => x1 x2) (pure fun (q p : Prop) => p ∧ q) (combine (fun (x : E) (f : E → Prop) => f x) pro (pure tired))) = do let x ← dref (indef man) pure (left x ∧ tired x)

A man left; he was tired — cross-sentential binding with static conjunction.

Dynamically closed operators

theorem Charlow2014.neg_dref_indef {E : Type} (ling left : E → Prop) : (neg do let x ← dref (indef ling) pure (left x)) = pure ¬∃ (x : E), ling x ∧ left x

In it's false that a linguist left negation discharges the indefinite's nondeterminism and dref (Fact 3.2).

theorem Charlow2014.neg_pro {E : Type} (m : E → StateSet E Prop) {s : Stack E} (h : s ≠ []) : neg (pro >>= m) s = (pro >>= fun (x : E) => neg (m x)) s

Negation is not closed for anaphoric sensitivity (Fact 3.3).

theorem Charlow2014.cond_dref_indef {E : Type} (P w r : E → Prop) : (cond (do let x ← dref (indef P) pure (w x)) do let y ← pro pure (r y)) = pure (∀ (x : E), P x → w x → r x)

In if someone walked, she ran the antecedent's indefinite binds into the consequent, and the conditional is closed (Fact 3.4).

theorem Charlow2014.every_dref_indef {E : Type} (ling hist : E → Prop) (met : E → E → Prop) : (every (fun (x : E) => pure (ling x)) fun (x : E) => do let y ← dref (indef hist) pure (met y x)) = pure (∀ (x : E), ling x → ∃ (y : E), hist y ∧ met y x)

Every linguist met a historian (Fact 3.5).

theorem Charlow2014.every_dref_pro {E : Type} (ling : E → Prop) (rubbed : E → E → Prop) (head : E → E) : (every (fun (x : E) => pure (ling x)) fun (x : E) => do let ν ← dref (pure x) let y ← pro pure (rubbed (head y) ν)) = pure (∀ (x : E), ling x → rubbed (head x) x)

In every linguist rubbed her head the pronoun is bound in scope by the dref of the quantified-over individual, which is then discarded (Fact 3.6).

Continuations over the State.Set monad

A tower ContT β (StateSet E) α returns an α in a computation of type StateSet E β. monadLift is monadic Lift (m ↑ = (m >>= ·)), ContT.eval Lower (application to pure), scopal application is combine in ContT.

@[reducible, inline]

abbrev Charlow2014.Tower (E β α : Type) : Type

A tower is a scope-taker over State.Set programs.

Equations

• Charlow2014.Tower E β α = ContT β (Charlow2014.StateSet E) α

theorem Charlow2014.combine_contT {ρ : Type} {M : Type → Type} [Monad M] {α β γ : Type} (f : α → β → γ) (m : ContT ρ M α) (n : ContT ρ M β) : combine f m n = fun (k : γ → M ρ) => m.run fun (x : α) => n.run fun (y : β) => k (f x y)

Scopal application is continuation-monadic application (Fact 3.7).

theorem Charlow2014.monadLift_id {ρ α : Type} (a : Id α) : monadLift a = fun (k : α → Id ρ) => k a

Lift into the continuation monad over Id is the Montague lift.

theorem Charlow2014.static_every {E : Type} {ling : E → Prop} (saw : E → E → Prop) (p : E) : (combine (fun (x : E) (f : E → Prop) => f x) (pure p) (combine (fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (pure saw) fun (k : E → Id Prop) => ∀ (x : E), ling x → k x)).eval = ∀ (x : E), ling x → saw x p

In a static reading of Polly saw every linguist a generalized quantifier in object position composes by scopal application and Lower discharges it.

theorem Charlow2014.eval_combine_monadLift {M : Type u → Type u} [Monad M] [LawfulMonad M] {α β γ : Type u} (f : α → β → γ) (m : M α) (n : M β) : (combine f (monadLift m) (monadLift n)).eval = combine f m n

Scopal application subsumes monadic application, since lifting, combining and lowering is combining in the underlying monad (Fact 3.14).

theorem Charlow2014.reset_combine_monadLift {M : Type u → Type u} [Monad M] [LawfulMonad M] {α β γ ρ : Type u} (f : α → β → γ) (m : M α) (n : M β) : (combine f (monadLift m) (monadLift n)).reset = monadLift (combine f m n)

Evaluating a combination of lifted programs and lifting the result is lifting their combination, so the side effects of the underlying monad, whichever it is, survive evaluation (Fact 4.1).

def Charlow2014.liftValue {E α β : Type} (a : α) : Tower E β α

liftValue a coerces a value into a trivial program and lifts it (Def. 2.9 with Lift), so (liftValue a).run k = k a, the Montague lift again (3.20).

Equations

• Charlow2014.liftValue a = monadLift (pure a)

@[simp]

theorem Charlow2014.run_liftValue {E α β : Type} (a : α) (k : α → StateSet E β) : ContT.run (liftValue a) k = k a

def Charlow2014.everyDP {E : Type} (P : E → Prop) : Tower E Prop E

Universal DPs as scope-takers (Table 3.1).

Equations

• Charlow2014.everyDP P = Charlow2014.every fun (x : E) => pure (P x)

def Charlow2014.noDP {E : Type} (P : E → Prop) : Tower E Prop E

Negative DPs as scope-takers (Table 3.1).

Equations

• Charlow2014.noDP P = Charlow2014.no fun (x : E) => pure (P x)

@[simp]

theorem Charlow2014.run_everyDP {E : Type} (P : E → Prop) (k : E → StateSet E Prop) : ContT.run (everyDP P) k = neg do let x ← indef P neg (k x)

@[simp]

theorem Charlow2014.run_noDP {E : Type} (P : E → Prop) (k : E → StateSet E Prop) : ContT.run (noDP P) k = neg (indef P >>= k)

theorem Charlow2014.name_saw_indef {E : Type} (j : E) (saw : E → E → Prop) (ling : E → Prop) : (combine (fun (x : E) (f : E → Prop) => f x) (liftValue j) (combine (fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (liftValue saw) (monadLift (indef ling)))).eval = do let x ← indef ling pure (saw x j)

In John saw a linguist the indefinite's nondeterminism survives Lower (3.23).

theorem Charlow2014.indef_saw_every {E : Type} (man ling : E → Prop) (saw : E → E → Prop) : (combine (fun (x : E) (f : E → Prop) => f x) (monadLift (indef man)) (combine (fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (liftValue saw) (everyDP ling))).eval = do let x ← indef man pure (∀ (y : E), ling y → saw y x)

In the surface-scope reading of a man saw every linguist the universal is trapped in the indefinite's scope (3.24).

Bind

def Charlow2014.bindShift {E β : Type} (m : Tower E β E) : Tower E β E

bindShift m is the Bind type-shifter (Def. 3.16), which pushes the tower's value onto the stack before continuing.

Equations

• Charlow2014.bindShift m k = ContT.run m fun (a : E) (s : Charlow2014.Stack E) => k a (s ++ [a])

@[simp]

theorem Charlow2014.run_bindShift {E β : Type} (m : Tower E β E) (k : E → StateSet E β) : ContT.run (bindShift m) k = ContT.run m fun (a : E) (s : Stack E) => k a (s ++ [a])

theorem Charlow2014.run_bindShift_eq_dref {E β : Type} (m : Tower E β E) (k : E → StateSet E β) : ContT.run (bindShift m) k = ContT.run m fun (a : E) => dref (pure a) >>= k

Bind continues from the value's dref introduction.

@[simp]

theorem Charlow2014.bindShift_monadLift {E β : Type} (m : StateSet E E) : bindShift (monadLift m) = monadLift (dref m)

Bind on a lifted program is dref introduction (Fact 3.15).

@[simp]

theorem Charlow2014.bindShift_liftValue {E β : Type} (a : E) : bindShift (liftValue a) = monadLift (dref (pure a))

theorem Charlow2014.run_bindShift_monadLift_indef {E β : Type} (P : E → Prop) (k : E → StateSet E β) : ContT.run (bindShift (monadLift (indef P))) k = fun (s : Stack E) => ⋃ (x : E), ⋃ (_ : P x), k x (s ++ [x])

A Bind-shifted lifted indefinite feeds its scope each satisfier with the extended stack, the DyS correspondence for indefinites (Fact 3.17).

theorem Charlow2014.run_monadLift_pro {E β : Type} (k : E → StateSet E β) : ContT.run (monadLift pro) k = fun (s : Stack E) => ⋃ x ∈ List.getLast? s, k x s

DyS correspondence for pronouns (Fact 3.18).

theorem Charlow2014.name_rubbed_pro_head {E : Type} (j : E) (rubbed : E → E → Prop) (head : E → E) : (combine (fun (x : E) (f : E → Prop) => f x) (bindShift (liftValue j)) (combine (fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (liftValue rubbed) (combine (fun (x : E) (f : E → E) => f x) (monadLift pro) (liftValue head)))).eval = fun (s : List E) => {(rubbed (head j) j, s ++ [j])}

John rubbed his head is bound without coindexation (3.25).

theorem Charlow2014.name_mom_saw_pro {E : Type} (j : E) (saw : E → E → Prop) (mom : E → E) : (combine (fun (x : E) (f : E → Prop) => f x) (combine (fun (x : E) (f : E → E) => f x) (bindShift (liftValue j)) (liftValue mom)) (combine (fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (liftValue saw) (monadLift pro))).eval = fun (s : List E) => {(saw j (mom j), s ++ [j])}

John's mom saw him is bound without surface c-command (3.26).

Inverse scope

External Lift of a tower is pure one level up (Fact 3.19), internal Lift is Functor.map pure (Def. 3.17), three-level combination is combine over combine (Def. 3.18), and one-fell-swoop Lower runs the outer tower at ContT.eval.

def Charlow2014.eval₂ {E β : Type} (m : Tower E β (Tower E β β)) : StateSet E β

Three-level Lower (Def. 3.19).

Equations

• Charlow2014.eval₂ m = ContT.run m ContT.eval

@[simp]

theorem Charlow2014.eval₂_def {E β : Type} (m : Tower E β (Tower E β β)) : eval₂ m = ContT.run m ContT.eval

theorem Charlow2014.every_over_indef {E : Type} (man ling : E → Prop) (saw : E → E → Prop) : eval₂ (combine (combine fun (x : E) (f : E → Prop) => f x) (pure (bindShift (monadLift (indef man)))) (combine (combine fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (pure (liftValue saw)) (pure <$> everyDP ling))) = pure (∀ (y : E), ling y → ∃ (x : E), man x ∧ saw y x)

In the inverse-scope reading of a man saw every linguist the universal discharges the indefinite's nondeterminism and dref (3.28).

theorem Charlow2014.every_owl_that_saw {E : Type} (owl : E → Prop) (saw : E → E → Prop) (a : E) (k : E → StateSet E Prop) : every (fun (x : E) => do let ν ← dref (pure x) let y ← pro pure (owl ν ∧ saw y a)) k = fun (s : Stack E) => {(∀ (ν : E), owl ν ∧ saw ν a → holds (k ν) (s ++ [ν]), s)}

In every owl that Al saw the gap is a pronoun bound by the determiner's dref, and the relative pronoun is conjunction (3.30).

Scope islands and exceptional scope

A scope island is a constituent that must be evaluated (Def. 4.2); evaluating and re-lifting is ContT.reset, and ContT.reset_monadLift is Fact 4.1: Reset is invisible to a lifted program, so whatever survives evaluation keeps taking scope. A tower whose value is itself a program is finished by lifting the value and lowering in one fell swoop, ContT.eval (m >>= monadLift).

theorem Charlow2014.reset_indef_left {E : Type} (ling left : E → Prop) : (combine (fun (x : E) (f : E → Prop) => f x) (monadLift (indef ling)) (liftValue left)).reset = monadLift do let x ← indef ling pure (left x)

Resetting a linguist left changes nothing, so indefinites escape islands (Fact 4.2, Examples.ex4_1a).

theorem Charlow2014.reset_every {E : Type} (ling left : E → Prop) : (combine (fun (x : E) (f : E → Prop) => f x) (everyDP ling) (liftValue left)).reset = liftValue (∀ (x : E), ling x → left x)

Resetting every linguist left discharges the universal into a truth condition on the bottom level, so quantifiers do not escape (Fact 4.4, Examples.ex4_1b, Examples.ex4_1c).

theorem Charlow2014.reset_indef_every {E : Type} (man ling : E → Prop) (met : E → E → Prop) : (combine (fun (x : E) (f : E → Prop) => f x) (bindShift (monadLift (indef man))) (combine (fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (liftValue met) (everyDP ling))).reset = monadLift do let x ← dref (indef man) pure (∀ (y : E), ling y → met y x)

Resetting a man met every linguist keeps the indefinite's nondeterminism and dref but not the universal (Fact 4.5).

theorem Charlow2014.reset_every_indef {E : Type} (man ling : E → Prop) (met : E → E → Prop) : monadLift (eval₂ (combine (combine fun (x : E) (f : E → Prop) => f x) (pure (bindShift (monadLift (indef man)))) (combine (combine fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (pure (liftValue met)) (pure <$> everyDP ling)))) = liftValue (∀ (y : E), ling y → ∃ (x : E), man x ∧ met y x)

Resetting the inverse-scope reading cannot reanimate an indefinite that an inverse-scoped universal discharged (Fact 4.6).

theorem Charlow2014.reset_every_pro {E α : Type} (ling : E → Prop) (met : E → E → Prop) (k : Prop → StateSet E α) {s : Stack E} (h : s ≠ []) : (combine (fun (x : E) (f : E → Prop) => f x) (everyDP ling) (combine (fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (liftValue met) (monadLift pro))).reset.run k s = ContT.run (monadLift do let y ← pro pure (∀ (x : E), ling x → met y x)) k s

Resetting every linguist met her keeps the pronoun's stack sensitivity past the universal (Fact 4.7).

theorem Charlow2014.exceptional_binding {E : Type} (man ling left : E → Prop) (met : E → E → Prop) : (combine (fun (x : Prop) (f : Prop → Prop) => f x) (combine (fun (x : E) (f : E → Prop) => f x) (bindShift (monadLift (indef man))) (combine (fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (liftValue met) (everyDP ling))).reset (combine (fun (x1 : Prop → Prop → Prop) (x2 : Prop) => x1 x2) (liftValue fun (q p : Prop) => p ∧ q) (combine (fun (x : E) (f : E → Prop) => f x) (monadLift pro) (liftValue left)).reset)).eval = do let x ← dref (indef man) pure ((∀ (y : E), ling y → met y x) ∧ left x)

In a man met every linguist, and he left both sentences are Reset and the indefinite binds across them (4.7).

theorem Charlow2014.exceptional_neg {E : Type} (rel ling : E → Prop) (met : E → E → Prop) : (combine (fun (x1 : StateSet E Prop → StateSet E Prop) (x2 : StateSet E Prop) => x1 x2) (liftValue neg) (pure <$> (combine (fun (x : E) (f : E → Prop) => f x) (monadLift (indef rel)) (combine (fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (liftValue met) (everyDP ling))).reset) >>= monadLift).eval = do let x ← indef rel pure ¬∀ (y : E), ling y → met y x

After Reset the embedded indefinite's nondeterminism outscopes it wasn't the case that, exceptional scope over negation (4.8).

theorem Charlow2014.exceptional_cond {E : Type} (rel dies : E → Prop) (rich : Prop) : (combine (fun (x1 : StateSet E Prop → StateSet E Prop) (x2 : StateSet E Prop) => x1 x2) (combine (fun (x1 : StateSet E Prop → StateSet E Prop → StateSet E Prop) (x2 : StateSet E Prop) => x1 x2) (liftValue cond) (pure <$> (combine (fun (x : E) (f : E → Prop) => f x) (monadLift (indef rel)) (liftValue dies)).reset)) (pure <$> liftValue rich) >>= monadLift).eval = do let x ← indef rel pure (dies x → rich)

If a relative of mine dies, I'll be rich gets ∃ > if from a Reset antecedent (4.9, Examples.ex4_1a). The thesis notes that the truth conditions are a little too weak, one relative who does not die verifying the conditional.

theorem Charlow2014.island_cond_every {E : Type} (rel dies : E → Prop) (rich : Prop) : (combine (fun (x1 : StateSet E Prop → StateSet E Prop) (x2 : StateSet E Prop) => x1 x2) (combine (fun (x1 : StateSet E Prop → StateSet E Prop → StateSet E Prop) (x2 : StateSet E Prop) => x1 x2) (liftValue cond) (pure <$> (combine (fun (x : E) (f : E → Prop) => f x) (everyDP rel) (liftValue dies)).reset)) (pure <$> liftValue rich) >>= monadLift).eval = pure ((∀ (x : E), rel x → dies x) → rich)

In if every relative of mine dies, I'll be rich the universal is discharged inside the Reset antecedent, so the conditional is a plain truth condition with the universal below if, and no reading puts it above (Examples.ex4_1b).

theorem Charlow2014.exceptional_feeds_binding {E : Type} (rel dies steelMagnate : E → Prop) (rich : Prop) : (combine (fun (x : Prop) (f : Prop → Prop) => f x) (monadLift (combine (fun (x1 : StateSet E Prop → StateSet E Prop) (x2 : StateSet E Prop) => x1 x2) (combine (fun (x1 : StateSet E Prop → StateSet E Prop → StateSet E Prop) (x2 : StateSet E Prop) => x1 x2) (liftValue cond) (pure <$> (combine (fun (x : E) (f : E → Prop) => f x) (bindShift (monadLift (indef rel))) (liftValue dies)).reset)) (pure <$> liftValue rich) >>= monadLift).eval) (combine (fun (x1 : Prop → Prop → Prop) (x2 : Prop) => x1 x2) (liftValue fun (q p : Prop) => p ∧ q) (combine (fun (x : E) (f : E → Prop) => f x) (monadLift pro) (liftValue steelMagnate)).reset)).eval = do let x ← dref (indef rel) pure ((dies x → rich) ∧ steelMagnate x)

Exceptional scope feeds binding, since the dref of a relative of mine escapes the conditional and binds she (4.11).

theorem Charlow2014.brc_derivation {E : Type} (cand : E → Prop) (paperBy submitted : E → E → Prop) : eval₂ (combine (combine fun (x : E) (f : E → Prop) => f x) (pure (bindShift (noDP cand))) (combine (combine fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (pure (liftValue submitted)) (pure <$> monadLift do let z ← pro indef (paperBy z)))) = do let z ← pro let y ← indef (paperBy z) pure ¬∃ (x : E), cand x ∧ submitted y x

Giving a paper he wrote scope over no candidate evaluates the pronoun outside the quantifier's scope, the Binder Roof Constraint (4.12, Examples.ex4_4).

Choice functions (section 4.7.1)

The choice-functional theory interprets an indefinite as a choice function applied to its restrictor and closes the function existentially wherever it likes, so the indefinite takes apparent scope without moving. When the restrictor varies with a bound variable, closing the function above the binder yields readings that no scope-taking derivation gives.

theorem Charlow2014.cf_exceptional_cond {E : Type} (rel dies : E → Prop) (rich : Prop) (hrel : ∃ (x : E), rel x) (s : Stack E) : (∃ (f : Reference.ChoiceFunction E), dies (f rel) → rich) ↔ holds (do let x ← indef rel pure (dies x → rich)) s

Closing the choice function above the conditional gives the exceptional reading that exceptional_cond derives by scope (4.34).

theorem Charlow2014.cf_no_candidate_iff {E : Type} [Nonempty E] (cand : E → Prop) (paperBy submitted : E → E → Prop) (hwrote : ∀ (x : E), cand x → ∃ (y : E), paperBy x y) (hinj : Set.InjOn paperBy {x : E | cand x}) : (∃ (f : Reference.ChoiceFunction E), ¬∃ (x : E), cand x ∧ submitted (f (paperBy x)) x) ↔ ¬∃ (x : E), cand x ∧ ∀ (y : E), paperBy x y → submitted y x

Closing the choice function above no candidate gives the reading on which no candidate submitted every paper he wrote ([Sch01]), given that every candidate wrote a paper and no two wrote the same papers (4.35, Examples.ex4_4).

theorem Charlow2014.cf_same_restrictor_iff {E : Type} (girl : E → Prop) (boysFancied gave : E → E → Prop) {B : E → Prop} (hB : ∃ (y : E), B y) (hsame : ∀ (x : E), girl x → boysFancied x = B) : (∃ (f : Reference.ChoiceFunction E), ∀ (x : E), girl x → gave (f (boysFancied x)) x) ↔ ∃ (y : E), B y ∧ ∀ (x : E), girl x → gave y x

When every girl fancies the same boys B, a choice function closed above every girl picks one boy for all of them, the reading [Geu00] objects to (4.36).

theorem Charlow2014.cf_layered_iff {E : Type} [Nonempty E] (linguist : E → Prop) (bookBy : E → E → Prop) (read : E → Prop) (hling : ∃ (x : E), linguist x) (hbook : ∀ (x : E), linguist x → ∃ (y : E), bookBy x y) (hinj : Set.InjOn bookBy {x : E | linguist x}) : (∃ (f : Reference.ChoiceFunction E), ¬∃ (g : Reference.ChoiceFunction E), read (f (bookBy (g linguist)))) ↔ ∀ (x : E), linguist x → ∃ (y : E), bookBy x y ∧ ¬read y

Closing the choice function of a book by … above negation and that of a famous linguist below it gives the reading that every famous linguist wrote a book I did not read, given that no two famous linguists wrote the same books (4.37, Examples.ex4_6).

theorem Charlow2014.cf_disjunction_iff {E : Type} [Nonempty E] (cand : E → Prop) (vita portfolio : E → E) (submit : E → E → Prop) (hinj : Set.InjOn (fun (x y : E) => y = vita x ∨ y = portfolio x) {x : E | cand x}) : (∃ (f : Reference.ChoiceFunction E), ¬∃ (x : E), cand x ∧ submit (f fun (y : E) => y = vita x ∨ y = portfolio x) x) ↔ ¬∃ (x : E), cand x ∧ submit (vita x) x ∧ submit (portfolio x) x

A choice function closed above no candidate over the doubleton of each candidate's vita and portfolio gives the reading that no candidate submitted both, given that the doubletons are distinct (4.38).

Selective exceptional scope

Two indefinites on one island yield three fully evaluated programs: one StateSet E Prop with the nondeterminism agglomerated, and two StateSet E (StateSet E Prop) layerings. A layered program unfolds back into a three-level tower after evaluation, so the indefinites scope separately.

theorem Charlow2014.indef_visits_indef {E : Type} (law rel : E → Prop) (visits : E → E → Prop) : (combine (fun (x : E) (f : E → Prop) => f x) (monadLift (indef law)) (combine (fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (liftValue visits) (monadLift (indef rel)))).eval = do let x ← indef law let y ← indef rel pure (visits y x)

A persuasive lawyer visits a relative of mine, agglomerated.

theorem Charlow2014.indef_visits_indef_layered {E : Type} (law rel : E → Prop) (visits : E → E → Prop) : (ContT.eval <$> combine (combine fun (x : E) (f : E → Prop) => f x) (pure (monadLift (indef law))) (combine (combine fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (pure (liftValue visits)) (pure <$> monadLift (indef rel)))).eval = do let y ← indef rel pure do let x ← indef law pure (visits y x)

A persuasive lawyer visits a relative of mine, layered with the object indefinite outermost (section 4.5.2), the structure behind Examples.ex4_18b.

theorem Charlow2014.monadLift_layered {M : Type u → Type u} [Monad M] [LawfulMonad M] {ρ α β : Type u} (m : M α) (f : α → M β) : (monadLift <$> monadLift do let y ← m pure (f y)) = fun (c : ContT ρ M β → M ρ) => do let y ← m c (monadLift (f y))

Lifting a layered program twice restores the three-level tower.

Plural indefinites and distributivity

Plural individuals are sets of atoms (Def. 4.3), atoms identified with singletons. Plural indefinites are nondeterministic like singular ones, so their existential scope escapes islands, while the distributivity operator is a scope-taker discharged on evaluation.

def Charlow2014.distr {α A : Type} (R : Set A → α) (X : Set A) : Tower (Set A) Prop α

distr R X is the distributivity operator (Def. 4.5), a tower quantifying over the atoms of its plural argument.

Equations

• Charlow2014.distr R X k s = {(∀ x ∈ X, Charlow2014.holds (k (R {x})) s, s)}

@[simp]

theorem Charlow2014.run_distr {α A : Type} (R : Set A → α) (X : Set A) (k : α → StateSet (Set A) Prop) : ContT.run (distr R X) k = fun (s : Stack (Set A)) => {(∀ x ∈ X, holds (k (R {x})) s, s)}

theorem Charlow2014.indef_fronts_two_distr {A : Type} (guard bldgs : Set A → Prop) (fronts : Set A → Set A → Prop) : (ContT.run (combine (combine (combine fun (x : Set A) (f : Set A → Prop) => f x)) (pure (pure (monadLift (indef guard)))) ((fun (x : Tower (Set A) Prop (Set A → Prop)) => pure <$> x) <$> distr fronts <$> monadLift (indef fun (X : Set A) => bldgs X ∧ X.ncard = 2))) fun (x : Tower (Set A) Prop (Tower (Set A) Prop Prop)) => ContT.run x ContT.eval) = do let Y ← indef fun (X : Set A) => bldgs X ∧ X.ncard = 2 pure (∀ y ∈ Y, ∃ (x : Set A), guard x ∧ fronts {y} x)

In the distributive inverse-scope reading of a guard is standing in front of two buildings guards vary with buildings, and the plural's nondeterminism outscopes the distributed universal (4.17).

Disjunction

Program disjunction is <|> in StateT _ Set (Def. 4.6, the union of outputs); or disjoins two scope-takers' results (Def. 4.7). Disjunctions are therefore nondeterministic programs that survive Reset, bind donkey pronouns, and, being polymorphic, scope over an operator that scopes over their disjuncts.

theorem Charlow2014.orElse_apply {E α : Type} (m n : StateSet E α) (s : Stack E) : (m <|> n) s = m s ∪ n s

@[simp]

theorem Charlow2014.mem_orElse {E α : Type} (m n : StateSet E α) (s : Stack E) (q : α × Stack E) : q ∈ (m <|> n) s ↔ q ∈ m s ∨ q ∈ n s

theorem Charlow2014.orElse_bind {E α β : Type} (m n : StateSet E α) (f : α → StateSet E β) : (m <|> n) >>= f = (m >>= f <|> n >>= f)

def Charlow2014.or {E α β : Type} (m n : Tower E β α) : Tower E β α

Disjunction of scope-takers (Def. 4.7).

Equations

• Charlow2014.or m n k = (ContT.run m k <|> ContT.run n k)

@[simp]

theorem Charlow2014.run_or {E α β : Type} (m n : Tower E β α) (k : α → StateSet E β) : ContT.run (or m n) k = (ContT.run m k <|> ContT.run n k)

theorem Charlow2014.or_names_left {E : Type} (c m : E) (left : E → Prop) : (combine (fun (x : E) (f : E → Prop) => f x) (or (bindShift (liftValue c)) (bindShift (liftValue m))) (liftValue left)).eval = do let x ← dref (pure c) <|> dref (pure m) pure (left x)

Chomsky or May left introduces a dref in nondeterministic superposition (4.27).

theorem Charlow2014.or_subparts {E : Type} (me a c : E) (see hear : E → E → Prop) : (combine (fun (x : E) (f : E → Prop) => f x) (liftValue me) (or (combine (fun (x : E) (f : E → E → Prop) => f x) (bindShift (liftValue a)) (liftValue see)) (combine (fun (x : E) (f : E → E → Prop) => f x) (bindShift (liftValue c)) (liftValue hear)))).eval = ((do let x ← dref (pure a) pure (see x me)) <|> do let x ← dref (pure c) pure (hear x me))

In whenever I see Alf or hear Cal, I scream his name the antecedent is a proper subpart of each disjunct, and the disjunctive program still hosts the dref (4.28).

theorem Charlow2014.or_pure_pure {E : Type} (steak burger : E → Prop) : or (pure (monadLift (indef steak))) (pure (monadLift (indef burger))) = fun (c : Tower E Prop E → StateSet E Prop) => c (monadLift (indef steak)) <|> c (monadLift (indef burger))

Disjoining externally lifted indefinites puts program disjunction above the continuation and the indefinites below it, disjunction under the Binder Roof Constraint (4.29).

theorem Charlow2014.or_over_every {E : Type} (person steak burger : E → Prop) (ate : E → E → Prop) : eval₂ (combine (combine fun (x : E) (f : E → Prop) => f x) (pure (everyDP person)) (combine (combine fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (pure (liftValue ate)) (or (pure (monadLift (indef steak))) (pure (monadLift (indef burger)))))) = (pure (∀ (y : E), person y → ∃ (x : E), steak x ∧ ate x y) <|> pure (∀ (y : E), person y → ∃ (x : E), burger x ∧ ate x y))

In either everyone ate a steak or a hamburger, with everyone externally lifted beside the disjunction of (4.29), the universal outscopes each indefinite and not the disjunction's nondeterminism, which lives on the top level (Examples.ex4_24b).

theorem Charlow2014.or_map_pure_every {E : Type} (steak burger : E → Prop) : or (pure <$> everyDP steak) (pure <$> everyDP burger) = fun (c : Tower E Prop E → StateSet E Prop) => (ContT.run (everyDP steak) fun (x : E) => c (pure x)) <|> ContT.run (everyDP burger) fun (x : E) => c (pure x)

In someone ate every steak or every burger disjoining internally lifted universals puts their scopal effects, with the disjunction, on the top level (4.30).

theorem Charlow2014.or_or_names {E : Type} (m j b : E) : (ContT.eval <$> or (pure (or (liftValue m) (liftValue j))) (pure (liftValue b))).eval = (pure (pure m <|> pure j) <|> pure (pure b))

In the higher-order disjunctive program Mary or John or Bill (4.31) the disjunction of Mary and John is lifted and disjoined with Bill, and lowering twice leaves the layering {{m, j}, b}.

Drefs of proper names take exceptional scope

Anything Bind-shifted survives evaluation (Fact 1.4, Ch. 5.2), so a proper name inside an island binds a sloppy pro-form outside it.

theorem Charlow2014.name_dref_inverse {E : Type} (person : E → Prop) (thinks : Prop → E → Prop) (come : E → Prop) (b : E) : eval₂ (combine (combine fun (x : E) (f : E → Prop) => f x) (pure (everyDP person)) (combine (combine fun (x1 : Prop → E → Prop) (x2 : Prop) => x1 x2) (pure (liftValue thinks)) (pure <$> combine (fun (x : E) (f : E → Prop) => f x) (bindShift (liftValue b)) (liftValue come)))) = do let y ← dref (pure b) pure (∀ (x : E), person x → thinks (come y) x)

In everyone thinks BILL will come Bill's dref takes inverse scope over the dynamically closed everyone (5.8, Examples.ex5_7a).

theorem Charlow2014.name_dref_cond {E : Type} (person : E → Prop) (thinks : Prop → E → Prop) (come invite : E → Prop) (b : E) : (cond (do let y ← dref (pure b) pure (∀ (x : E), person x → thinks (come y) x)) do let z ← pro pure ¬invite z) = pure ((∀ (x : E), person x → thinks (come b) x) → ¬invite b)

In … we'll have to invite him the escaped dref binds the consequent's pronoun, so replacing BILL by John yields a meaning identical to the antecedent's and Contrast is satisfiable.

Maximal drefs and dynamic generalized quantifiers

A dynamic GQ (Def. 5.3) returns its truth condition and pushes the refset — the restrictor individuals satisfying the scope — as a plural dref. The stack holds pluralities; the quantifier ranges over atoms.

def Charlow2014.dynGQ {A : Type} (DET : Set A → Set A → Prop) (M : Set A) : Tower (Set A) Prop A

Dynamic GQ with a maximal refset dref (Def. 5.3).

Equations

• Charlow2014.dynGQ DET M k s = {(DET M {x : A | x ∈ M ∧ Charlow2014.holds (k x) s}, s ++ [{x : A | x ∈ M ∧ Charlow2014.holds (k x) s}])}

@[simp]

theorem Charlow2014.run_dynGQ {A : Type} (DET : Set A → Set A → Prop) (M : Set A) (k : A → StateSet (Set A) Prop) : ContT.run (dynGQ DET M) k = fun (s : Stack (Set A)) => {(DET M {x : A | x ∈ M ∧ holds (k x) s}, s ++ [{x : A | x ∈ M ∧ holds (k x) s}])}

theorem Charlow2014.dynGQ_left {A : Type} (ling left : Set A) : (combine (fun (x : A) (f : A → Prop) => f x) (dynGQ (fun (x N : Set A) => N.ncard = 1) ling) (liftValue fun (x : A) => x ∈ left)).eval = do let N ← dref (pure (ling ∩ left)) pure (N.ncard = 1)

Exactly one linguist left is true iff one linguist left, with the linguists who left on the stack (5.19).

theorem Charlow2014.dynGQ_pro {A : Type} (ling left : Set A) (tired : Set A → Prop) : (combine (fun (x : Prop) (f : Prop → Prop) => f x) (monadLift do let N ← dref (pure (ling ∩ left)) pure (N.ncard = 1)) (combine (fun (x1 : Prop → Prop → Prop) (x2 : Prop) => x1 x2) (liftValue fun (q p : Prop) => p ∧ q) (combine (fun (x : Set A) (f : Set A → Prop) => f x) (monadLift pro) (liftValue tired)))).eval = do let N ← dref (pure (ling ∩ left)) pure (N.ncard = 1 ∧ tired N)

In exactly one linguist left; she was tired the pronoun is the maximal dref (5.3.2).

theorem Charlow2014.dynGQ_neg {A : Type} (sen admire : Set A) : (combine (fun (x1 : StateSet (Set A) Prop → StateSet (Set A) Prop) (x2 : StateSet (Set A) Prop) => x1 x2) (liftValue neg) (pure <$> (combine (fun (x : A) (f : A → Prop) => f x) (dynGQ (fun (x N : Set A) => N = ∅) sen) (liftValue fun (x : A) => x ∈ admire)).reset) >>= monadLift).eval = do let N ← dref (pure (sen ∩ admire)) pure ¬N = ∅

In it's absolutely false that no senators admire Cruz negation flips the truth value, and the refset dref survives for they (5.24, Examples.ex5_23).

The Focus monad

Rooth's two-dimensional focus semantics is the pointed-powerset monad ([Sha02a]): a value paired with its alternatives, sequencing the Identity monad on the first coordinate and the Set monad on the second (Def. 5.6). It is the library's WithAlternatives, whose monad laws are the thesis's Appendix B.9. F-marking injects a value with its alternatives; only/also quantify over the alternatives of a monadic VP (Def. 5.10). Focus effects are managed by scope like any other, so they survive Reset and can be layered for selective association across islands.

theorem Charlow2014.Focus.combine_eq_map₂ {α β γ : Type u} (f : α → β → γ) (m : WithAlternatives α) (n : WithAlternatives β) : combine f m n = WithAlternatives.map₂ f m n

Application in the Focus monad is binary composition, pointwise on values and NA on alternatives, Rooth's two interpretation functions at once (Fact 5.4).

def Charlow2014.Focus.fmark {E : Type} (alt : E → Set E) (a : E) : WithAlternatives E

fmark alt a is F-marking (Def. 5.7), a value with its contextual alternatives.

Equations

• Charlow2014.Focus.fmark alt a = { ordinary := a, alternatives := alt a }

def Charlow2014.Focus.toSet {E W : Type} (Q : E → W → Prop) : Set (E × W)

A VP meaning as the set of subject–world pairs it holds of.

Equations

• Charlow2014.Focus.toSet Q = {xw : E × W | Q xw.1 xw.2}

@[simp]

theorem Charlow2014.Focus.mem_toSet {E W : Type} {Q : E → W → Prop} {x : E} {w : W} : (x, w) ∈ toSet Q ↔ Q x w

theorem Charlow2014.Focus.toSet_injective {E W : Type} : Function.Injective toSet

def Charlow2014.Focus.only {E W : Type} (P : WithAlternatives (E → W → Prop)) : E → W → Prop

only P holds of x at w when the VP's value is among its alternatives and only on the identity scale is true at (x, w).

Equations

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

def Charlow2014.Focus.also {E W : Type} (P : WithAlternatives (E → W → Prop)) : E → W → Prop

also P holds of x at w when the VP's value is among its alternatives and the additive on the identity scale is true at (x, w).

Equations

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

theorem Charlow2014.Focus.only_iff {E W : Type} (P : WithAlternatives (E → W → Prop)) (x : E) (w : W) : only P x w ↔ {Q : E → W → Prop | Q ∈ P.alternatives ∧ Q x w} = {P.ordinary}

Only is Def. 5.10's, true where the VP's value is the sole true alternative.

theorem Charlow2014.Focus.also_iff {E W : Type} (P : WithAlternatives (E → W → Prop)) (x : E) (w : W) : also P x w ↔ {P.ordinary} ⊂ {Q : E → W → Prop | Q ∈ P.alternatives ∧ Q x w}

Also is Def. 5.10's, true where some alternative besides the VP's value is true too.

theorem Charlow2014.Focus.fmark_left {E : Type} (alt : E → Set E) (j : E) (left : E → Prop) : (combine (fun (x : E) (f : E → Prop) => f x) (monadLift (fmark alt j)) (monadLift (pure left))).eval = { ordinary := left j, alternatives := {p : Prop | ∃ x ∈ alt j, p = left x} }

JOHNᶠ left (5.30).

theorem Charlow2014.Focus.only_met_fmark {E W : Type} (alt : E → Set E) (j : E) (met : E → E → W → Prop) : only (combine (fun (x1 : E → E → W → Prop) (x2 : E) => x1 x2) (monadLift (pure met)) (monadLift (fmark alt j))).eval = fun (x : E) (w : W) => {Q : E → W → Prop | (∃ y ∈ alt j, Q = met y) ∧ Q x w} = {met j}

Sharon only met JOHNᶠ associates with focus at the VP.

theorem Charlow2014.Focus.only_fmark_fmark {E W : Type} (alt : E → Set E) (b s : E) (intro : E → E → E → W → Prop) : only (combine (fun (x1 : E → E → W → Prop) (x2 : E) => x1 x2) (combine (fun (x1 : E → E → E → W → Prop) (x2 : E) => x1 x2) (monadLift (pure intro)) (monadLift (fmark alt b))) (monadLift (fmark alt s))).eval = fun (z : E) (w : W) => {Q : E → W → Prop | (∃ x ∈ alt b, ∃ y ∈ alt s, Q = intro x y) ∧ Q z w} = {intro b s}

In unselective association only binds both foci in its scope (5.4.3).

theorem Charlow2014.Focus.only_focus_layered {E W : Type} (alt : E → Set E) (b s : E) (intro : E → E → E → W → Prop) : (combine (fun (x1 : WithAlternatives (E → W → Prop) → E → W → Prop) (x2 : WithAlternatives (E → W → Prop)) => x1 x2) (monadLift (pure only)) (ContT.eval <$> combine (combine fun (x1 : E → E → W → Prop) (x2 : E) => x1 x2) (combine (combine fun (x1 : E → E → E → W → Prop) (x2 : E) => x1 x2) (pure (monadLift (pure intro))) (pure (monadLift (fmark alt b)))) (pure <$> monadLift (fmark alt s)))).eval = { ordinary := only (combine (fun (x1 : E → E → W → Prop) (x2 : E) => x1 x2) (combine (fun (x1 : E → E → E → W → Prop) (x2 : E) => x1 x2) (pure intro) (fmark alt b)) (pure s)), alternatives := {P : E → W → Prop | ∃ y ∈ alt s, P = only (combine (fun (x1 : E → E → W → Prop) (x2 : E) => x1 x2) (combine (fun (x1 : E → E → E → W → Prop) (x2 : E) => x1 x2) (pure intro) (fmark alt b)) (pure y))} }

In selective association, with BILLᶠ externally and SUEᶠ internally lifted, only catches Bill's alternatives at the inner level and Sue's survive to also, for the scope order also > SUEᶠ > only > BILLᶠ (5.4.4, Examples.ex5_27b).

theorem Charlow2014.Focus.also_only_focus_layered {E W : Type} (alt : E → Set E) (b s : E) (intro : E → E → E → W → Prop) : also (combine (fun (x1 : WithAlternatives (E → W → Prop) → E → W → Prop) (x2 : WithAlternatives (E → W → Prop)) => x1 x2) (monadLift (pure only)) (ContT.eval <$> combine (combine fun (x1 : E → E → W → Prop) (x2 : E) => x1 x2) (combine (combine fun (x1 : E → E → E → W → Prop) (x2 : E) => x1 x2) (pure (monadLift (pure intro))) (pure (monadLift (fmark alt b)))) (pure <$> monadLift (fmark alt s)))).eval = fun (z : E) (w : W) => {only (combine (fun (x1 : E → E → W → Prop) (x2 : E) => x1 x2) (combine (fun (x1 : E → E → E → W → Prop) (x2 : E) => x1 x2) (pure intro) (fmark alt b)) (pure s))} ⊂ {Q : E → W → Prop | (∃ y ∈ alt s, Q = only (combine (fun (x1 : E → E → W → Prop) (x2 : E) => x1 x2) (combine (fun (x1 : E → E → E → W → Prop) (x2 : E) => x1 x2) (pure intro) (fmark alt b)) (pure y))) ∧ Q z w}

In he also only introduced BILLᶠ to SUEᶠ merging in also captures the surviving alternatives of SUEᶠ, for the scope order also > SUEᶠ > only > BILLᶠ (Examples.ex5_27b).

theorem Charlow2014.Focus.reset_fmark {E : Type} (alt : E → Set E) (j : E) (left : E → Prop) : (combine (fun (x : E) (f : E → Prop) => f x) (monadLift (fmark alt j)) (monadLift (pure left))).reset = monadLift do let x ← fmark alt j pure (left x)

Focus effects survive Reset, an instance of Fact 4.1.

theorem Charlow2014.focus_over_stateSet {E : Type} (alt : E → Set E) (p : E) (ling : E → Prop) (met : E → E → Prop) : (ContT.eval <$> combine (combine fun (x : E) (f : E → Prop) => f x) (pure (monadLift (indef ling))) (combine (combine fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (pure (liftValue met)) (pure <$> monadLift (Focus.fmark alt p)))).eval = { ordinary := do let x ← indef ling pure (met p x), alternatives := {π : StateSet E Prop | ∃ y ∈ alt p, π = do let x ← indef ling pure (met y x)} }

With two underlying monads, Focus effects on the top level and State.Set effects on the second evaluate to a layered WithAlternatives (StateSet E Prop) (5.4.5).

Alternative semantics: the Reader.Set monad

Swapping StateT for ReaderT over Set gives [KS17]-style alternative semantics with scope-managed side effects: indefinites still take selective exceptional scope, and Bind (Def. 5.21) handles in-scope binding without the abstraction rule [Sha04] criticised. But pure discards the stack, so nothing binds out of an island: the account of exceptional scope lives in the Set monad both share, the account of exceptional binding in State.

@[reducible, inline]

abbrev Charlow2014.ReaderSet (E α : Type) : Type

The Reader.Set monad is ReaderT over the Set monad.

Equations

• Charlow2014.ReaderSet E = ReaderT (Charlow2014.Stack E) Set

def Charlow2014.ReaderSet.indef {E : Type} (P : E → Prop) : ReaderSet E E

indef P is an indefinite, a nondeterministic individual insensitive to the stack.

Equations

• Charlow2014.ReaderSet.indef P x✝ = {x : E | P x}

def Charlow2014.ReaderSet.pro {E : Type} : ReaderSet E E

pro is a pronoun, the topical dref.

Equations

• Charlow2014.ReaderSet.pro s = {x : E | List.getLast? s = some x}

def Charlow2014.ReaderSet.holds {E : Type} (m : ReaderSet E Prop) (s : Stack E) : Prop

Some output is true.

Equations

• m.holds s = ∃ p ∈ m s, p

def Charlow2014.ReaderSet.neg {E : Type} (m : ReaderSet E Prop) : ReaderSet E Prop

Negation (Def. 5.18).

Equations

• m.neg s = {¬m.holds s}

def Charlow2014.ReaderSet.everyDP {E : Type} (P : E → Prop) : ContT Prop (ReaderSet E) E

The universal (Def. 5.19).

Equations

• Charlow2014.ReaderSet.everyDP P k = (do let x ← Charlow2014.ReaderSet.indef P (k x).neg).neg

def Charlow2014.ReaderSet.noDP {E : Type} (P : E → Prop) : ContT Prop (ReaderSet E) E

The negative quantifier.

Equations

• Charlow2014.ReaderSet.noDP P k = (Charlow2014.ReaderSet.indef P >>= k).neg

def Charlow2014.ReaderSet.bindShift {E β : Type} (m : ContT β (ReaderSet E) E) : ContT β (ReaderSet E) E

bindShift m is Bind for Reader.Set towers (Def. 5.21), whose continuation reads the extended stack.

Equations

• Charlow2014.ReaderSet.bindShift m k = m.run fun (a : E) (s : Charlow2014.Stack E) => k a (s ++ [a])

@[simp]

theorem Charlow2014.ReaderSet.mem_indef {E : Type} (P : E → Prop) (s : Stack E) (x : E) : x ∈ indef P s ↔ P x

@[simp]

theorem Charlow2014.ReaderSet.mem_pro {E : Type} (s : Stack E) (x : E) : x ∈ pro s ↔ List.getLast? s = some x

@[simp]

theorem Charlow2014.ReaderSet.neg_apply {E : Type} (m : ReaderSet E Prop) (s : Stack E) : m.neg s = {¬m.holds s}

@[simp]

theorem Charlow2014.ReaderSet.holds_pure {E : Type} (p : Prop) (s : Stack E) : (pure p).holds s ↔ p

@[simp]

theorem Charlow2014.ReaderSet.holds_bind {E α : Type} (m : ReaderSet E α) (k : α → ReaderSet E Prop) (s : Stack E) : (m >>= k).holds s ↔ ∃ x ∈ m s, (k x).holds s

@[simp]

theorem Charlow2014.ReaderSet.holds_map {E α : Type} (f : α → Prop) (m : ReaderSet E α) (s : Stack E) : (f <$> m).holds s ↔ ∃ x ∈ m s, f x

@[simp]

theorem Charlow2014.ReaderSet.holds_neg {E : Type} (m : ReaderSet E Prop) (s : Stack E) : m.neg.holds s ↔ ¬m.holds s

@[simp]

theorem Charlow2014.ReaderSet.run_everyDP {E : Type} (P : E → Prop) (k : E → ReaderSet E Prop) : (everyDP P).run k = (do let x ← indef P (k x).neg).neg

@[simp]

theorem Charlow2014.ReaderSet.run_noDP {E : Type} (P : E → Prop) (k : E → ReaderSet E Prop) : (noDP P).run k = (indef P >>= k).neg

@[simp]

theorem Charlow2014.ReaderSet.run_bindShift {E β : Type} (m : ContT β (ReaderSet E) E) (k : E → ReaderSet E β) : (bindShift m).run k = m.run fun (a : E) (s : Stack E) => k a (s ++ [a])

theorem Charlow2014.ReaderSet.reset_indef_left {E : Type} (ling left : E → Prop) : (combine (fun (x : E) (f : E → Prop) => f x) (monadLift (indef ling)) (monadLift (pure left))).reset = monadLift do let x ← indef ling pure (left x)

Resetting a linguist left keeps the indefinite (Fact 5.7).

theorem Charlow2014.ReaderSet.reset_every {E : Type} (ling left : E → Prop) : (combine (fun (x : E) (f : E → Prop) => f x) (everyDP ling) (monadLift (pure left))).reset = monadLift (pure (∀ (x : E), ling x → left x))

Resetting every linguist left discharges the universal (Fact 5.8).

theorem Charlow2014.ReaderSet.indef_met_indef_layered {E : Type} (sem phon : E → Prop) (met : E → E → Prop) : (ContT.eval <$> combine (combine fun (x : E) (f : E → Prop) => f x) (pure (monadLift (indef sem))) (combine (combine fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (pure (monadLift (pure met))) (pure <$> monadLift (indef phon)))).eval = do let y ← indef phon pure do let x ← indef sem pure (met y x)

Layered M (M Prop) derivation of a semanticist met a phonologist (Fact 5.9).

theorem Charlow2014.ReaderSet.bind_pro_append {E α : Type} (π : E → ReaderSet E α) (s : Stack E) (a : E) : (pro >>= π) (s ++ [a]) = π a (s ++ [a])

A pronoun read at an extended stack evaluates to the new dref (Fact 5.12).

theorem Charlow2014.ReaderSet.indef_rubbed_pro_head {E : Type} (ling : E → Prop) (rubbed : E → E → Prop) (head : E → E) : (combine (fun (x : E) (f : E → Prop) => f x) (bindShift (monadLift (indef ling))) (combine (fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (monadLift (pure rubbed)) (combine (fun (x : E) (f : E → E) => f x) (monadLift pro) (monadLift (pure head))))).eval = do let x ← indef ling pure (rubbed (head x) x)

A linguist rubbed his head is bound in scope via Bind.

theorem Charlow2014.ReaderSet.indef_told_no_indef_pro {E : Type} (man person : E → Prop) (bookBy : E → E → Prop) (told : E → E → E → Prop) : (combine (combine fun (x : E) (f : E → Prop) => f x) (pure <$> bindShift (monadLift (indef man))) (combine (combine fun (x1 : E → E → Prop) (x2 : E) => x1 x2) (pure (combine (fun (x1 : E → E → E → Prop) (x2 : E) => x1 x2) (monadLift (pure told)) (noDP person))) (pure <$> monadLift do let u ← pro indef (bookBy u)))).run ContT.eval = do let x ← indef man let z ← indef (bookBy x) pure ¬∃ (y : E), person y ∧ told y z x

In a man told nobody about a book he wrote, with the object indefinite scoping over nobody and its pronoun bound by the subject, the subject and object indefinites take the top level and nobody the second.

theorem Charlow2014.ReaderSet.no_exceptional_binding {E : Type} (man left tired : E → Prop) : (combine (fun (x : Prop) (f : Prop → Prop) => f x) (combine (fun (x : E) (f : E → Prop) => f x) (bindShift (monadLift (indef man))) (monadLift (pure left))).reset (combine (fun (x1 : Prop → Prop → Prop) (x2 : Prop) => x1 x2) (monadLift (pure fun (q p : Prop) => p ∧ q)) (combine (fun (x : E) (f : E → Prop) => f x) (monadLift pro) (monadLift (pure tired))).reset)).eval = do let x ← indef man let u ← pro pure (left x ∧ tired u)

In Reader.Set, in a man left; he was tired the indefinite's nondeterminism survives the island and its dref does not, the second sentence's pronoun still reading the input stack. Contrast Charlow2014.exceptional_binding.

theorem Charlow2014.ReaderSet.run_monadLift {E α β : Type} (m : ReaderSet E α) (k : α → ReaderSet E β) : (monadLift m).run k = fun (s : Stack E) => ⋃ x ∈ m s, k x s

A Reader.Set continuation is evaluated at the input stack, so no dref made inside a lifted program reaches it, the reckoning of (5.5.4).

theorem Charlow2014.run_monadLift {E α β : Type} (m : StateSet E α) (k : α → StateSet E β) : ContT.run (monadLift m) k = fun (s : Stack E) => ⋃ q ∈ m s, k q.1 q.2

... whereas a State.Set continuation is evaluated at the lifted program's output stack.