Effect-Driven Interpretation

@cite{bumford-charlow-2024}

@cite{bumford-charlow-2024} propose that diverse semantic phenomena — scope, binding, conventional implicatures, indeterminacy — are all instances of algebraic effects within the Functor → Applicative → Monad hierarchy. The grammar's composition rules are built from meta-combinators (F̄, F̃, A, J) that systematically lift basic modes of combination to work in the presence of effects.

This file formalizes the core of their framework and bridges it to existing linglib infrastructure:

Effect	Paper name	Type	linglib type
Scope	C	(α → ρ) → ρ	Cont R A
CI / supplementation	W	α × List P	Writer P A
Input (binding)	R	ι → α	Reader (Binding.lean)
Output (antecedents)	W	α × ι	Prod
Indeterminacy	S	{α}	α → Prop (SetMonad.lean)

Organization

• §1 Lean typeclass instances for Cont and Writer
• §2 Meta-combinators: F̄, F̃, A, J (the paper's core contribution)
• §3 Generalized Application and hierarchy theorems
• §4 The W ⊣ R adjunction for binding
• §5 Effect operations and handlers
• §6 Bridge theorems
• §7 General scope agreement (Cont ≡ GQ application)
• §8 Three-way binding unification (denotGJoin = W = adj_ε)

Coverage

Of the 9 meta-combinators in Figure 10, this file formalizes 5: F̄ (Map Left), F̃ (Map Right), A (Structured App), J (Join), C (Co-unit).

Omitted: Ū/Ũ (Unit Left/Right) are trivial wrappers around pure; ⊿̄/⊿̃ (Eject Left/Right) require the Υ isomorphism from §5.3.2 (Kleisli arrow repackaging), which is not yet formalized.

§1 Typeclass instances for existing types

Register Functor, Applicative, and Monad instances for linglib's Cont R and Writer P types, delegating to existing operations.

Note: Cont R A := (A → R) → R requires R : Type (not universe-polymorphic) for Lean's Monad class.

instance Semantics.Composition.Effects.instFunctorCont {R : Type} : Functor (Core.Continuation.Cont R)

Equations

• Semantics.Composition.Effects.instFunctorCont = { map := fun {α β : Type ?u.14} => Core.Continuation.Cont.map }

instance Semantics.Composition.Effects.instPureCont {R : Type} : Pure (Core.Continuation.Cont R)

Equations

• Semantics.Composition.Effects.instPureCont = { pure := fun {α : Type ?u.9} => Core.Continuation.Cont.pure }

instance Semantics.Composition.Effects.instBindCont {R : Type} : Bind (Core.Continuation.Cont R)

Equations

• Semantics.Composition.Effects.instBindCont = { bind := fun {α β : Type ?u.10} => Core.Continuation.Cont.bind }

instance Semantics.Composition.Effects.instSeqCont {R : Type} : Seq (Core.Continuation.Cont R)

Equations

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

instance Semantics.Composition.Effects.instMonadCont {R : Type} : Monad (Core.Continuation.Cont R)

Equations

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

instance Semantics.Composition.Effects.instLawfulMonadCont {R : Type} : LawfulMonad (Core.Continuation.Cont R)

instance Semantics.Composition.Effects.instFunctorWriter {P : Type} : Functor (WriterMonad.Writer P)

Equations

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

instance Semantics.Composition.Effects.instPureWriter {P : Type} : Pure (WriterMonad.Writer P)

Equations

• Semantics.Composition.Effects.instPureWriter = { pure := fun {α : Type ?u.10} (a : α) => Semantics.Composition.WriterMonad.Writer.pure a }

instance Semantics.Composition.Effects.instBindWriter {P : Type} : Bind (WriterMonad.Writer P)

Equations

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

instance Semantics.Composition.Effects.instSeqWriter {P : Type} : Seq (WriterMonad.Writer P)

Equations

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

instance Semantics.Composition.Effects.instMonadWriter {P : Type} : Monad (WriterMonad.Writer P)

Equations

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

instance Semantics.Composition.Effects.instLawfulFunctorWriter {P : Type} : LawfulFunctor (WriterMonad.Writer P)

instance Semantics.Composition.Effects.instLawfulApplicativeWriter {P : Type} : LawfulApplicative (WriterMonad.Writer P)

instance Semantics.Composition.Effects.instLawfulMonadWriter {P : Type} : LawfulMonad (WriterMonad.Writer P)

§2 Meta-combinators

central contribution: meta-combinators that build higher-order modes of combination from basic ones. Given any binary combinator (∗) :: σ → τ → ω (e.g., function application), these produce new combinators that work when one or both daughters carry effects.

Meta-combinator	Effectful daughters	Hierarchy	Paper ref
F̄ (Map Left)	left	Functor	Figure 4
F̃ (Map Right)	right	Functor	Figure 4
A (Structured App)	both	Applicative	Figure 7
J (Join)	both + nested	Monad	Figure 8
C (Co-unit)	adjoint pair	Adjunction	Figure 10

F̄, F̃, A, and J are parameterized over any effect type Σ for which the appropriate typeclass (Functor/Applicative/Monad) holds. C is defined in §4, parameterized over an adjunction (specifically W ⊣ R).

def Semantics.Composition.Effects.mapL {σ τ ω : Type} {F : Type → Type} [Functor F] (star : σ → τ → ω) (e₁ : F σ) (e₂ : τ) : F ω

F̄ (Map Left): lift a binary combinator when the left daughter carries an effect.

eq. 2.17a, Figure 4: F̄(∗) E₁ E₂ := (λa. a ∗ E₂) • E₁

Equations

• Semantics.Composition.Effects.mapL star e₁ e₂ = (fun (a : σ) => star a e₂) <$> e₁

def Semantics.Composition.Effects.mapR {σ τ ω : Type} {F : Type → Type} [Functor F] (star : σ → τ → ω) (e₁ : σ) (e₂ : F τ) : F ω

F̃ (Map Right): lift a binary combinator when the right daughter carries an effect.

eq. 2.17b, Figure 4: F̃(∗) E₁ E₂ := (λb. E₁ ∗ b) • E₂

Equations

• Semantics.Composition.Effects.mapR star e₁ e₂ = (fun (b : τ) => star e₁ b) <$> e₂

def Semantics.Composition.Effects.structuredApp {σ τ ω : Type} {F : Type → Type} [Applicative F] (star : σ → τ → ω) (e₁ : F σ) (e₂ : F τ) : F ω

A (Structured Application): lift when both daughters carry effects of the same type, merging them into a single layer.

eq. 3.10, Figure 7: A(∗) E₁ E₂ := η(∗) ⊛ E₁ ⊛ E₂

Equations

• Semantics.Composition.Effects.structuredApp star e₁ e₂ = pure star <*> e₁ <*> e₂

def Semantics.Composition.Effects.joinMode {σ τ ω : Type} {F : Type → Type} [Monad F] (star : σ → τ → F ω) (e₁ : F σ) (e₂ : F τ) : F ω

J (Join): monadic flattening for when the basic combinator produces a nested effect F(F ω).

eq. 4.22, Figure 8: J(∗) E₁ E₂ := μ(E₁ ∗ E₂) where μ is monadic join.

Equations

• Semantics.Composition.Effects.joinMode star e₁ e₂ = Semantics.Composition.Effects.structuredApp star e₁ e₂ >>= id

@[reducible]

def Semantics.Composition.Effects.fa' {α β : Type} (f : α → β) (x : α) : β

Forward application: f > x := f x.

Equations

• Semantics.Composition.Effects.fa' f x = f x

@[reducible]

def Semantics.Composition.Effects.ba' {α β : Type} (x : α) (f : α → β) : β

Backward application: x < f := f x.

Equations

• Semantics.Composition.Effects.ba' x f = f x

theorem Semantics.Composition.Effects.mapR_fa_eq_fmap {α β : Type} {F : Type → Type} [Functor F] (f : α → β) (e₂ : F α) : mapR fa' f e₂ = f <$> e₂

F̃(>) = fmap. Map Right applied to forward application is functorial map — the forward mapping operation (•>).

eq. 2.18.

theorem Semantics.Composition.Effects.mapL_ba_eq_fmap {α β : Type} {F : Type → Type} [Functor F] (e₁ : F α) (f : α → β) : mapL ba' e₁ f = f <$> e₁

F̄(<) = fmap. Map Left applied to backward application is functorial map — the backward mapping operation (•<).

eq. 2.18.

theorem Semantics.Composition.Effects.fmap_eq_pure_ap {F : Type → Type} [Applicative F] [LawfulApplicative F] {α β : Type} (f : α → β) (m : F α) : f <$> m = pure f <*> m

Eq. 3.6: (•) = η + (⊛). The functorial map decomposes as pure (η) the function, then applicatively sequence (⊛).

eq. 3.6: k • m := η k ⊛ m

theorem Semantics.Composition.Effects.structuredApp_pure_left {σ τ ω : Type} {F : Type → Type} [Applicative F] [LawfulApplicative F] (star : σ → τ → ω) (a : σ) (e₂ : F τ) : structuredApp star (pure a) e₂ = mapR star a e₂

Structured Application with a pure left reduces to Map Right: A(∗)(η a)(E₂) = F̃(∗)(a)(E₂).

Follows from the Homomorphism and Identity laws for applicatives (eq. 3.4).

§3 Generalized Application and hierarchy theorems

The meta-combinators instantiated to forward application (>) yield the familiar hierarchy of composition rules:

• FA: ordinary function application (the identity functor, no effects)
• Functorial map: pure function + effectful argument = F̃(>)
• Applicative ap: both effectful = A(>)
• Monadic bind: sequenced effects

H&K's FA is the base case — the identity functor applied to ordinary (effect-free) meanings.

def Semantics.Composition.Effects.fApp {α β : Type} {F : Type → Type} [Functor F] (f : α → β) (ma : F α) : F β

Functorial application: pure function, effectful argument.

This is the (•) map operation from eq. 2.3, with the forward variant (•>) from Figure 3.

Equations

• Semantics.Composition.Effects.fApp f ma = f <$> ma

def Semantics.Composition.Effects.aApp {α β : Type} {F : Type → Type} [Applicative F] (mf : F (α → β)) (ma : F α) : F β

Applicative application: both function and argument effectful.

This is (⊛) from eq. 3.3 — the applicative functor's sequencing operation.

Equations

• Semantics.Composition.Effects.aApp mf ma = mf <*> ma

def Semantics.Composition.Effects.mApp {α β : Type} {F : Type → Type} [Monad F] (mf : F (α → β)) (ma : F α) : F β

Monadic application: both effectful, with sequencing.

Enabled by (≫=) from Ch. 4. Every monad determines an applicative via eq. 4.19a: F ⊛ X = F ≫= λf. f • X.

Equations

• Semantics.Composition.Effects.mApp mf ma = do let f ← mf f <$> ma

theorem Semantics.Composition.Effects.fApp_id_is_fa {α β : Type} (f : α → β) (a : α) : fApp f a = f a

FA is functorial application for the identity functor.

theorem Semantics.Composition.Effects.mApp_eq_aApp {α β : Type} {F : Type → Type} [Monad F] [LawfulMonad F] (mf : F (α → β)) (ma : F α) : mApp mf ma = aApp mf ma

For lawful monads, monadic application agrees with applicative.

theorem Semantics.Composition.Effects.aApp_pure_left {α β : Type} {F : Type → Type} [Applicative F] [LawfulApplicative F] (f : α → β) (ma : F α) : aApp (pure f) ma = fApp f ma

Applicative application with pure f reduces to functorial map.

theorem Semantics.Composition.Effects.aApp_eq_structuredApp_fa {α β : Type} {F : Type → Type} [Applicative F] [LawfulApplicative F] (mf : F (α → β)) (ma : F α) : aApp mf ma = structuredApp fa' mf ma

Applicative application = Structured Application applied to FA.

(⊛) is A(>) — the meta-combinator A instantiated to forward application (eq. 3.10).

§4 The W ⊣ R adjunction for binding

§5.1 proposes that binding arises from an adjunction between the output effect W (= product) and the input effect R (= reader). The adjunction W ⊣ R says that functions out of pairs α × ι → β are isomorphic to curried functions α → ι → β — this is just currying.

The co-unit ε of this adjunction — which takes a pair ⟨f, x⟩ and applies f to x — IS the binding mechanism. When an antecedent stores itself via ▷(x) = ⟨x, x⟩ and the sentence body uses the bound variable, the co-unit ε yields the W combinator W κ x = κ x x from Binding.lean.

Note: the paper's W (product) is distinct from linglib's Writer P A (accumulating list log). The product W models single-referent storage; the Writer models CI accumulation.

def Semantics.Composition.Effects.Φ {ι α β : Type} (c : α × ι → β) (a : α) (x : ι) : β

Φ (currying): convert from uncurried to curried form.

eq. 5.3: Φ := λcaλx. c ⟨a, x⟩

Equations

• Semantics.Composition.Effects.Φ c a x = c (a, x)

def Semantics.Composition.Effects.Ψ {ι α β : Type} (k : α → ι → β) (p : α × ι) : β

Ψ (uncurrying): convert from curried to uncurried form.

eq. 5.3: Ψ := λk⟨a, x⟩. k a x

Equations

• Semantics.Composition.Effects.Ψ k p = k p.1 p.2

theorem Semantics.Composition.Effects.Φ_Ψ_id {ι α β : Type} (k : α → ι → β) : Φ (Ψ k) = k

Φ and Ψ are inverses (curry-uncurry round-trip).

theorem Semantics.Composition.Effects.Ψ_Φ_id {ι α β : Type} (c : α × ι → β) : Ψ (Φ c) = c

Ψ and Φ are inverses (uncurry-curry round-trip).

def Semantics.Composition.Effects.adj_η {ι α : Type} (a : α) (x : ι) : α × ι

η (unit) of W ⊣ R: η a x = ⟨a, x⟩.

eq. 5.4: η := Φ id

Equations

• Semantics.Composition.Effects.adj_η a x = (a, x)

def Semantics.Composition.Effects.adj_ε {ι α : Type} (p : (ι → α) × ι) : α

ε (co-unit) of W ⊣ R: ε ⟨f, x⟩ = f x.

eq. 5.4: ε := Ψ id

The co-unit extracts the value by applying the stored function to the stored referent — this IS binding resolution.

Equations

• Semantics.Composition.Effects.adj_ε p = p.1 p.2

theorem Semantics.Composition.Effects.adj_η_eq {ι α : Type} : adj_η = Φ id

η = Φ(id)

theorem Semantics.Composition.Effects.adj_ε_eq {ι α : Type} : adj_ε = Ψ id

ε = Ψ(id)

theorem Semantics.Composition.Effects.adj_counit_yields_W {ι β : Type} (κ : ι → ι → β) (x : ι) : adj_ε (κ x, x) = Reference.Binding.W κ x

The co-unit applied to reflexive binding yields the W combinator.

When an antecedent x stores itself (via ▷(x) = ⟨x, x⟩) and the sentence body κ has been partially applied to x, we get ε(κ x, x) = κ x x = W κ x.

This connects adjunction-based binding to the W combinator in Binding.lean.

theorem Semantics.Composition.Effects.adj_binding_agrees_with_hk {m : Montague.Model} (n : ℕ) (body : m.Entity → m.Entity → Bool) (binder : m.Entity) (g : Montague.Variables.Assignment m) : adj_ε (body binder, binder) = body (g.update n binder n) (g.update n binder n)

H&K assignment-based binding and the adjunction co-unit agree for reflexive binding: both produce body(binder, binder).

This connects the adjunction (§5.1 of the paper) to the existing hk_bs_reflexive_equiv theorem in Binding.lean.

The C meta-combinator

eq. 5.8, Figure 10: the co-unit meta-combinator uses the adjunction's ε to compose W-computations (antecedent storage) with R-computations (pronoun resolution). For W ⊣ R, C reduces to unpacking the stored referent and feeding it to the reader function.

def Semantics.Composition.Effects.counitApp {ι σ τ ω : Type} (star : σ → τ → ω) (e₁ : σ × ι) (e₂ : ι → τ) : ω

C (Co-unit): the adjunction-based meta-combinator for binding.

eq. 5.8, Figure 10: C(∗) E₁ E₂ := ε((λl. (λr. l ∗ r) • E₂) • E₁)

For the W ⊣ R adjunction (§5.1), where W α = α × ι (product) and R α = ι → α (reader), the two fmap operations compose the binary combinator with both computations, and ε extracts the result: C(∗) ⟨s, i⟩ f = s ∗ f(i)

Crossover (§5.2): The type signature encodes the crossover constraint — the W effect (antecedent, σ × ι) must be the left daughter and the R effect (pronoun, ι → τ) the right daughter. Swapping them produces a type error, not a binding failure: there is no well-typed counitApp star (e₂ : ι → τ) (e₁ : σ × ι).

Equations

• Semantics.Composition.Effects.counitApp star e₁ e₂ = star e₁.1 (e₂ e₁.2)

theorem Semantics.Composition.Effects.counitApp_via_adj_ε {ι σ τ ω : Type} (star : σ → τ → ω) (e₁ : σ × ι) (e₂ : ι → τ) : counitApp star e₁ e₂ = adj_ε (star e₁.1 ∘ e₂, e₁.2)

C decomposes as ε applied to the doubly-mapped product.

The general formula maps (λr. l ∗ r) over E₂ (R-fmap = ∘), maps the result over E₁ (W-fmap on the first component), then applies ε to extract the value.

theorem Semantics.Composition.Effects.counitApp_reflexive_is_W {ι ω : Type} (κ : ι → ι → ω) (x : ι) : counitApp fa' (κ x, x) id = Reference.Binding.W κ x

C with reflexive storage ▷(x) = ⟨x, x⟩ and identity reader yields W.

When an antecedent stores itself and the pronoun is the identity reader, C(>) reduces to the W combinator from Binding.lean: C(>) ⟨κ x, x⟩ id = κ x x = W κ x.

This connects adjunction mechanism (their central §5 contribution) to the classical duplicator combinator that underlies binding.

§5 Effect operations and handlers

Named operations from, connecting existing linglib infrastructure to the effect/handler pattern.

Effects (introduce computational context):

• aside: Log a CI proposition (= Writer.tell)

Handlers (eliminate computational context):

• handleScope: Lower a Cont to its result (= Cont.lower)
• handleCI: Extract at-issue value and CI log from Writer

def Semantics.Composition.Effects.aside {P : Type} (p : P) : WriterMonad.Writer P Unit

Log a CI proposition as a side-effect. Alias for Writer.tell.

Equations

• Semantics.Composition.Effects.aside p = Semantics.Composition.WriterMonad.Writer.tell p

def Semantics.Composition.Effects.handleScope {R : Type} (m : Core.Continuation.Cont R R) : R

Handle the scope effect by evaluating with the identity continuation. Alias for Cont.lower.

Equations

• Semantics.Composition.Effects.handleScope m = m.lower

def Semantics.Composition.Effects.handleCI {P α : Type} (m : WriterMonad.Writer P α) : α × List P

Handle CI effects by extracting the value and accumulated log.

Equations

• Semantics.Composition.Effects.handleCI m = (m.val, m.log)

§6 Bridge theorems

Connect the effect framework to existing linglib constructions, proving that independently-developed linglib modules are instances of the effect-driven architecture.

theorem Semantics.Composition.Effects.writer_app_is_seq {P A B : Type} (mf : WriterMonad.Writer P (A → B)) (mx : WriterMonad.Writer P A) : mf.app mx = mf <*> mx

Writer.app is applicative application (⊛) for the Writer monad.

This connects WriterMonad.lean's monadic application to the effect hierarchy.

theorem Semantics.Composition.Effects.cont_lower_is_handleScope {R : Type} (m : Core.Continuation.Cont R R) : m.lower = handleScope m

Lowering a Cont is handling the scope effect.

def Semantics.Composition.Effects.twoDimToWriter {W : Type} (p : Lexical.Expressives.TwoDimProp W) : WriterMonad.Writer (W → Bool) (W → Bool)

A TwoDimProp embeds into a Writer (W → Bool) (W → Bool): the at-issue content is the value, the CI is the log.

This connects @cite{potts-2005}'s two-dimensional semantics to Writer effect (their W constructor in Table 2).

Equations

• Semantics.Composition.Effects.twoDimToWriter p = { val := p.atIssue, log := [p.ci] }

theorem Semantics.Composition.Effects.twoDim_neg_ci_via_writer {W : Type} (p : Lexical.Expressives.TwoDimProp W) : (twoDimToWriter p.neg).log = (twoDimToWriter p).log

CI projection through negation follows from the Writer architecture: map transforms the value but leaves the log untouched.

theorem Semantics.Composition.Effects.twoDim_neg_val_via_writer {W : Type} (p : Lexical.Expressives.TwoDimProp W) : (twoDimToWriter p.neg).val = fun (w : W) => !p.atIssue w

The at-issue content of negation is pointwise negation of the original.

def Semantics.Composition.Effects.gqAsCont {m : Montague.Model} (gq : (m.Entity → Bool) → Bool) : Core.Continuation.Cont Bool m.Entity

A generalized quantifier IS a Cont Bool Entity value.

Ch. 4: the continuation monad is the algebraic effect for scope-taking. A GQ (e → t) → t IS Cont Bool Entity by definition.

Equations

• Semantics.Composition.Effects.gqAsCont gq = gq

def Semantics.Composition.Effects.contAsGQ {m : Montague.Model} (c : Core.Continuation.Cont Bool m.Entity) : (m.Entity → Bool) → Bool

A Cont Bool Entity value IS a generalized quantifier.

Equations

• Semantics.Composition.Effects.contAsGQ c = c

theorem Semantics.Composition.Effects.gq_cont_roundtrip {m : Montague.Model} (gq : (m.Entity → Bool) → Bool) : contAsGQ (gqAsCont gq) = gq

Round-trip: GQ → Cont → GQ is identity.

def Semantics.Composition.Effects.every_as_cont (restrictor : Montague.toyModel.Entity → Bool) : Core.Continuation.Cont Bool Montague.toyModel.Entity

every_sem applied to a restrictor is a Cont Bool Entity value.

Equations

• Semantics.Composition.Effects.every_as_cont restrictor = Semantics.Composition.Effects.gqAsCont (Semantics.Lexical.Determiner.Quantifier.every_sem Semantics.Montague.toyModel restrictor)

def Semantics.Composition.Effects.some_as_cont (restrictor : Montague.toyModel.Entity → Bool) : Core.Continuation.Cont Bool Montague.toyModel.Entity

some_sem applied to a restrictor is a Cont Bool Entity value.

Equations

• Semantics.Composition.Effects.some_as_cont restrictor = Semantics.Composition.Effects.gqAsCont (Semantics.Lexical.Determiner.Quantifier.some_sem Semantics.Montague.toyModel restrictor)

theorem Semantics.Composition.Effects.scope_lower_eq_gq_id (restrictor scope' : Montague.toyModel.Entity → Bool) : handleScope ((gqAsCont (Lexical.Determiner.Quantifier.every_sem Montague.toyModel restrictor)).bind fun (x : Montague.toyModel.Entity) => Core.Continuation.Cont.pure (scope' x)) = Lexical.Determiner.Quantifier.every_sem Montague.toyModel restrictor scope'

Lowering a scope-taking quantifier = applying it to the scope.

theorem Semantics.Composition.Effects.scope_agrees_with_qr_everyStudentSleeps : handleScope ((gqAsCont (Lexical.Determiner.Quantifier.every_sem Montague.toyModel Lexical.Determiner.Quantifier.student_sem)).bind fun (x : Montague.toyModel.Entity) => Core.Continuation.Cont.pure (Montague.ToyLexicon.sleeps_sem x)) = (Tree.evalTree QuantifierComposition.quantLex QuantifierComposition.g₀ QuantifierComposition.tree_everyStudentSleeps).get!

Scope resolution via Cont agrees with QR tree for "every student sleeps".

theorem Semantics.Composition.Effects.scope_agrees_with_qr_someStudentSleeps : handleScope ((gqAsCont (Lexical.Determiner.Quantifier.some_sem Montague.toyModel Lexical.Determiner.Quantifier.student_sem)).bind fun (x : Montague.toyModel.Entity) => Core.Continuation.Cont.pure (Montague.ToyLexicon.sleeps_sem x)) = (Tree.evalTree QuantifierComposition.quantLex QuantifierComposition.g₀ QuantifierComposition.tree_someStudentSleeps).get!

Scope resolution via Cont agrees with QR tree for "some student sleeps".

theorem Semantics.Composition.Effects.scope_surface_agrees_with_qr : handleScope ((gqAsCont (Lexical.Determiner.Quantifier.every_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem)).bind fun (x : Montague.toyModel.Entity) => (gqAsCont (Lexical.Determiner.Quantifier.some_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem)).bind fun (y : Montague.toyModel.Entity) => Core.Continuation.Cont.pure (Montague.ToyLexicon.sees_sem y x)) = (Tree.evalTree QuantifierComposition.quantLex QuantifierComposition.g₀ QuantifierComposition.tree_surface).get!

Surface scope (∀>∃) via continuation composition agrees with QR.

theorem Semantics.Composition.Effects.scope_inverse_agrees_with_qr : handleScope ((gqAsCont (Lexical.Determiner.Quantifier.some_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem)).bind fun (y : Montague.toyModel.Entity) => (gqAsCont (Lexical.Determiner.Quantifier.every_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem)).bind fun (x : Montague.toyModel.Entity) => Core.Continuation.Cont.pure (Montague.ToyLexicon.sees_sem y x)) = (Tree.evalTree QuantifierComposition.quantLex QuantifierComposition.g₀ QuantifierComposition.tree_inverse).get!

Inverse scope (∃>∀) via continuation composition agrees with QR.

theorem Semantics.Composition.Effects.cont_scope_readings_differ : handleScope ((gqAsCont (Lexical.Determiner.Quantifier.every_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem)).bind fun (x : Montague.toyModel.Entity) => (gqAsCont (Lexical.Determiner.Quantifier.some_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem)).bind fun (y : Montague.toyModel.Entity) => Core.Continuation.Cont.pure (Montague.ToyLexicon.sees_sem y x)) ≠ handleScope ((gqAsCont (Lexical.Determiner.Quantifier.some_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem)).bind fun (y : Montague.toyModel.Entity) => (gqAsCont (Lexical.Determiner.Quantifier.every_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem)).bind fun (x : Montague.toyModel.Entity) => Core.Continuation.Cont.pure (Montague.ToyLexicon.sees_sem y x))

The two scope orderings via Cont yield genuinely different readings, matching scope_readings_differ from QuantifierComposition.lean.

theorem Semantics.Composition.Effects.surface_scope_via_cont : handleScope ((gqAsCont (Lexical.Determiner.Quantifier.every_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem)).bind fun (x : Montague.toyModel.Entity) => (gqAsCont (Lexical.Determiner.Quantifier.some_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem)).bind fun (y : Montague.toyModel.Entity) => Core.Continuation.Cont.pure (Montague.ToyLexicon.sees_sem y x)) = true

Surface scope reading = true in the toy model.

theorem Semantics.Composition.Effects.inverse_scope_via_cont : handleScope ((gqAsCont (Lexical.Determiner.Quantifier.some_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem)).bind fun (y : Montague.toyModel.Entity) => (gqAsCont (Lexical.Determiner.Quantifier.every_sem Montague.toyModel Lexical.Determiner.Quantifier.person_sem)).bind fun (x : Montague.toyModel.Entity) => Core.Continuation.Cont.pure (Montague.ToyLexicon.sees_sem y x)) = false

Inverse scope reading = false in the toy model.

Binding via the C meta-combinator

Worked derivation connecting C (eq. 5.8) to existing binding infrastructure over the toy model.

The W combinator W κ x = κ x x is the shared link between three independent binding mechanisms:

• C (co-unit meta-combinator): C(<) ▷(x) body = W body x
• H&K (assignment-based): body (g[n↦x] n) (g[n↦x] n) = W body x
• @cite{charlow-2018}'s Reader join: denotGJoin body = W body (proven in Charlow2018.lean:denotGJoin_is_W)

The derivation follows §5.1: the subject stores itself as an antecedent via ▷(x) = ⟨x, x⟩ (a W-computation), the reflexive pronoun is the identity reader (an R-computation), and C resolves the binding by feeding the stored referent to the reader.

def Semantics.Composition.Effects.store {α : Type} (x : α) : α × α

Antecedent storage: ▷(x) = ⟨x, x⟩.

eq. 5.1b: an entity stores its referent in the W (product) effect, making it available for downstream binding via the co-unit ε.

Equations

• Semantics.Composition.Effects.store x = (x, x)

theorem Semantics.Composition.Effects.counitApp_ba_store_is_W {ι β : Type} (body : ι → ι → β) (x : ι) : counitApp ba' (store x) body = Reference.Binding.W body x

C(<) with storage yields the W combinator.

Backward-application variant of counitApp_reflexive_is_W: C(<) ▷(x) body = body x x = W body x.

theorem Semantics.Composition.Effects.john_sees_himself_via_C : (counitApp ba' (store Montague.ToyEntity.john) fun (i : Montague.ToyEntity) => Montague.ToyLexicon.sees_sem i) = false

Reflexive binding: "John sees himself" via C.

The subject stores itself (▷(john) = ⟨john, john⟩), the reflexive pronoun resolves to the object via the identity reader, and C(<) merges them: C(<) ▷(j) (λi. sees i) = sees j j = false.

The false result confirms the toy model has no reflexive seeing (John sees Mary and Mary sees John, but neither sees themselves).

theorem Semantics.Composition.Effects.binding_C_agrees_with_hk (g : Montague.Variables.Assignment Montague.toyModel) : (counitApp ba' (store Montague.ToyEntity.john) fun (i : Montague.ToyEntity) => Montague.ToyLexicon.sees_sem i) = Montague.ToyLexicon.sees_sem (g.update 1 Montague.ToyEntity.john 1) (g.update 1 Montague.ToyEntity.john 1)

C-based binding agrees with H&K assignment-based binding: both compute sees(g[1↦j](1), g[1↦j](1)) = sees(j, j).

This connects adjunction mechanism to @cite{heim-kratzer-1998}'s predicate abstraction.

theorem Semantics.Composition.Effects.binding_C_agrees_with_hk_mary (g : Montague.Variables.Assignment Montague.toyModel) : (counitApp ba' (store Montague.ToyEntity.mary) fun (i : Montague.ToyEntity) => Montague.ToyLexicon.sees_sem i) = Montague.ToyLexicon.sees_sem (g.update 2 Montague.ToyEntity.mary 2) (g.update 2 Montague.ToyEntity.mary 2)

C and H&K agree for Mary as well: C(<) ▷(m) (λi. sees i) = sees m m.

§7 General scope agreement

The ScopeBridge section (§6) proved Cont ↔ QR agreement for the toy model via native_decide. Here we prove the agreement is structural: it holds for any type, any quantifier, and any predicate — not because we checked all cases, but because the two approaches compute the same function.

The key insight: Cont R E := (E → R) → R is literally a generalized quantifier. The identity function gqAsCont witnesses this — there is no encoding, no coercion, no wrapper. So the Cont derivation is GQ application by definition.

Scope ambiguity in the Cont framework is not a special mechanism: it is the order of monadic bind. Surface scope = bind the subject first; inverse scope = bind the object first. The bind order IS the scope order, and lower IS GQ application.

This establishes Cont as a general scope framework, with QR trees as one particular syntax for specifying bind order.

theorem Semantics.Composition.Effects.cont_scope_reduce {E R : Type} (q : Core.Continuation.Cont R E) (scope : E → R) : (q.bind fun (x : E) => Core.Continuation.Cont.pure (scope x)).lower = q scope

Single scope reduction: lowering a Cont-wrapped quantifier with a pure scope predicate is plain GQ application.

lower(Q >>= λx. pure(P x)) = Q(P)

This is the general version of scope_agrees_with_qr_everyStudentSleeps — it holds for ANY quantifier and ANY predicate, not just the toy model.

theorem Semantics.Composition.Effects.cont_scope_double {E R : Type} (q₁ q₂ : Core.Continuation.Cont R E) (rel : E → E → R) : (q₁.bind fun (x : E) => q₂.bind fun (y : E) => Core.Continuation.Cont.pure (rel x y)).lower = q₁ fun (x : E) => q₂ fun (y : E) => rel x y

Two-quantifier scope reduction: nested Cont binds compute nested GQ application. The bind nesting determines scope order.

lower(Q₁ >>= λx. Q₂ >>= λy. pure(R x y)) = Q₁(λx. Q₂(λy. R x y))

theorem Semantics.Composition.Effects.scope_ambiguity_is_bind_order {E R : Type} (q₁ q₂ : Core.Continuation.Cont R E) (rel : E → E → R) : ((q₁.bind fun (x : E) => q₂.bind fun (y : E) => Core.Continuation.Cont.pure (rel x y)).lower = q₁ fun (x : E) => q₂ fun (y : E) => rel x y) ∧ (q₂.bind fun (y : E) => q₁.bind fun (x : E) => Core.Continuation.Cont.pure (rel x y)).lower = q₂ fun (y : E) => q₁ fun (x : E) => rel x y

Scope ambiguity = bind order. The two readings of "Q₁ R Q₂" arise from nesting Q₁ outside Q₂ vs Q₂ outside Q₁.

Both reduce to GQ application in the corresponding order.

theorem Semantics.Composition.Effects.cont_scope_triple {E R : Type} (q₁ q₂ q₃ : Core.Continuation.Cont R E) (rel : E → E → E → R) : (q₁.bind fun (x : E) => q₂.bind fun (y : E) => q₃.bind fun (z : E) => Core.Continuation.Cont.pure (rel x y z)).lower = q₁ fun (x : E) => q₂ fun (y : E) => q₃ fun (z : E) => rel x y z

Three-quantifier scope: the pattern extends to arbitrary depth.

theorem Semantics.Composition.Effects.cont_pure_is_fa {R A : Type} (f : A → R) (x : A) : ((Core.Continuation.Cont.pure f).bind fun (g : A → R) => (Core.Continuation.Cont.pure x).bind fun (y : A) => Core.Continuation.Cont.pure (g y)).lower = f x

Non-scope-taking = ordinary FA: when all meanings are wrapped in Cont.pure, Cont composition reduces to function application.

lower(pure(f) >>= λg. pure(x) >>= λy. pure(g y)) = f x

This is the embedding of Reader (the non-scope-taking fragment) into Cont: @cite{charlow-2018}'s ρ(f) ⊛ ρ(x) = ρ(f x) is exactly the Cont homomorphism law.

theorem Semantics.Composition.Effects.qr_cont_structural_agreement {m : Montague.Model} (q : (m.Entity → Bool) → Bool) (body : Montague.Variables.DenotG m Montague.Ty.t) (n : ℕ) (g : Montague.Variables.Assignment m) : q (Montague.Variables.lambdaAbsG n body g) = (Core.Continuation.Cont.bind q fun (x : m.Entity) => Core.Continuation.Cont.pure (body (g.update n x))).lower

QR scope = Cont scope via lambdaAbsG: the structural connection between QR trees and Cont derivations.

In a QR tree [Q [n body]], Predicate Abstraction produces Q(λx. ⟦body⟧^{g[n↦x]}) = Q(lambdaAbsG n body g).

In a Cont derivation, lower(bind(Q, λx. pure(body(g[n↦x])))) = Q(λx. body(g[n↦x])) = Q(lambdaAbsG n body g).

Both compute the same thing: the quantifier applied to the predicate abstraction of its scope. QR and Cont differ only in how scope order is specified (tree structure vs bind order), not in what they compute.

§8 Three-way binding unification

Three independently-developed binding mechanisms in linglib all compute the same operation f e e:

Source	Operation	Definition	File
@cite{heim-kratzer-1998}	denotGJoin (μ)	λg. f g g	Variables.lean
@cite{barker-shan-2014}	W (duplicator)	W κ x = κ x x	Binding.lean
	adj_ε (co-unit)	ε(f e, e) = (f e) e	Effects.lean §4

The individual two-way bridges exist:

• denotGJoin_is_W (Charlow2018.lean)
• adj_counit_yields_W (Effects.lean §4)

Here we close the triangle with a single three-way theorem.

theorem Semantics.Composition.Effects.w_three_way {E A : Type} (f : E → E → A) (e : E) : (fun (g : E) => f g g) e = Reference.Binding.W f e ∧ Reference.Binding.W f e = adj_ε (f e, e)

Three-way W: the duplicator, Reader join, and adjunction co-unit all compute f e e. This is the universal binding mechanism.

The identity is definitional: the three frameworks are not merely extensionally equal but intensionally identical up to currying/pairing.

theorem Semantics.Composition.Effects.binding_unification {m : Montague.Model} {A : Type} (f : Montague.Variables.Assignment m → Montague.Variables.Assignment m → A) (g : Montague.Variables.Assignment m) : Montague.Variables.denotGJoin f g = Reference.Binding.W f g ∧ Reference.Binding.W f g = adj_ε (f g, g)

Specialization for Montague assignments: denotGJoin = W = adj_ε when applied to assignment-dependent meanings.

theorem Semantics.Composition.Effects.binding_triangle {m : Montague.Model} {A : Type} (f : Montague.Variables.Assignment m → Montague.Variables.Assignment m → A) (g : Montague.Variables.Assignment m) : Montague.Variables.denotGJoin f g = adj_ε (f g, g)

Closing the triangle directly: denotGJoin = adj_ε ∘ ⟨f·, ·⟩.

    denotGJoin ──── rfl ────→ W
          \                    |
           \                   |
       rfl  \              rfl |
             ↘                 ↓
               adj_ε ∘ ⟨f·, ·⟩

§9 Indeterminacy effect

The indeterminacy effect — labeled S in's Table 2 — is the set monad (S, η, ⫝̸) from @cite{charlow-2020}, formalized in SetMonad.lean.

Effect	η (pure)	⫝̸ (bind)	Linguistic use
Scope (C)	λκ. κ x	λκ. m(λa. f a κ)	Quantifier scope
CI (W)	⟨x, []⟩	⟨(f m.val).val, m.log ++ ...⟩	Supplements
Binding (R)	λ_. x	λe. f(m e) e	Assignment-sensitivity
Indeterminacy (S)	{x}	⋃_{a ∈ m} f(a)	Indefinites, focus, wh

The set monad's applicative instance is pointwise composition — the standard mechanism of alternative semantics (@cite{hamblin-1973b}, @cite{kratzer-shimoyama-2002}). Its monadic bind is scope-taking — the mechanism @cite{charlow-2020} argues is needed for exceptional scope.

The applicative is strictly weaker: it cannot derive selectivity (§5.4 of the paper) or the Binder Roof Constraint (§6.4). The monad can.

theorem Semantics.Composition.Effects.indeterminacy_pure_is_eta {A : Type} (x : A) : SetMonad.eta x = fun (y : A) => y = x

The set monad's η is the indeterminacy effect's pure.

theorem Semantics.Composition.Effects.indeterminacy_bind_is_setBind {A B : Type} (m : A → Prop) (f : A → B → Prop) : SetMonad.setBind m f = fun (b : B) => ∃ (a : A), m a ∧ f a b

The set monad's ⫝̸ is the indeterminacy effect's bind.

theorem Semantics.Composition.Effects.indeterminacy_associativity {A B C : Type} (m : A → Prop) (f : A → B → Prop) (g : B → C → Prop) : SetMonad.setBind (SetMonad.setBind m f) g = SetMonad.setBind m fun (a : A) => SetMonad.setBind (f a) g

Indeterminacy obeys ASSOCIATIVITY. Re-export from SetMonad.lean.

This is the property that distinguishes the full monad from the mere applicative: (m ⫝̸ f) ⫝̸ g = m ⫝̸ (λx. f x ⫝̸ g). Without it, indefinites cannot iteratively scope out of nested islands.