Anand & Nevins 2004: shifty operators in changing contexts

In Zazaki every indexical may shift under vano 'say', and in Slave first-person indexicals shift under hadi, yet indexicals in one speech-context domain never take their values from different contexts (Shift-Together); in Slave the embedding verb decides which indexicals shift and whether they must; and under two stacked reports a shifted indexical in the intermediate clause blocks the lowest indexical from reaching the utterance context. The account: Kaplan's context and index parameters are made the same type, an attitude verb quantifies over indices, and a language's context-shifting operators overwrite the context from the index — all of it in Zazaki, the author coordinate alone in Slave — so shifting is literal overwriting, whence Shift-Together and the loss of the utterance context under an intermediate shift; lexical entries pair verbs with operator options.

Main definitions

• Params: the context–index pair; I, you, here, now read the context, proSubj and logAddr the index.
• Op: the context-shifting operators (2); attitude is (23b).
• Entry: a verb's operator options (39); readings, readings₂ the values an indexical can take under one or two reports.

References

• [AN04b]
• [Kap89] — context and index
• [Sch03a] — the lexical-underspecification rival and the Amharic data
• [Sta78] — Op.all as the diagonal operator

Two parameters of the same type

@[reducible, inline]

abbrev AnandNevins2004.Params (W : Type u_5) (E : Type u_6) (P : Type u_7) (T : Type u_8) : Type (max (max (max u_8 u_7) u_6) u_5)

Kaplan's context and index, both of context type (§3.1).

Equations

• AnandNevins2004.Params W E P T = (Reference.Context W E P T × Reference.Context W E P T)

@[reducible, inline]

abbrev AnandNevins2004.Expr (W : Type u_5) (E : Type u_6) (P : Type u_7) (T : Type u_8) (R : Type u_9) : Type (max (max (max (max u_9 u_8) u_7) u_6) u_5)

An expression interpreted relative to the two parameters.

Equations

• AnandNevins2004.Expr W E P T R = (AnandNevins2004.Params W E P T → R)

def AnandNevins2004.I {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Expr W E P T E

The indexicals read the context parameter (24).

Equations

• AnandNevins2004.I p = p.1.agent

def AnandNevins2004.you {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Expr W E P T E

Equations

• AnandNevins2004.you p = p.1.addressee

def AnandNevins2004.here {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Expr W E P T P

Equations

• AnandNevins2004.here p = p.1.position

def AnandNevins2004.now {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Expr W E P T T

Equations

• AnandNevins2004.now p = p.1.time

def AnandNevins2004.proSubj {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Expr W E P T E

Subject-controlled PRO reads the author of the index (41); the logophors read its author and addressee (43).

Equations

• AnandNevins2004.proSubj p = p.2.agent

def AnandNevins2004.logAddr {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Expr W E P T E

Equations

• AnandNevins2004.logAddr p = p.2.addressee

inductive AnandNevins2004.Op : Type

The context-shifting operators (2): none, Zazaki's all overwriting every coordinate of the context with the index, and Slave's auth overwriting the author coordinate alone.

• none : Op
• all : Op
• auth : Op

@[instance_reducible]

instance AnandNevins2004.instDecidableEqOp : DecidableEq Op

Equations

• AnandNevins2004.instDecidableEqOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AnandNevins2004.Op.act {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Op → Params W E P T → Params W E P T

The rewriting an operator performs on the parameters.

Equations

• One or more equations did not get rendered due to their size.
• AnandNevins2004.Op.none.act = id
• AnandNevins2004.Op.all.act = fun (p : AnandNevins2004.Params W E P T) => (p.2, p.2)

def AnandNevins2004.attitude {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (acc : E → Reference.Context W E P T → Set (Reference.Context W E P T)) (x : E) (φ : Expr W E P T Prop) : Expr W E P T Prop

(23b): an attitude verb quantifies over the indices compatible with the attitude and leaves the context parameter untouched.

Equations

• AnandNevins2004.attitude acc x φ p = ∀ j ∈ acc x p.2, φ (p.1, j)

theorem AnandNevins2004.attitude_all {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (acc : E → Reference.Context W E P T → Set (Reference.Context W E P T)) (x : E) (φ : Expr W E P T Prop) (p : Params W E P T) : attitude acc x (φ ∘ Op.all.act) p ↔ ∀ j ∈ acc x p.2, φ (j, j)

(26)–(28): with all as sister of say, the complement is evaluated at the reported context alone, so every indexical in it shifts together.

theorem AnandNevins2004.I_auth {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (p : Params W E P T) : I (Op.auth.act p) = p.2.agent

(30): under auth the first person reads the reported author while the second person keeps the utterance addressee.

theorem AnandNevins2004.you_auth {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (p : Params W E P T) : you (Op.auth.act p) = p.1.addressee

theorem AnandNevins2004.I_all_eq_proSubj {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : I ∘ Op.all.act = proSubj

A shifted first person is read de se: under all it coincides with PRO (§5.1).

Lexical entries and readings

@[reducible, inline]

abbrev AnandNevins2004.Entry : Type

A verb's operator options (39): Zazaki vano and Slave TELL take all optionally, Slave WANT takes auth optionally, Slave SAY takes auth obligatorily, and the other Zazaki attitude verbs take none (fn. 3).

Equations

• AnandNevins2004.Entry = List AnandNevins2004.Op

def AnandNevins2004.vano : Entry

Equations

• AnandNevins2004.vano = [AnandNevins2004.Op.none, AnandNevins2004.Op.all]

def AnandNevins2004.zazakiAttitude : Entry

Equations

• AnandNevins2004.zazakiAttitude = [AnandNevins2004.Op.none]

def AnandNevins2004.slaveTell : Entry

Equations

• AnandNevins2004.slaveTell = [AnandNevins2004.Op.none, AnandNevins2004.Op.all]

def AnandNevins2004.slaveWant : Entry

Equations

• AnandNevins2004.slaveWant = [AnandNevins2004.Op.none, AnandNevins2004.Op.auth]

def AnandNevins2004.slaveSay : Entry

Equations

• AnandNevins2004.slaveSay = [AnandNevins2004.Op.auth]

def AnandNevins2004.readings {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {R : Type u_5} (e : Entry) (φ : Expr W E P T R) (c j : Reference.Context W E P T) : List R

The values an expression takes under a report with context c and reported context j, one per operator option.

Equations

• AnandNevins2004.readings e φ c j = List.map (fun (o : AnandNevins2004.Op) => φ (o.act (c, j))) e

theorem AnandNevins2004.readings_vano_I_you {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c j : Reference.Context W E P T) : readings vano (fun (p : Params W E P T) => (I p, you p)) c j = [(c.agent, c.addressee), (j.agent, j.addressee)]

(13): the first and second person under vano read from the same context — the two mixed pairs are not among the readings.

theorem AnandNevins2004.mixed_notMem_readings_vano {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {c j : Reference.Context W E P T} (ha : c.agent ≠ j.agent) (hb : c.addressee ≠ j.addressee) : (c.agent, j.addressee) ∉ readings vano (fun (p : Params W E P T) => (I p, you p)) c j ∧ (j.agent, c.addressee) ∉ readings vano (fun (p : Params W E P T) => (I p, you p)) c j

theorem AnandNevins2004.readings_slaveSay {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c j : Reference.Context W E P T) : readings slaveSay (fun (p : Params W E P T) => (I p, you p)) c j = [(j.agent, c.addressee)]

(17), (38b): under Slave SAY the first person is the reported author and the second the utterance addressee, obligatorily.

theorem AnandNevins2004.readings_slaveTell {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c j : Reference.Context W E P T) : readings slaveTell (fun (p : Params W E P T) => (I p, you p)) c j = [(c.agent, c.addressee), (j.agent, j.addressee)]

(36): under Slave TELL both persons shift together.

theorem AnandNevins2004.readings_slaveWant {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c j : Reference.Context W E P T) : readings slaveWant (fun (p : Params W E P T) => (I p, you p)) c j = [(c.agent, c.addressee), (j.agent, c.addressee)]

(37), (38a): under Slave WANT the first person shifts optionally and the second never.

Multiple embedding

theorem AnandNevins2004.opAll_forgets {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c c' j : Reference.Context W E P T) : (Op.all.act (c, j)).1 = (Op.all.act (c', j)).1

Overwriting loses the utterance context (§3.4): after all, the context no longer depends on what it was.

def AnandNevins2004.readings₂ {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {R : Type u_5} (e₁ e₂ : Entry) (φ : Expr W E P T R) (c j₁ j₂ : Reference.Context W E P T) : List R

Two stacked reports with reported contexts j₁ (intermediate) and j₂ (lowest): the values of an expression in the lowest clause, one per pair of operator options.

Equations

• AnandNevins2004.readings₂ e₁ e₂ φ c j₁ j₂ = List.flatMap (fun (o₁ : AnandNevins2004.Op) => List.map (fun (o₂ : AnandNevins2004.Op) => φ (o₂.act ((o₁.act (c, j₁)).1, j₂))) e₂) e₁

theorem AnandNevins2004.readings₂_vano_I {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c j₁ j₂ : Reference.Context W E P T) : readings₂ vano vano I c j₁ j₂ = [c.agent, j₂.agent, j₁.agent, j₂.agent]

(33): with nothing forcing a shift in the intermediate clause, the lowest first person may read the utterance author.

theorem AnandNevins2004.lowerI_of_shifted_you {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {c j₁ j₂ : Reference.Context W E P T} {o₁ o₂ : Op} (h₁ : o₁ ∈ vano) (h₂ : o₂ ∈ vano) (hyou : you (o₁.act (c, j₁)) = j₁.addressee) (hne : c.addressee ≠ j₁.addressee) : I (o₂.act ((o₁.act (c, j₁)).1, j₂)) ∈ [j₁.agent, j₂.agent]

(32): a shifted second person in the intermediate clause diagnoses all there, after which the lowest first person can only be the intermediate or the lowest reported author — never the utterance author.

The paper's examples

def AnandNevins2004.Op.shifts (o : Op) (coord : Reference.Context Bool Bool Bool Bool → Bool) : Bool

Whether an operator makes a coordinate read the reported context: the coordinate's value after the operator on the distinguishing pair of contexts.

Equations

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

def AnandNevins2004.Entry.ofString? : String → Option Entry

Equations

• AnandNevins2004.Entry.ofString? "vano" = some AnandNevins2004.vano
• AnandNevins2004.Entry.ofString? "zazaki_attitude" = some AnandNevins2004.zazakiAttitude
• AnandNevins2004.Entry.ofString? "slave_tell" = some AnandNevins2004.slaveTell
• AnandNevins2004.Entry.ofString? "slave_want" = some AnandNevins2004.slaveWant
• AnandNevins2004.Entry.ofString? "slave_say" = some AnandNevins2004.slaveSay
• AnandNevins2004.Entry.ofString? x✝ = none

def AnandNevins2004.coordOfString? : String → Option (Reference.Context Bool Bool Bool Bool → Bool)

Equations

• AnandNevins2004.coordOfString? "I" = some Reference.Context.agent
• AnandNevins2004.coordOfString? "you" = some Reference.Context.addressee
• AnandNevins2004.coordOfString? "here" = some Reference.Context.position
• AnandNevins2004.coordOfString? "now" = some Reference.Context.time
• AnandNevins2004.coordOfString? x✝ = none

theorem AnandNevins2004.rows_track_entries (r : Datum) : r ∈ Examples.all → r.feature? "pragmatic_clash" = none → ∀ e ∈ ((r.feature? "entry").bind Entry.ofString?).toList, ∀ coord ∈ ((r.feature? "indexical").bind coordOfString?).toList, ∀ x ∈ r.readings, (x.1 = "reported context" → (x.2 = Judgment.acceptable ↔ ∃ o ∈ e, o.shifts coord = true)) ∧ (x.1 = "utterance context" → (x.2 = Judgment.acceptable ↔ ∃ o ∈ e, o.shifts coord = false))

Every recorded reading of a single embedded indexical is available exactly when some operator option of the embedding verb's entry gives it: the reported-context reading when an option shifts the coordinate, the utterance-context reading when one does not.

theorem AnandNevins2004.rows_shift_together (r : Datum) : r ∈ Examples.all → r.feature? "test" = some "shift_together" → ∀ x ∈ r.readings, x.1.startsWith "mixed" = true → x.2 = Judgment.unacceptable

Shift-Together (16): wherever the paper lists mixed readings, they are unacceptable.