Fibered variable lookup

[Hof25], [Cha19b]

The lookup interface of dynamic semantics: iLookup : Ctx → V → W → M E returns the M-family of values for a variable at a world. Frameworks diverge on what a lookup returns when a variable has no referent — Hofmann's .star (M = Entity, instance in ICDRT/Basic.lean), Charlow's ∅ (M = Set, instance in Studies/Charlow2019.lean), plain values for the extensional baseline (M = Id, the Assignment instance below) — and the shared signature is what makes per-family lookups comparable (Reference/PronounDenotation.lean's interpPronoun_eq_iLookup).

The class is data-only (the Membership/GetElem pattern): update laws and accessibility predicates are each family's own commitments and live in the family's file; the comparisons live in the studies that draw them (Studies/Hofmann2025.lean, Studies/Charlow2019.lean).

class DynamicSemantics.HasFiberedLookup (M : outParam (Type u → Type u)) (Ctx : Type v) (V : outParam (Type w)) (W : outParam (Type x)) (E : outParam (Type u)) : Type (max (max (max u v) w) x)

Fibered lookup: iLookup i v w : M E returns the M-family of values for variable v at world w — M = Entity (ICDRT), M = Set (Charlow's marginal), M = Id (extensional baseline). M is outParam: each Ctx carries exactly one effect functor.

• iLookup : Ctx → V → W → M E

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

@[implicit_reducible]

instance DynamicSemantics.instAssignmentHasFiberedLookup (E : Type u) : HasFiberedLookup Id (Core.Assignment E) ℕ PUnit E

Assignments as the extensional dynamic-semantic context, with M = Id (no effect) and W = PUnit (no world parameter) — the baseline shared by [GS91a] DPL, [Mus96] CDRT, and [KR93] DRT, whose state types are all definitionally Nat → E = Assignment E. Lookup is function application.

Equations

• DynamicSemantics.instAssignmentHasFiberedLookup E = { iLookup := fun (g : Core.Assignment E) (v : ℕ) (x : PUnit) => g v }