[Cha18]: A Modular Theory of Pronouns and Binding

Simon Charlow (2018). "A modular theory of pronouns and binding." Manuscript, Rutgers University. https://lingbuzz.net/lingbuzz/003720

Thesis

The standard [HK98] treatment of assignment-sensitivity factors into two algebraic operations (§3.1, eqs 11–12):

• ρ x := λg. x — lift assignment-independent values
• m ⊛ n := λg. m g (n g) — assignment-friendly functional application

These form an applicative functor ([McBP08]) for G a := g → a, satisfying the four laws of §3.3 (Homomorphism, Identity, Interchange, Composition). The modularization (i) keeps the lexicon maximally simple — nothing is assignment-sensitive unless it really is — and (ii) makes predicate abstraction Λᵢ categorematic (eq. 13), eliminating H&K's syncategorematic rule.

Adding a join μ m := λg. m g g (eq. 19) upgrades the structure to a monad (§4.3), enabling higher-order variables anaphoric to intensions rather than extensions — yielding immediate analyses of paycheck pronouns (Fig. 6) and binding reconstruction (Fig. 7) with the unitary pronoun semantics ⟦proᵢ⟧ := λg. gᵢ.

§3.3 shows applicative functors are already implicit in existing semantic theory: Hamblin alternative semantics is the Set applicative (eqs 14–15), and Shan & Barker's continuation-based composition is the Cont applicative (eqs 16–17). Applicatives compose (Fig. 5) — unlike monads (§4.3 end: S ∘ G is not monadic) — which §5 exploits: with type-homogeneous assignments gᵣ := ℕ → r (§5.2), the composed applicative G_e ∘ G_{g_e→e} handles paychecks without monads. §6 plays us out with variable-free semantics ([Jac99]): the same ρ/⊛ with Entity as the environment type, where composing the VF applicative with itself makes assignment-dependence "spring organically into being."

Organization (following the paper)

• §3.1–3.2 — ρ/⊛, the four laws, H&K decomposition, categorematic Λᵢ
• §3.3 — applicatives already in semantic theory: Set, Cont, composition
• §4 — μ, higher-order variables: paychecks, binding reconstruction
• §5 — typed assignments gᵣ; composed-applicative paychecks
• §6 — variable-free semantics as Reader Entity
• Bridges — Core's DenotG apparatus and Reference/Binding's Reader monad

§3.1–3.2 Getting modular: ρ and ⊛

Eqs (11)–(12): instead of treating all lexical values as trivially assignment-dependent, invoke ρ to lift any x into a constant function from assignments, and ⊛ for assignment-friendly functional application on demand. The four applicative functor laws (§3.3 table) hold definitionally for G a := g → a.

def Charlow2018.readerPure {E A : Type} (x : A) : E → A

ρ (eq. 11): lift a value into the Reader space — ρ x := λg. x.

Equations

• Charlow2018.readerPure x x✝ = x

def Charlow2018.readerAp {E A B : Type} (f : E → A → B) (x : E → A) : E → B

⊛ (eq. 12): assignment-friendly functional application — m ⊛ n := λg. m g (n g).

Equations

• Charlow2018.readerAp f x e = f e (x e)

theorem Charlow2018.reader_homomorphism {E A B : Type} (f : A → B) (x : A) : readerAp (readerPure f) (readerPure x) = readerPure (f x)

Homomorphism (§3.3): ρ f ⊛ ρ x = ρ (f x).

theorem Charlow2018.reader_identity {E A : Type} (v : E → A) : readerAp (readerPure id) v = v

Identity (§3.3): ρ(λx.x) ⊛ v = v.

theorem Charlow2018.reader_interchange {E A B : Type} (u : E → A → B) (y : A) : readerAp u (readerPure y) = readerAp (readerPure fun (f : A → B) => f y) u

Interchange (§3.3): u ⊛ ρ y = ρ(λf. f y) ⊛ u.

theorem Charlow2018.reader_composition {E A B C : Type} (u : E → B → C) (v : E → A → B) (w : E → A) : readerAp (readerAp (readerAp (readerPure Function.comp) u) v) w = readerAp u (readerAp v w)

Composition (§3.3): ρ(∘) ⊛ u ⊛ v ⊛ w = u ⊛ (v ⊛ w).

The ρ/⊛ decomposition of H&K's interpretation function

§3.1–3.2: the standard H&K interpretation function ⟦α β⟧ := λg. ⟦α⟧ g (⟦β⟧ g) decomposes into ρ (for trivially assignment-dependent lexical entries: ⟦John⟧ = ρ(j)) and ⊛ (for binary branching). This decomposition is directly visible in linglib's interp (Composition/Tree.lean): its binary case computes FA(⟦α⟧^g, ⟦β⟧^g), which is applyG ⟦α⟧ ⟦β⟧ evaluated at g.

theorem Charlow2018.hk_decomposition {E W : Type} {σ τ : Intensional.Ty} (f : Intensional.Variables.DenotG E W (σ ⇒ τ)) (x : Intensional.Variables.DenotG E W σ) : Intensional.Variables.applyG f x = fun (g : Core.Assignment E) => f g (x g)

H&K's interpretation function ⟦α β⟧ = λg. ⟦α⟧ g (⟦β⟧ g) is definitionally applyG: ⊛ is ⟦·⟧ restricted to binary branching.

theorem Charlow2018.hk_lexical_lift {E W : Type} {σ : Intensional.Ty} (d : Intensional.Denot E W σ) : Intensional.Variables.constDenot d = fun (x : Core.Assignment E) => d

Non-pronominal entries in H&K are trivially assignment-dependent: ⟦John⟧ := λg. j. This is exactly ρ(j).

theorem Charlow2018.rho_ap_reduces {E W : Type} {σ τ : Intensional.Ty} (f : Intensional.Denot E W (σ ⇒ τ)) (x : Intensional.Denot E W σ) : Intensional.Variables.applyG (Intensional.Variables.constDenot f) (Intensional.Variables.constDenot x) = Intensional.Variables.constDenot (f x)

Composing two ρ-lifted entries via ⊛ yields ρ of the composition.

theorem Charlow2018.constDenot_is_readerPure {E W : Type} {σ : Intensional.Ty} (d : Intensional.Denot E W σ) : Intensional.Variables.constDenot d = readerPure d

Core's constDenot IS the paper's ρ.

theorem Charlow2018.applyG_is_readerAp {E W : Type} {σ τ : Intensional.Ty} (f : Intensional.Variables.DenotG E W (σ ⇒ τ)) (x : Intensional.Variables.DenotG E W σ) : Intensional.Variables.applyG f x = readerAp f x

Core's applyG IS the paper's ⊛.

Λᵢ: categorematic predicate abstraction

Eq. (13): Λᵢ := λf. λg. λx. f g^{i→x}. In H&K, predicate abstraction is a syncategorematic rule; with ρ/⊛ there is no grammatical default about how assignments get passed around, so Λᵢ becomes a categorematic operation — linglib's lambdaAbsG.

theorem Charlow2018.lambda_pronoun {E W : Type} (n : ℕ) (g : Core.Assignment E) (x : E) : Intensional.Variables.lambdaAbsG n (Intensional.Variables.interpPronoun n) g x = x

Λᵢ applied to a pronoun recovers the identity function: Λₙ(proₙ) = λg λx. x.

theorem Charlow2018.lambda_rho_ap_pronoun {E W : Type} (n : ℕ) (left : Intensional.Denot E W (Intensional.Ty.e ⇒ Intensional.Ty.t)) (g : Core.Assignment E) (x : E) : Intensional.Variables.lambdaAbsG n (Intensional.Variables.applyG (Intensional.Variables.constDenot left) (Intensional.Variables.interpPronoun n)) g x = left x

Λᵢ applied to ρ(left) ⊛ proₙ yields ρ(left): Λₙ(ρ(left) ⊛ proₙ) = λg λx. left(x) = ρ(left).

§3.3 Applicatives already in semantic theory

"Applicative functors can be factored out of a great deal of existing semantic theory." Two examples, then the composition property.

The Set applicative (eqs 14–15)

Hamblin alternative semantics restated as an applicative for sets S a := a → t: ρ x := {x} and m ⊛ n := {f x | f ∈ m, x ∈ n}. Operations are mathlib's Set pure/<*>; the application-form simp lemmas serve consumers that treat Set A = A → Prop. The monadic extension of this applicative — and why the monad matters for exceptional scope — is [Cha20], formalized in Studies/Charlow2020.lean.

def Charlow2018.setPure {A : Type} (x : A) : Set A

Set ρ (eq. 14): the singleton {x}. Mathlib's Set applicative pure.

Equations

• Charlow2018.setPure x = pure x

def Charlow2018.setAp {A B : Type} (m : Set (A → B)) (n : Set A) : Set B

Set ⊛ (eq. 15): pointwise application across sets, {f x | f ∈ m, x ∈ n}. Mathlib's Set applicative <*> (Set.seq).

Equations

• Charlow2018.setAp m n = m <*> n

@[simp]

theorem Charlow2018.mem_setPure {A : Type} (x y : A) : y ∈ setPure x ↔ y = x

@[simp]

theorem Charlow2018.setPure_apply {A : Type} (x y : A) : setPure x y ↔ y = x

Application-form characterisation of setPure (consumers treat Set A = A → Prop).

@[simp]

theorem Charlow2018.mem_setAp {A B : Type} (m : Set (A → B)) (n : Set A) (b : B) : b ∈ setAp m n ↔ ∃ f ∈ m, ∃ x ∈ n, f x = b

@[simp]

theorem Charlow2018.setAp_apply {A B : Type} (m : Set (A → B)) (n : Set A) (b : B) : setAp m n b ↔ ∃ (f : A → B), m f ∧ ∃ (x : A), n x ∧ f x = b

Application-form characterisation of setAp.

theorem Charlow2018.set_homomorphism {A B : Type} (f : A → B) (x : A) : setAp (setPure f) (setPure x) = setPure (f x)

Homomorphism for Set: {f} ⊛ {x} = {f x}.

theorem Charlow2018.set_identity {A : Type} (v : Set A) : setAp (setPure id) v = v

Identity for Set: {id} ⊛ v = v.

theorem Charlow2018.set_interchange {A B : Type} (u : Set (A → B)) (y : A) : setAp u (setPure y) = setAp (setPure fun (f : A → B) => f y) u

Interchange for Set: u ⊛ {y} = {(fun f => f y)} ⊛ u.

theorem Charlow2018.set_composition {A B C : Type} (u : Set (B → C)) (v : Set (A → B)) (w : Set A) : setAp (setAp (setAp (setPure Function.comp) u) v) w = setAp u (setAp v w)

Composition for Set: {∘} ⊛ u ⊛ v ⊛ w = u ⊛ (v ⊛ w).

The Cont applicative (eqs 16–17)

Shan & Barker's continuation-based composition is built on two combinators (Lift/Scope) that directly instantiate the applicative functor for continuations Cᵣ a := (a → r) → r. The operations are definitionally Cont.pure and the <*> derived from Composition/Continuation.lean's monad instance.

theorem Charlow2018.cont_pure_eq {R A : Type} (x : A) : (fun (κ : A → R) => κ x) = Semantics.Composition.Continuation.Cont.pure x

Eq. (16): ρ x := λκ. κ x = Cont.pure.

theorem Charlow2018.cont_ap_eq {R A B : Type} (m : Semantics.Composition.Continuation.Cont R (A → B)) (n : Semantics.Composition.Continuation.Cont R A) : (fun (κ : B → R) => m fun (f : A → B) => n fun (x : A) => κ (f x)) = m.bind fun (f : A → B) => Semantics.Composition.Continuation.Cont.map f n

Eq. (17): m ⊛ n := λκ. m(λf. n(λx. κ(f x))) = Cont <*>.

Composed applicatives (Fig. 5)

Given two applicative type constructors F and G, their composition F ∘ G is applicative. For Reader E₁ ∘ Reader E₂:

ρ_{F∘G}(x) = λe₁ λe₂. x
(m ⊛_{F∘G} n)(e₁)(e₂) = m e₁ e₂ (n e₁ e₂)

This closure guarantees modularity: any two applicative-based analyses combine without additional machinery. G ∘ S yields assignment-dependent alternative sets; S ∘ G alternative assignment-dependent meanings; G ∘ G doubly assignment-dependent meanings (the §5 paycheck composite). Monads, by contrast, are NOT closed under composition (§4.3 end: S ∘ G is not monadic).

def Charlow2018.composedPure {E₁ E₂ A : Type} (x : A) : E₁ → E₂ → A

Composed ρ for Reader E₁ ∘ Reader E₂.

Equations

• Charlow2018.composedPure x x✝¹ x✝ = x

def Charlow2018.composedAp {E₁ E₂ A B : Type} (f : E₁ → E₂ → A → B) (x : E₁ → E₂ → A) : E₁ → E₂ → B

Composed ⊛ for Reader E₁ ∘ Reader E₂.

Equations

• Charlow2018.composedAp f x e₁ e₂ = f e₁ e₂ (x e₁ e₂)

theorem Charlow2018.composed_homomorphism {E₁ E₂ A B : Type} (f : A → B) (x : A) : composedAp (composedPure f) (composedPure x) = composedPure (f x)

theorem Charlow2018.composed_identity {E₁ E₂ A : Type} (v : E₁ → E₂ → A) : composedAp (composedPure id) v = v

theorem Charlow2018.composed_interchange {E₁ E₂ A B : Type} (u : E₁ → E₂ → A → B) (y : A) : composedAp u (composedPure y) = composedAp (composedPure fun (f : A → B) => f y) u

theorem Charlow2018.composed_composition {E₁ E₂ A B C : Type} (u : E₁ → E₂ → B → C) (v : E₁ → E₂ → A → B) (w : E₁ → E₂ → A) : composedAp (composedAp (composedAp (composedPure Function.comp) u) v) w = composedAp u (composedAp v w)

§4 Getting higher-order: paychecks and reconstruction

Higher-order variables (eq. 18: pro ::= g → e | g → pro) are anaphoric to intensions rather than extensions. The flattener μ (eq. 19: μ m := λg. m g g) converts a higher-order meaning to a garden-variety one. ρ, ⊛, and μ together form a monad (§4.3) — the Reader monad.

The Core.Assignment E = Nat → E type can only store entities, not intensions; §5.1 proposes type-homogeneous assignments gᵣ := ℕ → r to fix this (next section). Here we show the paycheck truth conditions using externally-provided intensions.

def Charlow2018.momIntension {E W : Type} (mom : E → E) (n : ℕ) : Intensional.Variables.DenotG E W Intensional.Ty.e

The intension ⟦his₀ mom⟧ = ρ(mom) ⊛ pro₀ = λg. mom(g₀).

Equations

• Charlow2018.momIntension mom n g = mom (g n)

theorem Charlow2018.momIntension_eq_rho_ap_pro {E W : Type} (mom : E → E) (n : ℕ) : momIntension mom n = Intensional.Variables.applyG (Intensional.Variables.constDenot mom) (Intensional.Variables.interpPronoun n)

momIntension is compositionally derived: ρ(mom) ⊛ proₙ.

theorem Charlow2018.paycheck_truth_conditions {E W : Type} (mom : E → E) (likes : Intensional.Denot E W (Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t)) (bill : E) (n : ℕ) (g : Core.Assignment E) : Intensional.Variables.applyG (Intensional.Variables.applyG (Intensional.Variables.constDenot likes) (momIntension mom n)) (Intensional.Variables.constDenot bill) g = likes (mom (g n)) bill

Paycheck truth conditions: likes(mom(g n), bill).

theorem Charlow2018.paycheck_reading {E W : Type} (mom : E → E) (likes : Intensional.Denot E W (Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t)) (bill : E) (n : ℕ) (g : Core.Assignment E) (h : g n = bill) : Intensional.Variables.applyG (Intensional.Variables.applyG (Intensional.Variables.constDenot likes) (momIntension mom n)) (Intensional.Variables.constDenot bill) g = likes (mom bill) bill

When g(n) = bill, the paycheck pronoun denotes Bill's mom.

Binding reconstruction via higher-order trace + Λᵢ (Fig. 7)

"[His₁ mom]ⱼ, every boy₁ likes tⱼ." The bound pronoun his₁ is inside a fronted constituent syntactically higher than the binder every boy₁. The analysis uses Λ₁ to abstract over the quantifier variable, producing the reconstructed predicate λx. likes(mom(x), x) without LF c-command — and without triggering Weak Crossover, since the bound-into expression originates lower than the binder.

theorem Charlow2018.reconstruction_predicate {E W : Type} (mom : E → E) (likes : Intensional.Denot E W (Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t)) (n : ℕ) (g : Core.Assignment E) (x : E) : Intensional.Variables.lambdaAbsG n (Intensional.Variables.applyG (Intensional.Variables.applyG (Intensional.Variables.constDenot likes) (momIntension mom n)) (Intensional.Variables.interpPronoun n)) g x = likes (mom x) x

The reconstructed VP predicate: λx. likes(mom(x), x).

theorem Charlow2018.reconstruction_independent {E W : Type} (mom : E → E) (likes : Intensional.Denot E W (Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t)) (n : ℕ) (g₁ g₂ : Core.Assignment E) : Intensional.Variables.lambdaAbsG n (Intensional.Variables.applyG (Intensional.Variables.applyG (Intensional.Variables.constDenot likes) (momIntension mom n)) (Intensional.Variables.interpPronoun n)) g₁ = Intensional.Variables.lambdaAbsG n (Intensional.Variables.applyG (Intensional.Variables.applyG (Intensional.Variables.constDenot likes) (momIntension mom n)) (Intensional.Variables.interpPronoun n)) g₂

The reconstruction predicate is assignment-independent.

§5 Stepping back, to applicatives: typed assignments

§5.1–5.2: type-homogeneous assignments gᵣ := ℕ → r avoid the inconsistency worries of a single polymorphic assignment type (Muskens 1995). Each type r gets its own assignment sort: gₑ maps indices to individuals, g_{gₑ→e} to individual concepts. The composed applicative Gₑ ∘ G_{gₑ→e} then handles paycheck pronouns without monadic μ: the paycheck pronoun reads an intension from the intension-assignment and evaluates it at the entity-assignment. "We needn't exploit the extra power of monads to treat paychecks and reconstruction; the only price is needing multiple assignments to extract propositional content from certain utterances."

@[reducible, inline]

abbrev Charlow2018.TypedAssignment (r : Type) : Type

Type-homogeneous assignment over carrier r (§5.2: gᵣ := ℕ → r). Equal to Core.Assignment r; aliased to read naturally in the paycheck composition where r ranges over both entity and intension carriers within one derivation.

Equations

• Charlow2018.TypedAssignment r = Core.Assignment r

theorem Charlow2018.typed_paycheck {E : Type} (likes : E → E → Bool) (mom : E → E) (bill : E) (j : ℕ) (gᵢ : TypedAssignment (TypedAssignment E → E)) (gₑ : TypedAssignment E) (h_intension : gᵢ j = fun (h : TypedAssignment E) => mom (h 0)) (h_bill : gₑ 0 = bill) : composedAp (composedAp (composedPure likes) fun (gᵢ' : TypedAssignment (TypedAssignment E → E)) (gₑ' : TypedAssignment E) => gᵢ' j gₑ') (composedPure bill) gᵢ gₑ = likes (mom bill) bill

Self-contained paycheck derivation via composed Gₑ ∘ G_{gₑ→e}.

The intension-assignment gᵢ maps index j to the intension λh. mom(h 0) (= "his₀ mom"). The entity-assignment gₑ maps index 0 to Bill. The paycheck pronoun herⱼ reads from gᵢ and evaluates at gₑ, yielding mom(bill) — "virtually identical to what we monadically derived in Figure 6, but depending on two assignments rather than one."

theorem Charlow2018.typed_intension_is_rho_ap_pro {E : Type} (mom : E → E) : (readerAp (readerPure mom) fun (h : TypedAssignment E) => h 0) = fun (h : TypedAssignment E) => mom (h 0)

The intension λh. mom(h 0) is compositionally derived as ρ(mom) ⊛ pro₀ in the inner Gₑ applicative.

theorem Charlow2018.composed_paycheck {E : Type} (likes : E → E → Bool) (mom : E → E) (b : E) (g h : ℕ → E) (j : ℕ) (h_stored : g j = mom (h 0)) : composedAp (composedAp (composedPure likes) fun (g' x : ℕ → E) => g' j) (composedPure b) g h = likes (mom (h 0)) b

G ∘ G paycheck reading with Core.Assignment sorts: the doubly assignment-dependent meaning λg λh. likes(g₁ h)(b) depends on two assignments.

§6 A bit of variable-free semantics to play us out

[Jac99]'s variable-free semantics treats pronouns as identity functions ⟦she⟧ := λx. x (type e → e). The composition apparatus is structurally identical to the assignment-sensitive version — ρ and ⊛ with Entity as the environment type instead of assignments ("we've only replaced g-dependent e's with e-dependent e's").

The striking observation: composing the VF applicative with itself (Reader E ∘ Reader E) yields two-pronoun readings where the pronouns resolve independently — uncurrying the result produces assignment-dependence "organically."

def Charlow2018.vfPronoun {E : Type} : E → E

VF pronoun: the identity function ⟦she⟧ := λx. x.

Equations

• Charlow2018.vfPronoun = id

theorem Charlow2018.vf_she_left {E : Type} (left : E → Bool) : readerAp (readerPure left) vfPronoun = left

"She left" in VF: ρ(left) ⊛ she = left.

theorem Charlow2018.vf_she_saw_her_single {E : Type} (saw : E → E → Bool) : readerAp (readerAp (readerPure saw) vfPronoun) vfPronoun = fun (e : E) => saw e e

"She saw her" with a single entity parameter: both pronouns resolve to the same entity, yielding λe. saw e e (reflexive reading).

theorem Charlow2018.vf_she_saw_her_composed {E : Type} (saw : E → E → Bool) : (composedAp (composedAp (composedPure saw) fun (x e₂ : E) => e₂) fun (e₁ x : E) => e₁) = fun (e₁ e₂ : E) => saw e₂ e₁

"She saw her" with the composed applicative (two entity parameters): the two pronouns resolve independently, yielding λx λy. saw y x. Assignment-dependence "springs organically into being" from uncurrying.

Bridge to Reference/Binding.lean's Reader monad

The paper's operations are instantiations of the Reader monad from Binding.lean:

• constDenot d = Reader pure at Core.Assignment E
• applyG f x = Reader <*> at Core.Assignment E
• denotGJoin (μ) = the W combinator
• VF readerPure = Reader pure at Entity

theorem Charlow2018.constDenot_is_reader_pure {E W : Type} {σ : Intensional.Ty} (d : Intensional.Denot E W σ) : Intensional.Variables.constDenot d = pure d

constDenot is the Reader monad's pure.

theorem Charlow2018.readerPure_is_reader_monad_pure {E A : Type} (x : A) : readerPure x = pure x

VF readerPure is also the Reader monad's pure.

theorem Charlow2018.denotGJoin_is_W {E A : Type} (f : Core.Assignment E → Core.Assignment E → A) : Intensional.Variables.denotGJoin f = Semantics.Reference.Binding.W f

denotGJoin (the paper's μ, eq. 19) is the W (duplicator) combinator from Binding.lean.