Docs / Semantics / Reference / Context / Tower

Context towers

import Linglib.Semantics.Reference.Context.Tower

A context tower is an origin, Kaplan's speech-act context, with the contexts bound by the embeddings above an expression, from outermost to innermost; an expression reads a coordinate of the context at some depth. Kaplanian indexicals read the origin and shifted indexicals the innermost context. The origin survives every embedding, so an indexical can read it whatever the clauses between read: the binding account of indexical shift, against which Anand and Nevins argue that shifting overwrites the context.

Main definitions

ContextTower: an origin with its bound contexts; contextAt k is the k-th of them, innermost the last, and push binds one more.
ContextTower.AccessPattern: a depth, given relative to the tower, and a coordinate; AccessPattern.origin and AccessPattern.innermost.
AccessPattern.Stable: binding another context leaves the pattern's value unchanged.

Main results

push_innermost, push_contextAt_of_le: a push binds the innermost context alone.
AccessPattern.stable_origin, AccessPattern.stable_innermost_iff: a pattern reading the origin is stable, one reading the innermost context only if its coordinate is constant.

References

Kaplan 1989, Demonstratives formalized
Schlenker 2003, A Plea for Monsters formalized
Anand & Nevins 2004, Shifty Operators in Changing Contexts formalized

Declarations

A context tower is an origin with the contexts bound above it, from outermost to innermost.

structure ContextTower L46–51

(C : Type u_1) :

Type u_1

origin : C
The root context, the speech-act context.
bound : List C
The bound contexts, the first bound by the outermost embedding.

Used by ContextTower.depth, ContextTower.contextAt, ContextTower.innermost, ContextTower.root, ContextTower.push, ContextTower.contextAt_zero, ContextTower.push_origin, ContextTower.push_depth, ContextTower.push_innermost, ContextTower.contextAt_depth, ContextTower.contextAt_saturates, ContextTower.push_contextAt_of_le, ContextTower.push_contextAt_of_lt, ContextTower.push_contextAt_succ_depth, ContextTower.AccessPattern.resolve, ContextTower.AccessPattern.resolve_map, ContextTower.AccessPattern.origin_resolve, ContextTower.AccessPattern.innermost_resolve, ContextTower.AccessPattern.Stable

Used in AnandNevins2004, Schlenker2003

L57–58

The context at depth k is the k-th bound context, saturating at the innermost one.

def ContextTower.contextAt L60–61

{C : Type u_1} (t : ContextTower C) (k : ℕ) :

t.contextAt k = (List.take k t.bound).getLastD t.origin

Built from

Used by ContextTower.root_contextAt, ContextTower.contextAt_zero, ContextTower.contextAt_depth, ContextTower.contextAt_saturates, ContextTower.push_contextAt_of_le, ContextTower.push_contextAt_of_lt, ContextTower.push_contextAt_succ_depth, ContextTower.AccessPattern.resolve

Used in AnandNevins2004

The innermost context is the last bound context.

def ContextTower.innermost L63–64

{C : Type u_1} (t : ContextTower C) :

t.innermost = t.bound.getLastD t.origin

Built from

Used by ContextTower.root_innermost, ContextTower.push_innermost, ContextTower.contextAt_depth, ContextTower.contextAt_saturates, ContextTower.AccessPattern.innermost_resolve

Used in AnandNevins2004, Schlenker2003

L66–67

Embed one level deeper, binding c.

def ContextTower.push L69–70

{C : Type u_1} (t : ContextTower C) (c : C) :

ContextTower C

t.push c = { origin := t.origin, bound := t.bound ++ [c] }

Built from

Used by ContextTower.push_origin, ContextTower.push_depth, ContextTower.push_innermost, ContextTower.push_contextAt_of_le, ContextTower.push_contextAt_of_lt, ContextTower.push_contextAt_succ_depth, ContextTower.AccessPattern.Stable

Used in Schlenker2003

@[simp] theorem ContextTower.push_innermost L79

{C : Type u_1} (t : ContextTower C) (c : C) :

(t.push c).innermost = c

Built from , ,

L81–82

L84–86

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

theorem ContextTower.push_contextAt_of_le L88–91

{C : Type u_1} (t : ContextTower C) (c : C) {k : ℕ} (hk : k ≤ t.depth) :

(t.push c).contextAt k = t.contextAt k

Built from , , ,

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

structure ContextTower.AccessPattern L126–133

(C : Type u_1) (R : Type u_2) :

Type (max u_1 u_2)

depth : DepthSpec
Which depth to read from.
project : C → R
Which coordinate to extract.

Built from

Used by ContextTower.AccessPattern.resolve, ContextTower.AccessPattern.instFunctor, ContextTower.AccessPattern.instLawfulFunctor, ContextTower.AccessPattern.map_depth, ContextTower.AccessPattern.map_project, ContextTower.AccessPattern.resolve_map, ContextTower.AccessPattern.origin, ContextTower.AccessPattern.innermost, ContextTower.AccessPattern.Stable

Used in Semantics/Reference/Kaplan, Schlenker2003

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

def ContextTower.AccessPattern.origin L160–161

{C : Type u_1} {R : Type u_2} (f : C → R) :

AccessPattern C R

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

Built from

Used by ContextTower.AccessPattern.origin_resolve, ContextTower.AccessPattern.stable_origin

Used in Semantics/Reference/Kaplan

A shifted indexical reads the coordinate f of the innermost context.

def ContextTower.AccessPattern.innermost L163–164

{C : Type u_1} {R : Type u_2} (f : C → R) :

AccessPattern C R

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

Built from

Used by ContextTower.AccessPattern.innermost_resolve, ContextTower.AccessPattern.stable_innermost_iff

Used in Schlenker2003

L166

L168–169

An access pattern is stable when binding another context on any tower leaves its resolution unchanged: Kaplan's thesis for the indexicals of English, and the Fixity Thesis of Schlenker.

def ContextTower.AccessPattern.Stable L171–173

{C : Type u_1} {R : Type u_2} (ap : AccessPattern C R) :

Prop

ap.Stable = ∀ (t : ContextTower C) (c : C), ap.resolve (t.push c) = ap.resolve t

Built from , , ,

Used by ContextTower.AccessPattern.stable_origin, ContextTower.AccessPattern.stable_innermost_iff

Used in Schlenker2003

A pattern reading the speech-act context is stable.

theorem ContextTower.AccessPattern.stable_origin L175–176

{C : Type u_1} {R : Type u_2} (f : C → R) :

(origin f).Stable

Built from ,

A pattern reading the innermost context is stable iff its coordinate is constant.

theorem ContextTower.AccessPattern.stable_innermost_iff L178–180

{C : Type u_1} {R : Type u_2} (f : C → R) :

(innermost f).Stable ↔ ∀ (c c' : C), f c = f c'

Built from ,