Dynamic Context — Effect-Functor-Parameterized Interface

@cite{groenendijk-stokhof-1991} @cite{muskens-1996} @cite{heim-1982} @cite{charlow-2019} @cite{hofmann-2025} @cite{grove-white-2025b}

A typeclass interface for dynamic-semantics contexts, parameterized on the effect functor M that wraps each variable's value at a world. The unifying frame across deterministic, nondeterministic, and probabilistic dynamic semantics — at the fibered-lookup signature.

Mathlib-style discipline

Where structure is shared, expose it via a typeclass. HasFiberedLookup gives every family the same iLookup : Ctx → V → W → M E interface, so cross-family predicates are by-construction comparable. HasIndivDrefs extends it, adding the Hofmann-specific iVarUp update relation. HasJointState extends it the other direction, marking frameworks whose underlying state is natively joint over (world, assignment) pairs — a strictly richer commitment than the fibered signature exposes.

Bridge maps between families are explicit named natural transformations of M, following the mathlib pattern (Function/Set.Image/ MeasurableFunction/PMF/Measure as a family of related-but-not- unified abstractions).

Honest scope: the lookup is fibered

The lookup signature Ctx → V → W → M E is fibered by construction — every state, joint or not, can answer "what is the M-distribution of v's value at world w?". For Charlow's joint Set (W × Assignment E), this requires marginalizing out the world-assignment correlation; for ICDRT it's a direct lookup; for fibered-Bayesian (W → PMF (Assignment E)) it's projection. The renamed class HasFiberedLookup (was HasIndivLookupM) makes this explicit — what is unified is the fibered projection, not the underlying state shape.

Six 2026 seams

What this interface does not paper over: six places where dynamic theories deliberately diverge in 2026. Each is named, locatable (grep "## SEAM"), and committed at the per-family file level — visible structure, not hidden disagreement.

Seam 1 — Falsifier convention

What does "no referent for v at w" mean?

Family	Falsifier	Source
ICDRT	Entity.star (bivalent distinguished value)	@cite{hofmann-2025}
Charlow	∅ (empty alternative-set; no value-level falsifier)	@cite{charlow-2019}
Bayesian	zero-mass (PMF assigns probability 0; no value-level falsifier)	@cite{grove-white-2025b}
FCS	Dom-partiality (FCP undefined; no value-level falsifier at all)	@cite{heim-1982}

Charlow's argument: bivalence undermines compositional negation. Hofmann's argument: alternative-sets underdetermine anaphora projection. Heim's argument: partiality models presupposition-as-definedness directly. The seam stays open.

Seam 2 — State shape (joint vs fibered)

Does the underlying state remember world–assignment correlation?

Family	State shape	Class
ICDRT	fibered (indiv : IVar → W → Entity E)	HasFiberedLookup only
Charlow	joint (Set (W × Assignment E))	HasFiberedLookup + HasJointState
Bayesian (PDS)	joint (PMF (W × Assignment E), per @cite{grove-white-2025b})	HasFiberedLookup + HasJointState
Bayesian (fibered)	fibered (W → PMF (Assignment E))	HasFiberedLookup only
FCS	joint (Sat ⊆ World × Assignment)	HasFiberedLookup + HasJointState

The lookup signature is fibered for every family — this is what HasFiberedLookup unifies. The underlying state may carry strictly more structure: HasJointState marks frameworks where it does. The fibered projection of a joint state is lossy — world-assignment correlations beyond what a single (v, w) query probes are discarded.

Seam 3 — Update mechanism

What does "extend the discourse" mean operationally?

Family	Update primitive
ICDRT	assignment update (updateIndiv g v e)
Charlow	alternative filtering / set-builder
Bayesian	conditioning (Bayes update / PMF.bind)
FCS	partial functional update (definedness-tracking)

These genuinely don't unify — Charlow's bind is non-commutative (his "scope of alternatives" thesis); PMF's bind is commutative under independence; Hofmann's update is sequential; Heim's is partial. The interface deliberately omits a master Update typeclass.

Seam 4 — Definedness predicate

"v has a definite referent at w in i."

Family	Predicate shape
ICDRT	iLookup i v w ≠ Entity.star
Charlow	iLookup i v w is a singleton set
Bayesian	iLookup i v w is a Dirac/point-mass
FCS	v ∈ Dom(F) (definedness is metadata, not value-level)

All four express "the M-fiber is determinate." Mathlib has Set.Subsingleton and PMF.IsDeterministic for the second/third; FCS's Dom-tracking is structurally distinct (it's a property of the state, not the fiber). We ship parallel-named predicates (isDeterminateAt per family) without yet abstracting; the seam stays visible until a study needs to quantify over it.

Seam 5 — Effect commutativity

Does the order in which effects are introduced matter?

Family	Commutativity
ICDRT	trivially yes (sequential update)
Charlow	NO — "scope of alternatives" thesis
Bayesian	yes under independence; no in general

Not visible in lookup; surfaces in composition (multiple lookups combining). Out of scope for this interface; lives in each family's own composition operators.

Seam 6 — Anaphora resolution mechanism

Where does pronoun resolution come from?

Family	Mechanism
Heim/Kamp	dref binding via assignment update
E-type / situation	NP reconstruction (Elbourne, Heim 1990)
Charlow	alternatives in the continuation
Hofmann (ICDRT)	propositional drefs as local contexts
Bayesian	posterior conditioning on observed reference

The deepest seam — not in the lookup signature, but in how lookups get used by Phenomena/.../Studies/. Each Studies file commits in its own resolution semantics. (Karttunen 1976 introduced the idea of drefs without the assignment-update formalization, so the binding row is attributed to Heim/Kamp.)

Key Types

Class	Carries
HasFiberedLookup M Ctx V W E	Fibered lookup signature Ctx → V → W → M E
HasJointState M Ctx V W E	Extends HasFiberedLookup; native joint state Ctx → M (W × (V → E))
HasIndivDrefs Ctx V W E	Extends HasFiberedLookup Entity + Hofmann iVarUp law
HasPropDrefs Ctx P W	Propositional drefs P to sets of worlds
HasDiscourseCommitment Ctx P	Distinguished commitment-set var (single speaker)
HasMultiDC Ctx P Speaker	Per-speaker commitment-set vars (dialogue)

class Semantics.Dynamic.Context.HasFiberedLookup (M : outParam (Type u → Type u)) [Functor M] (Ctx : Type v) (V : outParam (Type w)) (W : outParam (Type x)) (E : outParam (Type u)) : Type (max (max (max u v) w) x)

Fibered effect-functor lookup — the unifying frame across deterministic, nondeterministic, and probabilistic dynamic semantics.

iLookup i v w : M E returns a family of values structured by an effect functor M at a particular world:

• M = Entity (deterministic; ICDRT)
• M = Set (nondeterministic; Charlow's marginal at world w)
• M = PMF (probabilistic; Bayesian per-world fiber)
• M = Id (extensional baselines: DPL, CDRT, DRT — W = PUnit)

M is outParam: each Ctx carries exactly one effect functor. Functor M is enough — no Monad M requirement, since Set lacks a clean Monad instance in Lean. Bridge maps between families are explicit named natural transformations of M, not monad lifts.

SEAM (Seam 2): The signature is fibered by construction. Joint-state

families (Charlow, FCS, PDS Bayesian) provide an iLookup by marginalizing their joint state — see HasJointState for the explicit joint-vs-fibered distinction, and individual instance files for the per-family marginalization implementation.

SEAM (Seam 1): Per-family iLookup instances commit to a falsifier

convention — .star (Entity), ∅ (Set), zero-mass (PMF), Dom-partiality (FCS metadata-level).

• iLookup : Ctx → V → W → M E

  Look up the M-family of values for variable v at world w.

class Semantics.Dynamic.Context.HasJointState (M : outParam (Type u → Type u)) [Functor M] (Ctx : Type v) (V W E : outParam (Type u)) extends Semantics.Dynamic.Context.HasFiberedLookup M Ctx V W E : Type (max u v)

Joint-state interface — frameworks whose underlying state is a single M-distribution / structure over (world, assignment) pairs, rather than a fiber W → M (Assignment E). Per Seam 2.

Joint states automatically provide HasFiberedLookup (it is an extends parent), but the fibered projection of a joint state is lossy: world-assignment correlations beyond what a single (v, w) query probes are discarded by marginalization.

The marginalization itself is per-family because it requires more than Functor M — Charlow needs filtering (set-builder), PDS needs conditioning (PMF.cond machinery). Each HasJointState instance provides its own iLookup implementation that agrees with marginalizing its joint; the agreement is a per-family proof obligation, not a typeclass field.

Frameworks committing to this typeclass: Charlow 2019 (State W E := Set (W × Assignment E)), FCS (HeimFile with Sat ⊆ World × Assignment), PDS Bayesian per @cite{grove-white-2025b} (PMF (W × Assignment E)). Frameworks that deliberately do not declare it: ICDRT, fibered-Bayesian.

The joint field exposes the native joint object as M (W × (V → E)) — assignments rendered as functions V → E. This constrains V/W/E to share the universe u of M's domain.

SEAM (Seam 2): Declaring this typeclass commits empirically to having

joint structure to lose. The mere existence of HasFiberedLookup says nothing about the underlying state; HasJointState does.

• iLookup : Ctx → V → W → M E
• joint : Ctx → M (W × (V → E))

  The native joint object — the M-structure over (world, assignment) pairs that the framework natively carries. Assignments are rendered as functions V → E.

@[implicit_reducible]

instance Semantics.Dynamic.Context.instAssignmentHasFiberedLookup (E : Type u) : HasFiberedLookup Id (Core.Assignment E) ℕ PUnit.{u + 1} E

Assignments themselves serve as the extensional dynamic-semantic context, with M = Id (no effect) and W = PUnit (no world parameter). This is the trivial baseline shared by @cite{groenendijk-stokhof-1991} DPL, @cite{muskens-1996} CDRT, and @cite{kamp-reyle-1993} DRT — their state types are all definitionally Nat → E = Assignment E, so this single instance covers all three.

Lookup is just function application, world-independent. The "indefinite-persistence" pattern that recurs across these three extensional theories — pronouns can pick up whatever an indefinite introduced — is captured at the typeclass level by sharing the same HasFiberedLookup Id interface. Per-paper theorems can be stated abstractly over [HasFiberedLookup Id Ctx V W E] and instantiated to each theory.

SEAM (Seam 1): The extensional baseline has no falsifier — every

variable always has a value. This is the empirically wrong commitment that motivated the move to Hofmann's .star, Charlow's ∅, and Heim's Dom — but it is also the cleanest baseline against which the other three falsifier conventions are minimal extensions.

Equations

• Semantics.Dynamic.Context.instAssignmentHasFiberedLookup E = { iLookup := fun (g : Core.Assignment E) (v : ℕ) (x : PUnit.{?u.20 + 1}) => g v }

class Semantics.Dynamic.Context.HasIndivDrefs (Ctx : Type v) (V : outParam (Type w)) (W : outParam (Type x)) (E : outParam (Type u)) extends Semantics.Dynamic.Context.HasFiberedLookup Semantics.Dynamic.Core.Entity Ctx V W E : Type (max (max (max u v) w) x)

Hofmann-style deterministic context: HasFiberedLookup Entity plus the iVarUp update relation.

Extends the abstract effect-functor lookup with the Hofmann update law: two contexts that "differ at most in v" agree on every other variable. The Entity-specific extension; for non-bivalent families the analogous update relations are family-specific (Seam 3).

• iLookup : Ctx → V → W → Core.Entity E
• iVarUp : V → Ctx → Ctx → Prop

  "j differs from i at most in v" — relation form.

• iVarUp_other (v : V) (i j : Ctx) (u : V) : iVarUp v i j → u ≠ v → HasFiberedLookup.iLookup j u = HasFiberedLookup.iLookup i u

  Equality of lookups outside the updated variable.

class Semantics.Dynamic.Context.HasPropDrefs (Ctx : Type v) (P : outParam (Type w)) (W : outParam (Type x)) : Type (max (max v w) x)

Contexts carrying propositional drefs (sets of worlds).

• pLookup : Ctx → P → Set W

  Look up the worlds-set associated with propositional variable p.

• pVarUp : P → Ctx → Ctx → Prop

  "j differs from i at most in p" — relation form.

• pVarUp_other (p : P) (i j : Ctx) (q : P) : pVarUp p i j → q ≠ p → pLookup j q = pLookup i q

  Equality of lookups outside the updated variable.

class Semantics.Dynamic.Context.HasDiscourseCommitment (Ctx : Type v) (P : outParam (Type w)) : Type w

Contexts with a single distinguished commitment-set propositional var.

• commitVar : P

  The propositional variable naming the speaker's commitment set.

class Semantics.Dynamic.Context.HasMultiDC (Ctx : Type v) (P : outParam (Type w)) (Speaker : Type x) : Type (max w x)

Contexts with per-speaker commitment-set vars. Speaker is NOT outParam: the same context type may carry different speaker indexings.

• commitVarOf : Speaker → P

  Map from interlocutor identifier to her commitment-set var.

@[implicit_reducible]

instance Semantics.Dynamic.Context.instMultiDC_of_single {Ctx : Type v} {P : Type w} [HasDiscourseCommitment Ctx P] : HasMultiDC Ctx P PUnit.{u_1 + 1}

Single-speaker is the trivial multi-speaker case with Speaker = PUnit.

Equations

• Semantics.Dynamic.Context.instMultiDC_of_single = { commitVarOf := fun (x : PUnit.{?u.21 + 1}) => Semantics.Dynamic.Context.HasDiscourseCommitment.commitVar Ctx }

These predicates use the Entity.star falsifier and so are ICDRT-specific. Charlow / Bayesian analogs (uniquelyDeterminedAt, PMF determinism) live in their respective family files (Seam 4).

def Semantics.Dynamic.Context.localEntailment {Ctx : Type v} {V : Type w₁} {P : Type w₂} {W : Type x} {E : Type u} [HasIndivDrefs Ctx V W E] [HasPropDrefs Ctx P W] (φ : P) (v : V) (i : Ctx) : Prop

Local contextual entailment: v defined throughout φ(i). A precondition for anaphora to v resolved in local context φ.

Equations

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

def Semantics.Dynamic.Context.veridicalIndiv {Ctx : Type v} {V : Type w₁} {P : Type w₂} {W : Type x} {E : Type u} [HasIndivDrefs Ctx V W E] [HasPropDrefs Ctx P W] (φ_DC : P) (v : V) (i : Ctx) : Prop

Veridicality of an individual dref relative to a commitment set.

Equations

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

def Semantics.Dynamic.Context.counterfactualIndiv {Ctx : Type v} {V : Type w₁} {P : Type w₂} {W : Type x} {E : Type u} [HasIndivDrefs Ctx V W E] [HasPropDrefs Ctx P W] (φ_DC : P) (v : V) (i : Ctx) : Prop

Counterfactuality: v maps to ⋆ in all φ_DC-worlds.

Equations

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

def Semantics.Dynamic.Context.subsetReq {Ctx : Type v} {P : Type w₂} {W : Type x} [HasPropDrefs Ctx P W] (φ_anaphor φ_antecedent : P) (i : Ctx) : Prop

Subset requirement: φ_anaphor(i) ⊆ φ_antecedent(i).

Equations

• Semantics.Dynamic.Context.subsetReq φ_anaphor φ_antecedent i = (Semantics.Dynamic.Context.HasPropDrefs.pLookup i φ_anaphor ⊆ Semantics.Dynamic.Context.HasPropDrefs.pLookup i φ_antecedent)

def Semantics.Dynamic.Context.decCondition {Ctx : Type v} {P : Type w₂} {W : Type x} [HasPropDrefs Ctx P W] (φ_DC φ : P) (i : Ctx) : Prop

DEC condition: φ_DC(j) ⊆ φ(j).

Equations

• Semantics.Dynamic.Context.decCondition φ_DC φ i = (Semantics.Dynamic.Context.HasPropDrefs.pLookup i φ_DC ⊆ Semantics.Dynamic.Context.HasPropDrefs.pLookup i φ)

def Semantics.Dynamic.Context.consistentAt {Ctx : Type v} {P : Type w₂} {W : Type x} [HasPropDrefs Ctx P W] (φ_DC : P) (i : Ctx) : Prop

Discourse consistency: commitment set is nonempty.

Equations

• Semantics.Dynamic.Context.consistentAt φ_DC i = (Semantics.Dynamic.Context.HasPropDrefs.pLookup i φ_DC).Nonempty

def Semantics.Dynamic.Context.accessible {Ctx : Type v} {V : Type w₁} {P : Type w₂} {W : Type x} {E : Type u} [HasIndivDrefs Ctx V W E] [HasPropDrefs Ctx P W] (φ_anaphor : P) (v : V) (φ_DC : P) (i : Ctx) : Prop

Accessibility = local entailment ∧ consistency.

Equations

• Semantics.Dynamic.Context.accessible φ_anaphor v φ_DC i = (Semantics.Dynamic.Context.localEntailment φ_anaphor v i ∧ Semantics.Dynamic.Context.consistentAt φ_DC i)

def Semantics.Dynamic.Context.definedAt {Ctx : Type v} {V : Type w₁} {W : Type x} {E : Type u} [HasIndivDrefs Ctx V W E] (v : V) (i : Ctx) : Set W

Worlds where v has a non-⋆ referent in context i.

Equations

• Semantics.Dynamic.Context.definedAt v i = {w : W | Semantics.Dynamic.Context.HasFiberedLookup.iLookup i v w ≠ Semantics.Dynamic.Core.Entity.star}

def Semantics.Dynamic.Context.relVarUp {Ctx : Type v} {V : Type w₁} {P : Type w₂} {W : Type x} {E : Type u} [HasIndivDrefs Ctx V W E] [HasPropDrefs Ctx P W] (φ : P) (v : V) (i j : Ctx) : Prop

Generic relative-variable update: differ at most in v, and the propositional dref φ(j) tracks exactly v's definedness pattern in j. This is Hofmann's cross-field operation expressed without a new typeclass — pure combination of iVarUp and pLookup.

Equations

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

def Semantics.Dynamic.Context.commitVarFor {Ctx : Type v} (P : Type w) {Speaker : Type x} [HasMultiDC Ctx P Speaker] (s : Speaker) : P

Pull the commitment var out of HasMultiDC with explicit type arguments — wrapping avoids field-projection ambiguities from the non-outParam Speaker parameter.

Equations

• Semantics.Dynamic.Context.commitVarFor P s = Semantics.Dynamic.Context.HasMultiDC.commitVarOf Ctx s

def Semantics.Dynamic.Context.multiConsistentAt {Ctx : Type v} {P : Type w₁} {W : Type w₂} {Speaker : Type x} [HasPropDrefs Ctx P W] [HasMultiDC Ctx P Speaker] (speakers : Set Speaker) (i : Ctx) : Prop

Multi-agent discourse consistency: every speaker's commitment set is nonempty in i.

Equations

• Semantics.Dynamic.Context.multiConsistentAt speakers i = ∀ s ∈ speakers, (Semantics.Dynamic.Context.HasPropDrefs.pLookup i (Semantics.Dynamic.Context.commitVarFor P s)).Nonempty

def Semantics.Dynamic.Context.multiAccessible {Ctx : Type v} {P : Type w} {V : Type w₁} {W : Type w₂} {E : Type u} {Speaker : Type x} [HasIndivDrefs Ctx V W E] [HasPropDrefs Ctx P W] [HasMultiDC Ctx P Speaker] (φ_anaphor : P) (vr : V) (speakers : Set Speaker) (i : Ctx) : Prop

Per-speaker accessibility — local entailment plus multi-agent consistency.

Equations

• Semantics.Dynamic.Context.multiAccessible φ_anaphor vr speakers i = (Semantics.Dynamic.Context.localEntailment φ_anaphor vr i ∧ Semantics.Dynamic.Context.multiConsistentAt speakers i)

theorem Semantics.Dynamic.Context.counterfactual_blocks_veridical {Ctx : Type v} {P : Type w} {W : Type x} [HasPropDrefs Ctx P W] (i j : Ctx) (φ_DC φ_anaphor φ_neg : P) (h_extends_DC : HasPropDrefs.pLookup j φ_DC = HasPropDrefs.pLookup i φ_DC) (h_extends_neg : HasPropDrefs.pLookup j φ_neg = HasPropDrefs.pLookup i φ_neg) (h_DC_disjoint_neg : HasPropDrefs.pLookup i φ_DC ∩ HasPropDrefs.pLookup i φ_neg = ∅) (h_dec : decCondition φ_DC φ_anaphor j) (h_subset : subsetReq φ_anaphor φ_neg j) : ¬consistentAt φ_DC j

Counterfactual antecedent blocks veridical anaphor (abstract).

In any Ctx with prop drefs, if we extend i to j keeping φ_DC and φ_neg lookups fixed, and the antecedent provides counterfactuality (φ_DC(i) ∩ φ_neg(i) = ∅), then satisfying both DEC (φ_DC(j) ⊆ φ_anaphor(j)) and the subset requirement (φ_anaphor(j) ⊆ φ_neg(j)) forces φ_DC(j) = ∅, i.e. discourse inconsistency.

This is the typeclass-only version of @cite{hofmann-2025}'s bathroom- sentence theorem: "There isn't a bathroom. #It is upstairs."

SEAM 6 (Anaphora resolution): The theorem only needs HasPropDrefs

— individual drefs and the Entity/Set/PMF effect functor play no role. Charlow's State W E carries no propositional-dref structure, so this theorem does not transfer to Charlow contexts. The same empirical phenomenon under Charlow's framework is solved by alternative-set filtering, not by propositional-dref disjointness — different resolution mechanism, different theorem.

theorem Semantics.Dynamic.Context.multi_counterfactual_blocks_veridical {Ctx : Type v} {P : Type w} {W : Type w₂} {Speaker : Type x} [HasPropDrefs Ctx P W] [HasMultiDC Ctx P Speaker] (i j : Ctx) (φ_anaphor φ_neg : P) (speakers : Set Speaker) (s : Speaker) (hs : s ∈ speakers) (h_extends_DC : HasPropDrefs.pLookup j (commitVarFor P s) = HasPropDrefs.pLookup i (commitVarFor P s)) (h_extends_neg : HasPropDrefs.pLookup j φ_neg = HasPropDrefs.pLookup i φ_neg) (h_DC_disjoint_neg : HasPropDrefs.pLookup i (commitVarFor P s) ∩ HasPropDrefs.pLookup i φ_neg = ∅) (h_dec : decCondition (commitVarFor P s) φ_anaphor j) (h_subset : subsetReq φ_anaphor φ_neg j) : ¬multiConsistentAt speakers j

Multi-speaker generalization: blocks veridical anaphor for ANY speaker whose commitment set is disjoint from the negative prejacent.