Context Tower

[Abu97] [AN04b] [Cum26] [Sch03]

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 Semantics.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

@[implicit_reducible]

instance Semantics.Context.instDecidableEqShiftLabel : DecidableEq ShiftLabel

Equations

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

@[implicit_reducible]

instance Semantics.Context.instReprShiftLabel : Repr ShiftLabel

Equations

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

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

Equations

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

@[implicit_reducible]

instance Semantics.Context.instInhabitedShiftLabel : Inhabited ShiftLabel

Equations

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

structure Semantics.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 Semantics.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 Semantics.Context.ContextTower.depth {C : Type u_1} (t : ContextTower C) : ℕ

Embedding depth (number of shifts).

Equations

• t.depth = t.shifts.length

def Semantics.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) (σ : Semantics.Context.ContextShift C) => σ.apply c) t.origin (List.take k t.shifts)

def Semantics.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) (σ : Semantics.Context.ContextShift C) => σ.apply c) t.origin t.shifts

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

Trivial tower with no shifts.

Equations

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

def Semantics.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 Semantics.Context.ContextTower.root_origin {C : Type u_1} (c : C) : (root c).origin = c

@[simp]

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

@[simp]

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

@[simp]

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

theorem Semantics.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 Semantics.Context.ContextTower.push_origin {C : Type u_1} (t : ContextTower C) (σ : ContextShift C) : (t.push σ).origin = t.origin

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Semantics.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 Semantics.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 Semantics.Context.instDecidableEqDepthSpec.decEq (x✝ x✝¹ : DepthSpec) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Semantics.Context.instDecidableEqDepthSpec : DecidableEq DepthSpec

Equations

• Semantics.Context.instDecidableEqDepthSpec = Semantics.Context.instDecidableEqDepthSpec.decEq

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

Equations

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

@[implicit_reducible]

instance Semantics.Context.instReprDepthSpec : Repr DepthSpec

Equations

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

@[implicit_reducible]

instance Semantics.Context.instInhabitedDepthSpec : Inhabited DepthSpec

Equations

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

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

Resolve to a concrete depth index given the tower depth.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

structure Semantics.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 Semantics.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 Semantics.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 Semantics.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 Semantics.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.

def Semantics.Context.AccessPattern.Stable {C : Type u_1} {R : Type u_2} (ap : AccessPattern C R) (σ : ContextShift C) : Prop

An access pattern is stable under a shift when pushing that shift onto any tower leaves its resolution unchanged. This relation underlies both Kaplan-compliance (Reference/Kaplan.lean: an expression stable under every shift) and monsterhood (Reference/Monsters.lean: a shift that destabilizes some expression) — the two are its ∀-over-shifts and ∃-over-expressions projections.

Equations

• ap.Stable σ = ∀ (t : Semantics.Context.ContextTower C), ap.resolve (t.push σ) = ap.resolve t

theorem Semantics.Context.AccessPattern.Stable_of_depth_origin {C : Type u_1} {R : Type u_2} (ap : AccessPattern C R) (hd : ap.depth = DepthSpec.origin) (σ : ContextShift C) : ap.Stable σ

Origin-depth access is stable under every shift — the access-pattern form of origin_stable, and the sufficient condition for Kaplan-compliance.

def Semantics.Context.AccessPattern.innermostReader (C : Type u_4) : AccessPattern C C

The canonical innermost reader: returns the innermost context verbatim (.local depth, identity projection). It is the universal witness for instability — a shift destabilizes some access pattern iff it destabilizes this one, because a push only ever changes the innermost context — so monsterhood is defined as its instability (Reference/Monsters.lean).

Equations

• Semantics.Context.AccessPattern.innermostReader C = { depth := Semantics.Context.DepthSpec.local, project := id }

@[simp]

theorem Semantics.Context.AccessPattern.innermostReader_resolve {C : Type u_1} (t : ContextTower C) : (innermostReader C).resolve t = t.innermost

def Semantics.Context.AccessPattern.toIntension {C : Type u_1} {R : Type u_2} (ap : AccessPattern C R) : Intensional.Intension (ContextTower C) R

Bridge to the substrate's Intension framework: an AccessPattern IS an Intension (ContextTower C) R via its resolve method. The substrate's Intension-based machinery (Intensional.Intension.IsRigid, IsRigidOn, the functoriality lemmas in Semantics/Intensional/Rigidity.lean) thereby applies to access patterns. The push-invariance of origin-depth access (origin_stable above) is the access-pattern analog of the substrate's IsRigidOn on tower-shift orbits.

Equations

• ap.toIntension = ap.resolve

@[simp]

theorem Semantics.Context.AccessPattern.toIntension_apply {C : Type u_1} {R : Type u_2} (ap : AccessPattern C R) (t : ContextTower C) : ap.toIntension t = ap.resolve t

theorem Semantics.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.