Context towers

A depth-indexed stack of context shifts over an origin, the one carrier for the context-manipulation mechanisms of [abusch-1997], [anand-nevins-2004], [cumming-2026] and [schlenker-2003]: Kaplanian indexicals read the origin, shifted indexicals the innermost context, De Bruijn temporal indexing a relative depth. A shift is an endomorphism of the context type, an element of the monoid Function.End C acting on contexts, and a tower is an origin, Kaplan's speech-act context, with its shifts from outermost to innermost (ContextTower). The context at depth k is the product of the first k shifts acting on the origin (ContextTower.contextAt), saturating at the innermost context (ContextTower.innermost), and pushing a shift multiplies it in (ContextTower.push, push_innermost). An access pattern reads a coordinate of the context at a depth given relative to the tower (AccessPattern, DepthSpec); AccessPattern.origin reads the speech-act context and AccessPattern.innermost the innermost one, and a pattern is stable under a shift when pushing it changes nothing (AccessPattern.Stable), which every origin pattern is (AccessPattern.stable_origin).

References

• [kaplan-1989]
• [schlenker-2003]
• [anand-nevins-2004]
• [abusch-1997]
• [cumming-2026]

structure Reference.ContextTower (C : Type u_1) : Type u_1

A context tower: an origin with a stack of shifts, from outermost to innermost.

• origin : C

  The root context, the speech-act context.

• shifts : List (Function.End C)

  The shifts, the first being the outermost embedding.

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

The embedding depth: the number of shifts.

Equations

• t.depth = t.shifts.length

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

The context at depth k: the first k shifts acting on the origin, saturating at the innermost context.

Equations

• t.contextAt k = (List.take k t.shifts).reverse.prod • t.origin

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

The innermost context: every shift acting on the origin.

Equations

• t.innermost = t.shifts.reverse.prod • t.origin

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

The trivial tower over a context.

Equations

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

def Reference.ContextTower.push {C : Type u_1} (t : ContextTower C) (σ : Function.End C) : ContextTower C

Embed one level deeper.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Reference.ContextTower.push_origin {C : Type u_1} (t : ContextTower C) (σ : Function.End C) : (t.push σ).origin = t.origin

@[simp]

theorem Reference.ContextTower.push_depth {C : Type u_1} (t : ContextTower C) (σ : Function.End C) : (t.push σ).depth = t.depth + 1

@[simp]

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

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

@[simp]

theorem Reference.ContextTower.push_innermost {C : Type u_1} (t : ContextTower C) (σ : Function.End C) : (t.push σ).innermost = σ • t.innermost

Pushing a shift lets it act on the innermost context.

theorem Reference.ContextTower.push_contextAt_of_le {C : Type u_1} (t : ContextTower C) (σ : Function.End C) {k : ℕ} (hk : k ≤ t.depth) : (t.push σ).contextAt k = t.contextAt k

Below the tower depth, a push leaves the context at each depth unchanged.

theorem Reference.ContextTower.push_contextAt_of_lt {C : Type u_1} (t : ContextTower C) (σ : Function.End C) {k : ℕ} (hk : t.depth < k) : (t.push σ).contextAt k = σ • t.innermost

Beyond the tower depth, a push saturates at the shifted innermost context.

@[simp]

theorem Reference.ContextTower.push_contextAt_succ_depth {C : Type u_1} (t : ContextTower C) (σ : Function.End C) : (t.push σ).contextAt (t.depth + 1) = σ • t.innermost

inductive Reference.DepthSpec : Type

Which depth of a tower an expression reads: the origin, the innermost context, or a fixed depth.

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

@[instance_reducible]

instance Reference.instDecidableEqDepthSpec : DecidableEq DepthSpec

Equations

• Reference.instDecidableEqDepthSpec = Reference.instDecidableEqDepthSpec.decEq

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

Equations

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

@[instance_reducible]

instance Reference.instReprDepthSpec : Repr DepthSpec

Equations

• Reference.instReprDepthSpec = { reprPrec := Reference.instReprDepthSpec.repr }

def Reference.instReprDepthSpec.repr : DepthSpec → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Reference.instReprDepthSpec.repr Reference.DepthSpec.origin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reference.DepthSpec.origin")).group prec✝
• Reference.instReprDepthSpec.repr Reference.DepthSpec.local prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reference.DepthSpec.local")).group prec✝

@[instance_reducible]

instance Reference.instInhabitedDepthSpec : Inhabited DepthSpec

Equations

• Reference.instInhabitedDepthSpec = { default := Reference.instInhabitedDepthSpec.default }

def Reference.DepthSpec.resolve (d : DepthSpec) (towerDepth : ℕ) : ℕ

The depth read at a tower of the given depth.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

An access pattern: a depth specification and a projection, what a context-dependent expression reads. English I is origin Context.agent; Amharic I is innermost Context.agent.

• depth : DepthSpec

  Which depth to read from.

• project : C → R

  Which coordinate to extract.

def Reference.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))

@[instance_reducible]

instance Reference.AccessPattern.instFunctor {C : Type u_1} : Functor (AccessPattern C)

Equations

• Reference.AccessPattern.instFunctor = { map := fun {α β : Type ?u.1} (f : α → β) (ap : Reference.AccessPattern C α) => { depth := ap.depth, project := f ∘ ap.project } }

instance Reference.AccessPattern.instLawfulFunctor {C : Type u_1} : LawfulFunctor (AccessPattern C)

@[simp]

theorem Reference.AccessPattern.map_depth {C : Type u_1} {R S : Type u} (ap : AccessPattern C R) (g : R → S) : (g <$> ap).depth = ap.depth

@[simp]

theorem Reference.AccessPattern.map_project {C : Type u_1} {R S : Type u} (ap : AccessPattern C R) (g : R → S) : (g <$> ap).project = g ∘ ap.project

@[simp]

theorem Reference.AccessPattern.resolve_map {C : Type u_1} (t : ContextTower C) {R S : Type u} (ap : AccessPattern C R) (g : R → S) : (g <$> ap).resolve t = g (ap.resolve t)

def Reference.AccessPattern.origin {C : Type u_1} {R : Type u_2} (f : C → R) : AccessPattern C R

Read the coordinate f of the speech-act context: a Kaplanian pure indexical.

Equations

• Reference.AccessPattern.origin f = { depth := Reference.DepthSpec.origin, project := f }

def Reference.AccessPattern.innermost {C : Type u_1} {R : Type u_2} (f : C → R) : AccessPattern C R

Read the coordinate f of the innermost context: a shifted indexical.

Equations

• Reference.AccessPattern.innermost f = { depth := Reference.DepthSpec.local, project := f }

@[simp]

theorem Reference.AccessPattern.origin_resolve {C : Type u_1} {R : Type u_2} (t : ContextTower C) (f : C → R) : (origin f).resolve t = f t.origin

@[simp]

theorem Reference.AccessPattern.innermost_resolve {C : Type u_1} {R : Type u_2} (t : ContextTower C) (f : C → R) : (innermost f).resolve t = f t.innermost

def Reference.AccessPattern.Stable {C : Type u_1} {R : Type u_2} (ap : AccessPattern C R) (σ : Function.End C) : Prop

An access pattern is stable under a shift when pushing the shift onto any tower leaves its resolution unchanged. Kaplan-compliance is stability under every shift and monsterhood instability of some pattern (Reference/Kaplan.lean).

Equations

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

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

Origin access is invariant under push: Kaplan's thesis for expressions reading the speech-act context.

theorem Reference.AccessPattern.stable_of_depth_origin {C : Type u_1} {R : Type u_2} (ap : AccessPattern C R) (hd : ap.depth = DepthSpec.origin) (σ : Function.End C) : ap.Stable σ

theorem Reference.AccessPattern.stable_origin {C : Type u_1} {R : Type u_2} (f : C → R) (σ : Function.End C) : (origin f).Stable σ

theorem Reference.AccessPattern.local_updates {C : Type u_1} {R : Type u_2} (ap : AccessPattern C R) (hd : ap.depth = DepthSpec.local) (t : ContextTower C) (σ : Function.End C) : ap.resolve (t.push σ) = ap.project (σ • t.innermost)

Innermost access tracks the pushed shift.