Context Tower

@cite{abusch-1997} @cite{anand-nevins-2004} @cite{cumming-2026} @cite{schlenker-2003}

A depth-indexed stack of context shifts unifying the codebase's context-manipulation mechanisms: Kaplanian indexicals (origin access), shifted indexicals (local access), De Bruijn temporal indexing (depth-relative access), situation introduction (mood), and domain expansion (branching time).

The tower is parametric over any context type C. KContext serves as the canonical instantiation — it represents what a single context layer looks like. The tower wraps it with a stack of shifts.

Key Operations

• .origin — the root context (speech-act context, Kaplan's c*)
• .innermost — the most deeply embedded context (fold all shifts over origin)
• .contextAt k — the context at depth k (fold first k shifts)
• .push σ — embed deeper by adding a new shift
• .root c — trivial tower (no shifts, depth 0)

How FA Composes with Towers

FA takes two meanings (function and argument). Both are parameterized by the same tower. FA applies the function to the argument at that tower. The tower is threaded as a reader parameter — ContextTower C →... is the enriched meaning type.

inductive Core.Context.ShiftLabel : Type

Classification of context shifts by their linguistic source.

• attitude : ShiftLabel
• temporal : ShiftLabel
• evidential : ShiftLabel
• mood : ShiftLabel
• perspective : ShiftLabel
• quotation : ShiftLabel
• clauseChain : ShiftLabel
• roleShift : ShiftLabel
• generic : ShiftLabel

instance Core.Context.instDecidableEqShiftLabel : DecidableEq ShiftLabel

Equations

• Core.Context.instDecidableEqShiftLabel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Context.instReprShiftLabel : Repr ShiftLabel

Equations

• Core.Context.instReprShiftLabel = { reprPrec := Core.Context.instReprShiftLabel.repr }

def Core.Context.instReprShiftLabel.repr : ShiftLabel → ℕ → Std.Format

Equations

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

def Core.Context.instBEqShiftLabel.beq : ShiftLabel → ShiftLabel → Bool

Equations

• Core.Context.instBEqShiftLabel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Context.instBEqShiftLabel : BEq ShiftLabel

Equations

• Core.Context.instBEqShiftLabel = { beq := Core.Context.instBEqShiftLabel.beq }

instance Core.Context.instInhabitedShiftLabel : Inhabited ShiftLabel

Equations

• Core.Context.instInhabitedShiftLabel = { default := Core.Context.instInhabitedShiftLabel.default }

def Core.Context.instInhabitedShiftLabel.default : ShiftLabel

Equations

• Core.Context.instInhabitedShiftLabel.default = Core.Context.ShiftLabel.attitude

structure Core.Context.ContextShift (C : Type u_1) : Type u_1

A single context shift: a function transforming a context, tagged with its linguistic source.

• apply : C → C

  The context transformation

• label : ShiftLabel

  What kind of linguistic operation introduced this shift

structure Core.Context.ContextTower (C : Type u_1) : Type u_1

A context tower: an origin context with a stack of shifts.

The origin is the speech-act context (Kaplan's c*). Each shift corresponds to an embedding operator (attitude verb, temporal shift, mood operator). Contexts at each depth are computed by folding shifts over the origin — the path condition holds by construction.

• origin : C

  The root context (speech-act context)

• shifts : List (ContextShift C)

  Shifts from outermost to innermost. shifts[0] is the first embedding (e.g., the matrix attitude verb); the last element is the deepest.

def Core.Context.ContextTower.depth {C : Type u_1} (t : ContextTower C) : ℕ

Embedding depth (number of shifts).

Equations

• t.depth = t.shifts.length

def Core.Context.ContextTower.contextAt {C : Type u_1} (t : ContextTower C) (k : ℕ) : C

The context at depth k, computed by folding the first k shifts over the origin. Saturates at tower depth: contextAt k for k ≥ depth returns the innermost context.

• contextAt 0 = origin
• contextAt depth = innermost

Equations

• t.contextAt k = List.foldl (fun (c : C) (σ : Core.Context.ContextShift C) => σ.apply c) t.origin (List.take k t.shifts)

def Core.Context.ContextTower.innermost {C : Type u_1} (t : ContextTower C) : C

The innermost (most deeply embedded) context: fold all shifts over origin.

Equations

• t.innermost = List.foldl (fun (c : C) (σ : Core.Context.ContextShift C) => σ.apply c) t.origin t.shifts

def Core.Context.ContextTower.root {C : Type u_1} (c : C) : ContextTower C

Trivial tower with no shifts.

Equations

• Core.Context.ContextTower.root c = { origin := c, shifts := [] }

def Core.Context.ContextTower.push {C : Type u_1} (t : ContextTower C) (σ : ContextShift C) : ContextTower C

Push a new shift onto the tower (embed one level deeper).

Equations

• t.push σ = { origin := t.origin, shifts := t.shifts ++ [σ] }

@[simp]

theorem Core.Context.ContextTower.root_origin {C : Type u_1} (c : C) : (root c).origin = c

@[simp]

theorem Core.Context.ContextTower.root_innermost {C : Type u_1} (c : C) : (root c).innermost = c

@[simp]

theorem Core.Context.ContextTower.contextAt_zero {C : Type u_1} (t : ContextTower C) : t.contextAt 0 = t.origin

@[simp]

theorem Core.Context.ContextTower.contextAt_depth {C : Type u_1} (t : ContextTower C) : t.contextAt t.depth = t.innermost

theorem Core.Context.ContextTower.contextAt_saturates {C : Type u_1} (t : ContextTower C) (k : ℕ) (hk : t.depth ≤ k) : t.contextAt k = t.innermost

Past the tower depth, contextAt saturates at the innermost context. This is because List.take k on a list shorter than k returns the whole list.

@[simp]

theorem Core.Context.ContextTower.push_origin {C : Type u_1} (t : ContextTower C) (σ : ContextShift C) : (t.push σ).origin = t.origin

@[simp]

theorem Core.Context.ContextTower.root_depth {C : Type u_1} (c : C) : (root c).depth = 0

@[simp]

theorem Core.Context.ContextTower.push_depth {C : Type u_1} (t : ContextTower C) (σ : ContextShift C) : (t.push σ).depth = t.depth + 1

@[simp]

theorem Core.Context.ContextTower.root_contextAt {C : Type u_1} (c : C) (k : ℕ) : (root c).contextAt k = c

@[simp]

theorem Core.Context.ContextTower.push_innermost {C : Type u_1} (t : ContextTower C) (σ : ContextShift C) : (t.push σ).innermost = σ.apply t.innermost

Pushing a shift updates the innermost context.

inductive Core.Context.DepthSpec : Type

Which depth to read from in a tower.

• .origin: always read from depth 0 (speech-act context)
• .local: always read from the innermost context
• .relative k: read from depth k

• origin : DepthSpec
• local : DepthSpec
• relative (k : ℕ) : DepthSpec

def Core.Context.instDecidableEqDepthSpec.decEq (x✝ x✝¹ : DepthSpec) : Decidable (x✝ = x✝¹)

Equations

• Core.Context.instDecidableEqDepthSpec.decEq Core.Context.DepthSpec.origin Core.Context.DepthSpec.origin = isTrue ⋯
• Core.Context.instDecidableEqDepthSpec.decEq Core.Context.DepthSpec.origin Core.Context.DepthSpec.local = isFalse Core.Context.instDecidableEqDepthSpec.decEq._proof_1
• Core.Context.instDecidableEqDepthSpec.decEq Core.Context.DepthSpec.origin (Core.Context.DepthSpec.relative k) = isFalse ⋯
• Core.Context.instDecidableEqDepthSpec.decEq Core.Context.DepthSpec.local Core.Context.DepthSpec.origin = isFalse Core.Context.instDecidableEqDepthSpec.decEq._proof_3
• Core.Context.instDecidableEqDepthSpec.decEq Core.Context.DepthSpec.local Core.Context.DepthSpec.local = isTrue ⋯
• Core.Context.instDecidableEqDepthSpec.decEq Core.Context.DepthSpec.local (Core.Context.DepthSpec.relative k) = isFalse ⋯
• Core.Context.instDecidableEqDepthSpec.decEq (Core.Context.DepthSpec.relative k) Core.Context.DepthSpec.origin = isFalse ⋯
• Core.Context.instDecidableEqDepthSpec.decEq (Core.Context.DepthSpec.relative k) Core.Context.DepthSpec.local = isFalse ⋯
• Core.Context.instDecidableEqDepthSpec.decEq (Core.Context.DepthSpec.relative a) (Core.Context.DepthSpec.relative b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Core.Context.instDecidableEqDepthSpec : DecidableEq DepthSpec

Equations

• Core.Context.instDecidableEqDepthSpec = Core.Context.instDecidableEqDepthSpec.decEq

def Core.Context.instReprDepthSpec.repr : DepthSpec → ℕ → Std.Format

Equations

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

instance Core.Context.instReprDepthSpec : Repr DepthSpec

Equations

• Core.Context.instReprDepthSpec = { reprPrec := Core.Context.instReprDepthSpec.repr }

def Core.Context.instBEqDepthSpec.beq : DepthSpec → DepthSpec → Bool

Equations

• Core.Context.instBEqDepthSpec.beq Core.Context.DepthSpec.origin Core.Context.DepthSpec.origin = true
• Core.Context.instBEqDepthSpec.beq Core.Context.DepthSpec.local Core.Context.DepthSpec.local = true
• Core.Context.instBEqDepthSpec.beq (Core.Context.DepthSpec.relative a) (Core.Context.DepthSpec.relative b) = (a == b)
• Core.Context.instBEqDepthSpec.beq x✝¹ x✝ = false

instance Core.Context.instBEqDepthSpec : BEq DepthSpec

Equations

• Core.Context.instBEqDepthSpec = { beq := Core.Context.instBEqDepthSpec.beq }

def Core.Context.instInhabitedDepthSpec.default : DepthSpec

Equations

• Core.Context.instInhabitedDepthSpec.default = Core.Context.DepthSpec.origin

instance Core.Context.instInhabitedDepthSpec : Inhabited DepthSpec

Equations

• Core.Context.instInhabitedDepthSpec = { default := Core.Context.instInhabitedDepthSpec.default }

def Core.Context.DepthSpec.resolve (d : DepthSpec) (towerDepth : ℕ) : ℕ

Resolve to a concrete depth index given the tower depth.

Equations

• Core.Context.DepthSpec.origin.resolve towerDepth = 0
• Core.Context.DepthSpec.local.resolve towerDepth = towerDepth
• (Core.Context.DepthSpec.relative a).resolve towerDepth = a

@[simp]

theorem Core.Context.DepthSpec.origin_resolve (n : ℕ) : origin.resolve n = 0

@[simp]

theorem Core.Context.DepthSpec.local_resolve (n : ℕ) : «local».resolve n = n

@[simp]

theorem Core.Context.DepthSpec.relative_resolve (k n : ℕ) : (relative k).resolve n = k

structure Core.Context.AccessPattern (C : Type u_1) (R : Type u_2) : Type (max u_1 u_2)

An access pattern: a depth specification plus a projection from context to value.

This is how context-dependent expressions specify what they read:

• depth says which tower layer to read from
• project says which coordinate to extract

English "I" = ⟨.origin, KContext.agent⟩ Amharic "I" = ⟨.local, KContext.agent⟩ English "now" = ⟨.origin, KContext.time⟩

• depth : DepthSpec

  Which depth to read from

• project : C → R

  Which coordinate to extract

def Core.Context.AccessPattern.resolve {C : Type u_1} {R : Type u_2} (ap : AccessPattern C R) (t : ContextTower C) : R

Resolve an access pattern against a tower.

Equations

• ap.resolve t = ap.project (t.contextAt (ap.depth.resolve t.depth))

def Core.Context.AccessPattern.map {C : Type u_1} {R : Type u_2} {S : Type u_3} (ap : AccessPattern C R) (f : R → S) : AccessPattern C S

Map a function over the projected result.

Equations

• ap.map f = { depth := ap.depth, project := f ∘ ap.project }

theorem Core.Context.AccessPattern.origin_stable {C : Type u_1} {R : Type u_2} (ap : AccessPattern C R) (hd : ap.depth = DepthSpec.origin) (t : ContextTower C) (σ : ContextShift C) : ap.resolve (t.push σ) = ap.resolve t

Origin access is invariant under push. This is the formal content of Kaplan's thesis: expressions reading from the speech-act context are unaffected by embedding operators.

theorem Core.Context.AccessPattern.local_updates {C : Type u_1} {R : Type u_2} (ap : AccessPattern C R) (hd : ap.depth = DepthSpec.local) (t : ContextTower C) (σ : ContextShift C) : ap.resolve (t.push σ) = ap.project (σ.apply t.innermost)

Local access updates with push: the innermost projection tracks the new shift.

theorem Core.Context.AccessPattern.root_origin_eq_local {C : Type u_1} {R : Type u_2} (ap₁ ap₂ : AccessPattern C R) (h₁ : ap₁.depth = DepthSpec.origin) (h₂ : ap₂.depth = DepthSpec.local) (hProj : ap₁.project = ap₂.project) (c : C) : ap₁.resolve (ContextTower.root c) = ap₂.resolve (ContextTower.root c)

In a root tower, origin and local access agree.