Charlow 2018: A Modular Theory of Pronouns and Binding #
@cite{charlow-2018}
@cite{charlow-2018} factors the standard @cite{heim-kratzer-1998} treatment of assignment-sensitivity into two algebraic operations that form an applicative functor (the Reader applicative, @cite{mcbride-paterson-2008}):
ρ x := λg. x— lift assignment-independent values =constDenotm ⊛ n := λg. m g (n g)— assignment-sensitive FA =applyG
Adding a join (μ) operation μ m := λg. m g g = denotGJoin upgrades
the structure to a monad, enabling higher-order variables that are
anaphoric to intensions rather than extensions. This yields immediate
analyses of:
- Paycheck pronouns: "John hates his mom. Bill likes her" → her = Bill's mom
- Binding reconstruction: "[His mom], every boy likes t" → bound reading without c-command
The same ρ/⊛ combinators, instantiated with entities instead of assignments,
recover @cite{jacobson-1999}'s variable-free semantics (§6). The generic
applicative operations (readerPure, readerAp, composedPure, composedAp,
vfPronoun) and their laws live in Composition/Applicative.lean; this file
bridges them to the Montague Model/DenotG infrastructure.
Key results #
constDenot/applyGsatisfy the four applicative functor laws (Theories/Semantics/Montague/Variables.lean)denotGJoinsatisfies the monad laws (ibid.)- H&K's
⟦·⟧decomposes as ρ + ⊛ (hk_decomposition) - Λᵢ as a categorematic operation (
lambdaAbsG) - Higher-order pronouns + μ yield paycheck truth conditions
- Binding reconstruction predicate:
λx. likes(mom(x), x) - Composed applicatives are closed under composition (§3.3)
- Variable-free equivalence: same combinators with
Entityas environment - Typed assignments make the paycheck derivation self-contained (§5)
The ρ/⊛ decomposition of H&K's interpretation function #
@cite{charlow-2018} §3.1–3.2: the standard H&K interpretation function
⟦α β⟧ := λg. ⟦α⟧ g (⟦β⟧ g) decomposes into two
independent operations:
- ρ lifts assignment-independent values:
⟦John⟧ = ρ(j) - ⊛ composes assignment-dependent meanings:
⟦α β⟧ = ⟦α⟧ ⊛ ⟦β⟧
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.
H&K's interpretation function ⟦α β⟧ = λg. ⟦α⟧ g (⟦β⟧ g) is
definitionally applyG: ⊛ is ⟦·⟧ restricted to binary branching.
Non-pronominal entries in H&K are trivially assignment-dependent:
⟦John⟧ := λg. j. This is exactly ρ(j).
Composing two ρ-lifted entries via ⊛ yields ρ of the composition.
constDenot IS readerPure (from Applicative.lean).
applyG IS readerAp (from Applicative.lean).
Λᵢ: categorematic predicate abstraction #
@cite{charlow-2018} eq (13): Λᵢ := λf. λg. λx. f g^{i→x}
In H&K, predicate abstraction is a syncategorematic rule. With ρ/⊛,
Λᵢ becomes a categorematic operation — lambdaAbsG.
Λᵢ applied to a pronoun recovers the identity function:
Λₙ(proₙ) = λg λx. x.
Λᵢ applied to ρ(left) ⊛ proₙ yields ρ(left):
Λₙ(ρ(left) ⊛ proₙ) = λg λx. left(x) = ρ(left).
Paycheck pronouns via higher-order variables and μ #
@cite{charlow-2018} §4.1–4.2: paycheck pronouns are anaphoric to
intensions rather than extensions. The key mechanism is
higher-order variables + the monadic join μ (denotGJoin).
The Assignment m = Nat → m.Entity type can only store entities, not
intensions. @cite{charlow-2018} §5.1 proposes type-homogeneous assignments
gᵣ := ℕ → r to fix this — see typed_paycheck in Applicative.lean
for the self-contained derivation. Here we show the paycheck truth
conditions using externally-provided intensions.
The intension ⟦his₀ mom⟧ = ρ(mom) ⊛ pro₀ = λg. mom(g₀).
Equations
- Phenomena.Anaphora.Studies.Charlow2018.momIntension mom n g = mom (g n)
Instances For
momIntension is compositionally derived: ρ(mom) ⊛ proₙ.
Paycheck truth conditions: likes(mom(g n), bill).
When g(n) = bill, the paycheck pronoun denotes Bill's mom.
Bridge to DonkeyAnaphora.paycheckSentence: the paycheck datum
records a bound reading — exactly what intension retrieval predicts.
Binding reconstruction via higher-order trace + Λᵢ #
@cite{charlow-2018} §4.2, Fig 7: "[His₁ mom]ⱼ, every boy₁ likes tⱼ."
The bound pronoun his₁ is inside a fronted constituent that is
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 c-command.
The reconstructed VP predicate: λx. likes(mom(x), x).
The reconstruction predicate is assignment-independent.
Composed applicative: G ∘ G paycheck #
Generic composed applicative operations and all four laws live in
Composition/Applicative.lean. Here we bridge to the paper's
specific paycheck example using entities.
G ∘ G paycheck reading: doubly assignment-dependent meaning
λg λh. likes(g₁ h)(b) depends on two assignments.
Connection to Reference/Binding.lean's Reader monad #
@cite{charlow-2018}'s operations are instantiations of the Reader monad
from Binding.lean:
constDenot d= Reader pure atAssignment mapplyG f x= Reader<*>atAssignment mdenotGJoin= the W combinator (Binding.lean)- VF
readerPure= Reader pure at Entity
constDenot is the Reader monad's pure.
VF readerPure is also the Reader monad's pure.
denotGJoin is the W (duplicator) combinator from Binding.lean.