Docs / Semantics / Reference / Context / Overwrite

Overwriting coordinates of a context

import Linglib.Semantics.Reference.Context.Overwrite · namespace Kaplan

A context is the function from its coordinates to their values (Context.equivPi), and overwrite s c i is c with its coordinates in s taken from i, Finset.piecewise through that equivalence: the operation by which a shifty operator replaces coordinates of the context with those of an index of the same type. An indexical depends, in the sense of DependsOn, on one coordinate; after a sequence of overwrites it reads the context of the last overwrite that took that coordinate.

Main definitions

Context.Coord, Context.equivPi: the coordinates of a context, and the context as a function on them.
Context.overwrite s c i: c with the coordinates in s taken from i.
Context.localDepth ss k: the position of the last of the overwrites ss that takes k.
shiftyOp s: the shifty operator, evaluating its argument at the context overwritten from the index, Kaplan's shiftBy (overwrite s).

Main results

overwrite_overwrite: overwriting s and then t from the same context overwrites s ∪ t.
apply_overwrite_of_subset, apply_overwrite_of_disjoint: an expression reads the overwriting context when its coordinates are overwritten, the original one when none is.
apply_foldl_overwrite: Local Determination.
shiftyOp_shiftyOp, diag_shiftyOp: stacked shifty operators compose to the one overwriting the union of their coordinates, and unembedded a shifty operator is vacuous.

References

Anand & Nevins 2004, Shifty Operators in Changing Contexts formalized
Deal 2020, A Theory of Indexical Shift: Meaning, Grammar, and Crosslinguistic Variation formalized

Declarations

The coordinates of a context.

inductive Context.Coord L54–61

Type

agent : Coord
addressee : Coord
world : Coord
time : Coord
position : Coord

Derives DecidableEq, Fintype.

Used by Context.Coord.Carrier, Context.equivPi, Context.overwrite, Context.equivPi_overwrite, Context.overwrite_agent, Context.overwrite_addressee, Context.overwrite_world, Context.overwrite_time, Context.overwrite_position, Context.overwrite_self, Context.overwrite_overwrite, Context.apply_overwrite_of_subset, Context.apply_overwrite_of_disjoint, Context.apply_overwrite_of_apply_eq, Context.localDepth, Context.localDepth_nil, Context.localDepth_append_singleton, Context.localDepth_le_length, Context.apply_foldl_overwrite, shiftyOp, shiftyOp_apply, shiftyOp_shiftyOp, diag_shiftyOp

Used in AnandNevins2004, Deal2020

L63–68

A context is the function from its coordinates to their values.

def Context.equivPi L70–80

{W E P T : Type u} :

Context W E P T ≃ ((k : Coord) → Coord.Carrier W E P T k)

The definition is too large to print here; read it in the source.

Built from ,

Used by Context.overwrite, Context.equivPi_overwrite, Context.dependsOn_agent, Context.apply_overwrite_of_subset, Context.apply_overwrite_of_disjoint, Context.apply_overwrite_of_apply_eq, Context.apply_foldl_overwrite

Used in AnandNevins2004, Deal2020

The context c with the coordinates in s overwritten by those of i.

def Context.overwrite L82–84

{W E P T : Type u} (s : Finset Coord) (c i : Context W E P T) :

Context W E P T

Context.overwrite s c i = Context.equivPi.symm (s.piecewise (Context.equivPi i) (Context.equivPi c))

Built from ,

Used by Context.equivPi_overwrite, Context.overwrite_agent, Context.overwrite_addressee, Context.overwrite_world, Context.overwrite_time, Context.overwrite_position, Context.overwrite_empty, Context.overwrite_univ, Context.overwrite_self, Context.overwrite_overwrite, Context.apply_overwrite_of_subset, Context.apply_overwrite_of_disjoint, Context.apply_overwrite_of_apply_eq, Context.apply_foldl_overwrite, shiftyOp, shiftyOp_apply

Used in AnandNevins2004, Deal2020

Overwriting s and then t from the same context overwrites s ∪ t.

theorem Context.overwrite_overwrite L115–119

{W E P T : Type u} (s t : Finset Coord) (c i : Context W E P T) :

overwrite t (overwrite s c i) i = overwrite (s ∪ t) c i

Built from ,

Expressions reading some coordinates

L125–127

An expression reading only the coordinates s reads the overwriting context when they are all overwritten.

theorem Context.apply_overwrite_of_subset L131–137

{W E P T : Type u} {α : Type u_1} {f : Context W E P T → α} {s : Set Coord} {t : Finset Coord} (hf : DependsOn (f ∘ ⇑equivPi.symm) s) (h : s ⊆ ↑t) (c i : Context W E P T) :

f (overwrite t c i) = f i

Built from , ,

An expression reading only the coordinates s reads the original context when none of them is overwritten.

theorem Context.apply_overwrite_of_disjoint L139–145

{W E P T : Type u} {α : Type u_1} {f : Context W E P T → α} {s : Set Coord} {t : Finset Coord} (hf : DependsOn (f ∘ ⇑equivPi.symm) s) (h : Disjoint s ↑t) (c i : Context W E P T) :

f (overwrite t c i) = f c

Built from , ,

L147–153

Local Determination

The position, counting from one, of the last of the overwrites ss that takes the coordinate k, or 0 if none does.

def Context.localDepth L157–160

(ss : List (Finset Coord)) (k : Coord) :

ℕ

Context.localDepth ss k = List.foldl (fun (d : ℕ) (p : Finset Context.Coord × ℕ) => if k ∈ p.1 then p.2 + 1 else d) 0 ss.zipIdx

Built from

Used by Context.localDepth_nil, Context.localDepth_append_singleton, Context.localDepth_le_length, Context.apply_foldl_overwrite

Used in AnandNevins2004, Deal2020

L162

L164–166

L168–174

Local Determination: after overwrites by the pairs ops, outermost first, an expression reading only the coordinate k reads the context of the last pair that overwrites k, the last of the first localDepth overwriting contexts, or the original context if none does.

theorem Context.apply_foldl_overwrite L176–194

{W E P T : Type u} {α : Type u_1} {f : Context W E P T → α} {k : Coord} (hf : DependsOn (f ∘ ⇑equivPi.symm) {k}) (c : Context W E P T) (ops : List (Finset Coord × Context W E P T)) :

f (List.foldl (fun (c : Context W E P T) (p : Finset Coord × Context W E P T) => overwrite p.1 c p.2) c ops) = f ((List.take (localDepth (List.map Prod.fst ops) k) (List.map Prod.snd ops)).getLastD c)

Built from , , ,

The shifty operator overwriting the coordinates s of the context with those of the index, ⟦OP α⟧^{c,i} = ⟦α⟧^{overwrite s c i, i} (Anand & Nevins 2004, Deal 2020).

def shiftyOp L204–209

{W E P T : Type u} {α : Type u_1} (s : Finset Context.Coord) :

Character (Context W E P T) (Context W E P T) α → Character (Context W E P T) (Context W E P T) α

shiftyOp s = shiftBy (Context.overwrite s)

Built from ,

Used by shiftyOp_apply, shiftyOp_empty, shiftyOp_shiftyOp, diag_shiftyOp

Used in AnandNevins2004, Deal2020

L213–214

L216

Stacked shifty operators compose to the one overwriting the union of their coordinates.

@[simp] theorem shiftyOp_shiftyOp L218–220

{W E P T : Type u} {α : Type u_1} (s t : Finset Context.Coord) (χ : Character (Context W E P T) (Context W E P T) α) :

shiftyOp t (shiftyOp s χ) = shiftyOp (t ∪ s) χ

Built from ,

Unembedded, a shifty operator is vacuous: at a context taken as its own index, it has the value of its complement.

theorem diag_shiftyOp L222–225

{W E P T : Type u} {α : Type u_1} (s : Finset Context.Coord) (χ : Character (Context W E P T) (Context W E P T) α) :

Character.diag id (shiftyOp s χ) = Character.diag id χ

Built from ,