@cite{sidner-1983}: Focusing in the Comprehension of Definite Anaphora

@cite{sidner-1979}

Chapter 5 of @cite{sidner-1983} (originally in Brady & Berwick eds., Computational Models of Discourse, MIT Press), based on @cite{sidner-1979} (PhD thesis, MIT AI-TR-537).

Architectural difference from @cite{grosz-joshi-weinstein-1995}

@cite{grosz-joshi-weinstein-1995} §9 (p. 222) describes Sidner's account this way:

In Sidner's theory, each utterance provides an immediate discourse focus, an actor focus, and a set of potential foci. The discourse and actor foci may coincide, but need not. Her potential foci are roughly analogous to our C_f.

This makes the architectural contrast precise. Sidner does not have a Cf-ranker — she has a two-slot focus state (discourse focus + actor focus) plus an unranked set of potential foci. The two slots serve different roles in pronoun resolution: agent-position pronouns prefer the actor focus; non-agent-position pronouns prefer the discourse focus. This is fundamentally a different shape from GJW's single ranked Cf list and single Cb.

For this reason, this file does not instantiate Discourse.Centering.CfRanker. Sidner's account is a separate formalization, structurally orthogonal to the Centering substrate. The cross-framework comparison lives in Phenomena/Reference/Studies/GroszJoshiWeinstein1995.lean §8 (the chronologically-later paper, per linglib's chronological-dependency convention), which imports this file and proves the disagreement on GJW's example (34).

Scope

This file formalizes:

• The two-slot focus state (discourse focus + actor focus).
• The expected-focus algorithm for the discourse focus, from @cite{sidner-1983} §5.2.3 (p. 287). The thematic preference order is theme > other-non-agent > agent > VP — note that agent is ranked LAST among non-theme positions for discourse focus, and is picked separately as the actor focus. This is the opposite of what one might expect from a label-only reading of "thematic-role ranking" and is what makes the two-slot architecture coherent.
• The expected-focus algorithm for the actor focus (an analogous algorithm picking the agent, §5.2.3 p. 287).
• Sidner's pronoun-resolution rule: agent-position pronouns co-specify the actor focus; non-agent pronouns co-specify the discourse focus (§5.2.6 step 3, p. 293).
• Application to GJW example (34) at the bottom of the file.

The full focusing algorithm has 10 steps (§5.2.6 pp. 292-294) involving the alternate-focus list, focus stack, do-anaphora rule, and implicit specification. That full machinery is not formalized here — only the rules load-bearing for the GJW example (34) disagreement. A future expansion could formalize the rest if it becomes necessary for some downstream consumer.

inductive Sidner1983.Position : Type

A noun-phrase slot's syntactic position. Sidner's pronoun rule (§5.2.6 step 3) splits on agent vs. non-agent position, so the binary distinction is what matters for the formalization.

• agent : Position
• nonAgent : Position

@[implicit_reducible]

instance Sidner1983.instDecidableEqPosition : DecidableEq Position

Equations

• Sidner1983.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Sidner1983.instReprPosition : Repr Position

Equations

• Sidner1983.instReprPosition = { reprPrec := Sidner1983.instReprPosition.repr }

def Sidner1983.instReprPosition.repr : Position → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Sidner1983.instReprPosition.repr Sidner1983.Position.agent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sidner1983.Position.agent")).group prec✝

inductive Sidner1983.ThematicSlot : Type

@cite{sidner-1983} §5.2.3 (p. 287) — thematic preference for expected discourse focus. The DEF list is ordered:

• theme unless the theme is a verb complement in which case the theme from the complement is used.
• all other thematic positions with the agent last
• the verb phrase

agent is third in this order — it is deprioritized for discourse focus and instead picked separately as the actor focus (this file's expectedActorFocus).

• theme : ThematicSlot
• otherNonAgent : ThematicSlot
• agent : ThematicSlot
• verbPhrase : ThematicSlot

@[implicit_reducible]

instance Sidner1983.instDecidableEqThematicSlot : DecidableEq ThematicSlot

Equations

• Sidner1983.instDecidableEqThematicSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Sidner1983.instReprThematicSlot : Repr ThematicSlot

Equations

• Sidner1983.instReprThematicSlot = { reprPrec := Sidner1983.instReprThematicSlot.repr }

def Sidner1983.instReprThematicSlot.repr : ThematicSlot → ℕ → Std.Format

Equations

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

def Sidner1983.ThematicSlot.defRank : ThematicSlot → ℕ

The DEF preference order from @cite{sidner-1983} §5.2.3 (p. 287), encoded as a ranking. Lower number = higher preference for discourse focus.

Equations

• Sidner1983.ThematicSlot.theme.defRank = 0
• Sidner1983.ThematicSlot.otherNonAgent.defRank = 1
• Sidner1983.ThematicSlot.agent.defRank = 2
• Sidner1983.ThematicSlot.verbPhrase.defRank = 3

inductive Sidner1983.SentenceForm : Type

Sentence-form distinction used by the expected-focus algorithm (@cite{sidner-1983} §5.2.3 step 1 p. 287): is-a and there-insertion sentences pick the subject as expected focus; other sentences use the DEF preference order.

• isaOrThereInsertion : SentenceForm
• normal : SentenceForm

@[implicit_reducible]

instance Sidner1983.instDecidableEqSentenceForm : DecidableEq SentenceForm

Equations

• Sidner1983.instDecidableEqSentenceForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Sidner1983.instReprSentenceForm : Repr SentenceForm

Equations

• Sidner1983.instReprSentenceForm = { reprPrec := Sidner1983.instReprSentenceForm.repr }

def Sidner1983.instReprSentenceForm.repr : SentenceForm → ℕ → Std.Format

Equations

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

structure Sidner1983.Phrase (E : Type) : Type

A noun-phrase slot in a sentence. Carries the entity, its thematic position, its syntactic position (agent or non-agent), and whether the surface form is pronominal.

• entity : E
• thematic : ThematicSlot
• position : Position
• isPronoun : Bool

def Sidner1983.instReprPhrase.repr {E✝ : Type} [Repr E✝] : Phrase E✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Sidner1983.instReprPhrase {E✝ : Type} [Repr E✝] : Repr (Phrase E✝)

Equations

• Sidner1983.instReprPhrase = { reprPrec := Sidner1983.instReprPhrase.repr }

structure Sidner1983.Sentence (E : Type) : Type

A sentence as a flat list of noun-phrase slots, plus a form flag. The simplification mirrors the GJW substrate's Discourse.Centering.Utterance: we elide the syntactic tree and keep the slots that the focusing algorithm actually consults.

• form : SentenceForm
• phrases : List (Phrase E)

@[implicit_reducible]

instance Sidner1983.instReprSentence {E✝ : Type} [Repr E✝] : Repr (Sentence E✝)

Equations

• Sidner1983.instReprSentence = { reprPrec := Sidner1983.instReprSentence.repr }

def Sidner1983.instReprSentence.repr {E✝ : Type} [Repr E✝] : Sentence E✝ → ℕ → Std.Format

Equations

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

structure Sidner1983.FocusState (E : Type) : Type

@cite{sidner-1983} §5.2 (p. 282): "An actor focus is a discourse item which is predicated as the agent in some event. It is distinct from the main focus, which will be called the discourse focus." Reasons given: "(1) the focus of the discourse is often distinguished from the actor … and (2) actors can be spoken of anaphorically at the same time that the discourse focus is pronominalized."

The two slots are independently updated and queried — this is the architectural point that distinguishes Sidner from @cite{grosz-joshi-weinstein-1995}'s single-Cb account.

• discourseFocus : Option E
• actorFocus : Option E

@[implicit_reducible]

instance Sidner1983.instReprFocusState {E✝ : Type} [Repr E✝] : Repr (FocusState E✝)

Equations

• Sidner1983.instReprFocusState = { reprPrec := Sidner1983.instReprFocusState.repr }

def Sidner1983.instReprFocusState.repr {E✝ : Type} [Repr E✝] : FocusState E✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Sidner1983.instDecidableEqFocusState {E✝ : Type} [DecidableEq E✝] : DecidableEq (FocusState E✝)

Equations

• Sidner1983.instDecidableEqFocusState = Sidner1983.instDecidableEqFocusState.decEq

def Sidner1983.instDecidableEqFocusState.decEq {E✝ : Type} [DecidableEq E✝] (x✝ x✝¹ : FocusState E✝) : Decidable (x✝ = x✝¹)

Equations

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

def Sidner1983.FocusState.empty {E : Type} : FocusState E

The empty focus state, used as the discourse-initial state.

Equations

• Sidner1983.FocusState.empty = { discourseFocus := none, actorFocus := none }

def Sidner1983.expectedDiscourseFocus {E : Type} (s : Sentence E) : Option E

The expected discourse focus computed from a single sentence by the algorithm at @cite{sidner-1983} §5.2.3 (p. 287):

• For an is-a or there-insertion sentence: the subject (modeled as the agent-position phrase).
• Otherwise: the phrase with minimal DEF rank (theme > other-non-agent > agent > verbPhrase). Implemented via List.argmin from mathlib.

Equations

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

theorem Sidner1983.expectedDiscourseFocus_normal_le {E : Type} {s : Sentence E} {e : E} (hform : s.form = SentenceForm.normal) (h : expectedDiscourseFocus s = some e) : ∃ (p : Phrase E), p ∈ s.phrases ∧ p.entity = e ∧ ∀ (p' : Phrase E), p' ∈ s.phrases → p.thematic.defRank ≤ p'.thematic.defRank

Characterization of expectedDiscourseFocus on a normal sentence: when it returns some e, there exists a phrase p in the sentence realizing e, and p's thematic rank is at most every other phrase's. (The "at most" — vs. "less than" — is argmin's tie-breaking convention: ties are resolved by surface order.)

def Sidner1983.expectedActorFocus {E : Type} (s : Sentence E) : Option E

The expected actor focus, by the analogous algorithm to the discourse-focus one but selecting the agent (@cite{sidner-1983} §5.2.3 p. 287, second algorithm sketch).

Equations

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

def Sidner1983.updateState {E : Type} (state : FocusState E) (s : Sentence E) : FocusState E

Update the focus state after a sentence. The discourse focus moves to the new sentence's expected discourse focus when one exists (otherwise retained); the actor focus moves to the new sentence's actor focus when one exists.

This is a simplified version of the full focusing algorithm (@cite{sidner-1983} §5.2.6 pp. 292-294). It captures the discourse-initial step and the basic "movement on each new sentence" pattern, sufficient for the (34) example.

Equations

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

def Sidner1983.resolvePronounAt {E : Type} (state : FocusState E) (pos : Position) : Option E

@cite{sidner-1983} §5.2.6 step 3 (p. 293), the rule that drives the @cite{grosz-joshi-weinstein-1995} §9 example (34) disagreement:

If there is an anaphor co-specifying the CF and another co-specifying some member of the ALFL, retain the CF as focus if the anaphor is not in agent position. If it is, take the member of the ALFL as focus.

Distilled to the essential rule: an agent-position pronoun co-specifies the actor focus; a non-agent pronoun co-specifies the discourse focus. The function takes a Position directly (the pronoun's syntactic slot) rather than a full Phrase, since the pronoun's putative entity is exactly the answer being computed.

Equations

• Sidner1983.resolvePronounAt state Sidner1983.Position.agent = state.actorFocus
• Sidner1983.resolvePronounAt state Sidner1983.Position.nonAgent = state.discourseFocus

GJW (1995) §9 (p. 222) discusses this discourse to contrast their centering account with Sidner's two-focus account:

(34) a. I haven't seen Jeff for several days.
     b. Carl thinks he's studying for his exams,
     c. but I think he went to the Cape with Linda.

Sidner predicts that "he" in (34c) is Carl: Carl is the actor
focus after (34b), and "he" in (34c) is in subject (agent)
position, so by §5.2.6 step 3 the actor focus wins.

The downstream comparison theorem lives in `GroszJoshiWeinstein1995.lean`
§8 — that file imports this one to mechanize the disagreement. 

def Sidner1983.D34.a : Sentence String

(34a) "I haven't seen Jeff for several days." Speaker = subject (agent of "see"); Jeff = theme (object of "see").

Equations

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

def Sidner1983.D34.b : Sentence String

(34b) "Carl thinks he's studying for his exams." Carl is the matrix subject (agent of "think"); the sentence is normal (not is-a / there-insertion). For the discourse-focus computation we treat the embedded subject "he" as the theme of the matrix verb "think" (the propositional theme), so Jeff (the entity "he" co-specifies, carried over from (34a)) becomes the new discourse focus.

Equations

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

def Sidner1983.D34.stateAfterB : FocusState String

The state of Sidner's focusing model after (34a) and (34b), starting from the empty state.

Equations

• Sidner1983.D34.stateAfterB = Sidner1983.updateState (Sidner1983.updateState Sidner1983.FocusState.empty Sidner1983.D34.a) Sidner1983.D34.b

theorem Sidner1983.D34.state_after_b : stateAfterB = { discourseFocus := some "Jeff", actorFocus := some "Carl" }

After (34b), the discourse focus is Jeff (the theme of "Carl thinks ___"; Jeff was already in focus from 34a and is reaffirmed by the embedded "he"). The actor focus is Carl (matrix agent). This matches GJW's gloss in §9 p. 222.

def Sidner1983.D34.sidnerPredictedHe : Option String

Sidner's prediction for "he" in (34c). The pronoun is in agent (subject) position, so by §5.2.6 step 3 it co-specifies the actor focus. Returns Option String: none would mean the focus state has no actor focus to resolve to.

Equations

• Sidner1983.D34.sidnerPredictedHe = Sidner1983.resolvePronounAt Sidner1983.D34.stateAfterB Sidner1983.Position.agent

theorem Sidner1983.D34.sidner_predicts_carl : sidnerPredictedHe = some "Carl"