Sidner (1979): Towards a Computational Theory of Definite Anaphora Comprehension

This file formalizes the focusing theory of [Sid79], whose chapters on the discourse focus and on pronouns are reprinted as [Sid83]. A discourse has a discourse focus and an actor focus, each with an ordered list of alternates and a stack of rejected foci. The expected focus algorithm predicts the discourse focus from the first sentence: the subject of an is-a or there-insertion sentence, otherwise the first member of the default expected focus list, the phrases ordered theme first, then the other thematic positions with the agent last, then the verb phrase (Sentence.expectedFocus, Sentence.expectedFocus_le). The focusing algorithm confirms or rejects the current focus by the anaphora of each later sentence, retaining it when an anaphor co-specifies it and otherwise moving it to a co-specified alternate or stack member and stacking the rejected focus (State.confirm, State.step); the actor focus is the agent of the current sentence (State.updateActor). A pronoun is interpreted against the state: the discourse focus is preferred for a pronoun outside agent position and the actor focus for one in agent position, the alternates following, except that a discourse focus established in an earlier sentence than the actor focus takes precedence even in agent position (State.candidates, State.cospecify, State.cospecify_agent_of_precedence). The examples run through the pipeline: the three sentences illustrating the expected focus algorithm, the recency rule in D2, the confirmation in D25 and the movement in D35, the reversed co-specifications of D14, and D9, in which every he co-specifies Jeff while the actor focus moves from the speaker to Carl to Oscar (D9.he_jeff).

Implementation notes

• A sentence is its form, which names the subject of an is-a or there-insertion sentence, and its phrases in surface order, each with the entity it specifies (for a pronoun its co-specification), its thematic relation at the granularity of the default expected focus list, whether it is a pronoun, and whether it is animate; agent position is the agent relation, and the verb phrase is a phrase with the relation verbPhrase, which the examples omit.
• The pipeline processes interpreted sentences: the focusing algorithm consults the co-specifications of the anaphora, and the pronoun rules order the candidates from which a predicate standing for the syntactic anaphoric filters and the inference mechanism selects the first. Anaphora in agent position are not consulted by the focusing algorithm when others occur.
• Only pronominal anaphora are modelled, so the steps of the focusing algorithm on do-anaphora, focus sets, implicit specification and nominalization are omitted, and the clause of step 3 on a definite noun phrase mentioning the focus is vacuous. A focus moved to a stack member stacks the rejected focus above the remaining members. Possessives, plural pronouns and the potential actor ambiguity condition are outside the model.

References

• [Sid79]
• [Sid83]

inductive Sidner1979.Thematic : Type

The thematic relation of a phrase to its verb at the granularity of the default expected focus list: the theme, any other position, the agent, and the verb phrase itself.

• theme : Thematic
• other : Thematic
• agent : Thematic
• verbPhrase : Thematic

@[instance_reducible]

instance Sidner1979.instDecidableEqThematic : DecidableEq Thematic

Equations

• Sidner1979.instDecidableEqThematic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Sidner1979.instFintypeThematic : Fintype Thematic

Equations

• Sidner1979.instFintypeThematic = { elems := { val := ↑Sidner1979.Thematic.enumList, nodup := Sidner1979.Thematic.enumList_nodup }, complete := Sidner1979.instFintypeThematic._proof_1 }

def Sidner1979.Thematic.rank : Thematic → ℕ

The preference of the default expected focus list: the theme first, then the other thematic positions with the agent last, then the verb phrase.

Equations

• Sidner1979.Thematic.theme.rank = 0
• Sidner1979.Thematic.other.rank = 1
• Sidner1979.Thematic.agent.rank = 2
• Sidner1979.Thematic.verbPhrase.rank = 3

@[instance_reducible]

instance Sidner1979.instLinearOrderThematic : LinearOrder Thematic

Equations

• Sidner1979.instLinearOrderThematic = LinearOrder.lift' Sidner1979.Thematic.rank Sidner1979.instLinearOrderThematic._proof_1

inductive Sidner1979.Form (E : Type u_1) : Type u_1

The form of a sentence as far as the expected focus algorithm consults it: an is-a or there-insertion sentence with its subject, or a plain sentence.

• isA {E : Type u_1} (subject : E) : Form E
• thereInsertion {E : Type u_1} (subject : E) : Form E
• plain {E : Type u_1} : Form E

def Sidner1979.instDecidableEqForm.decEq {E✝ : Type u_1} [DecidableEq E✝] (x✝ x✝¹ : Form E✝) : Decidable (x✝ = x✝¹)

Equations

• Sidner1979.instDecidableEqForm.decEq (Sidner1979.Form.isA a) (Sidner1979.Form.isA b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Sidner1979.instDecidableEqForm.decEq (Sidner1979.Form.isA subject) (Sidner1979.Form.thereInsertion subject_1) = isFalse ⋯
• Sidner1979.instDecidableEqForm.decEq (Sidner1979.Form.isA subject) Sidner1979.Form.plain = isFalse ⋯
• Sidner1979.instDecidableEqForm.decEq (Sidner1979.Form.thereInsertion subject) (Sidner1979.Form.isA subject_1) = isFalse ⋯
• Sidner1979.instDecidableEqForm.decEq (Sidner1979.Form.thereInsertion a) (Sidner1979.Form.thereInsertion b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Sidner1979.instDecidableEqForm.decEq (Sidner1979.Form.thereInsertion subject) Sidner1979.Form.plain = isFalse ⋯
• Sidner1979.instDecidableEqForm.decEq Sidner1979.Form.plain (Sidner1979.Form.isA subject) = isFalse ⋯
• Sidner1979.instDecidableEqForm.decEq Sidner1979.Form.plain (Sidner1979.Form.thereInsertion subject) = isFalse ⋯
• Sidner1979.instDecidableEqForm.decEq Sidner1979.Form.plain Sidner1979.Form.plain = isTrue ⋯

@[instance_reducible]

instance Sidner1979.instDecidableEqForm {E✝ : Type u_1} [DecidableEq E✝] : DecidableEq (Form E✝)

Equations

• Sidner1979.instDecidableEqForm = Sidner1979.instDecidableEqForm.decEq

structure Sidner1979.Phrase (E : Type u_1) : Type u_1

A phrase of an interpreted sentence: the entity it specifies, for a pronoun its co-specification, its thematic relation, whether it is a pronoun, and whether it is animate.

• entity : E
• thematic : Thematic
• pronoun : Bool
• animate : Bool

@[instance_reducible]

instance Sidner1979.instDecidableEqPhrase {E✝ : Type u_1} [DecidableEq E✝] : DecidableEq (Phrase E✝)

Equations

• Sidner1979.instDecidableEqPhrase = Sidner1979.instDecidableEqPhrase.decEq

def Sidner1979.instDecidableEqPhrase.decEq {E✝ : Type u_1} [DecidableEq E✝] (x✝ x✝¹ : Phrase E✝) : Decidable (x✝ = x✝¹)

Equations

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

structure Sidner1979.Sentence (E : Type u_1) : Type u_1

A sentence is its form and its phrases in surface order.

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

def Sidner1979.instDecidableEqSentence.decEq {E✝ : Type u_1} [DecidableEq E✝] (x✝ x✝¹ : Sentence E✝) : Decidable (x✝ = x✝¹)

Equations

• Sidner1979.instDecidableEqSentence.decEq { form := a, phrases := a_1 } { form := b, phrases := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Sidner1979.instDecidableEqSentence {E✝ : Type u_1} [DecidableEq E✝] : DecidableEq (Sentence E✝)

Equations

• Sidner1979.instDecidableEqSentence = Sidner1979.instDecidableEqSentence.decEq

def Sidner1979.Phrase.Precedes {E : Type u_1} (p q : Phrase E) : Prop

p.Precedes q when the default expected focus list orders p no later than q.

Equations

• p.Precedes q = (p.thematic ≤ q.thematic)

@[instance_reducible]

instance Sidner1979.Phrase.instDecidableRelPrecedes {E : Type u_1} : DecidableRel Precedes

Equations

• p.instDecidableRelPrecedes q = { decide := p.thematic.rank.ble q.thematic.rank, reflects_decide := ⋯ }

instance Sidner1979.Phrase.instTotalPrecedes {E : Type u_1} : Std.Total Precedes

instance Sidner1979.Phrase.instIsTransPrecedes {E : Type u_1} : IsTrans (Phrase E) Precedes

def Sidner1979.Sentence.defList {E : Type u_1} (s : Sentence E) : List (Phrase E)

The default expected focus list: the phrases in the order of Phrase.Precedes, surface order breaking ties.

Equations

• s.defList = List.insertionSort Sidner1979.Phrase.Precedes s.phrases

def Sidner1979.Sentence.expectedFocus {E : Type u_1} (s : Sentence E) : Option E

The expected focus algorithm: the subject of an is-a or there-insertion sentence and otherwise the first member of the default expected focus list.

Equations

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

def Sidner1979.Sentence.agent {E : Type u_1} (s : Sentence E) : Option E

The agent of the sentence, the phrase in agent position.

Equations

• s.agent = Option.map (fun (x : Sidner1979.Phrase E) => x.entity) (List.find? (fun (p : Sidner1979.Phrase E) => decide (p.thematic = Sidner1979.Thematic.agent)) s.phrases)

def Sidner1979.Sentence.potentialActors {E : Type u_1} (s : Sentence E) : List E

The potential actors: the animate phrases outside agent position.

Equations

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

def Sidner1979.Sentence.potentialFoci {E : Type u_1} (s : Sentence E) [DecidableEq E] (focus : Option E) : List E

The potential focus list given the focus: the phrases outside agent position not co-specifying the focus, in the order of the default expected focus list.

Equations

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

def Sidner1979.Sentence.anaphora {E : Type u_1} (s : Sentence E) : List E

The anaphora the focusing algorithm consults: the pronouns outside agent position, or all the pronouns when none is outside agent position.

Equations

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

theorem Sidner1979.Sentence.expectedFocus_le {E : Type u_1} (s : Sentence E) {e : E} (hs : s.form = Form.plain) (h : s.expectedFocus = some e) : ∃ p ∈ s.phrases, p.entity = e ∧ ∀ q ∈ s.phrases, p.thematic ≤ q.thematic

The expected focus of a plain sentence is realized by a phrase of least thematic rank.

structure Sidner1979.Focus (E : Type u_2) : Type u_2

A focus with the sentence that established it.

• entity : E
• since : ℕ

def Sidner1979.instDecidableEqFocus.decEq {E✝ : Type u_2} [DecidableEq E✝] (x✝ x✝¹ : Focus E✝) : Decidable (x✝ = x✝¹)

Equations

• Sidner1979.instDecidableEqFocus.decEq { entity := a, since := a_1 } { entity := b, since := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Sidner1979.instDecidableEqFocus {E✝ : Type u_2} [DecidableEq E✝] : DecidableEq (Focus E✝)

Equations

• Sidner1979.instDecidableEqFocus = Sidner1979.instDecidableEqFocus.decEq

structure Sidner1979.State (E : Type u_2) : Type u_2

The state of the focusing mechanism: the discourse focus and the actor focus, the alternate focus list (the rest of the default expected focus list after the first sentence and the potential focus list afterwards), the potential actors, the last constituent of the previous sentence for the recency rule, and the stacks of rejected discourse and actor foci.

• time : ℕ
• discourse : Option (Focus E)
• actor : Option (Focus E)
• alternates : List E
• potentialActors : List E
• last : Option E
• stack : List E
• actorStack : List E

@[instance_reducible]

instance Sidner1979.instDecidableEqState {E✝ : Type u_2} [DecidableEq E✝] : DecidableEq (State E✝)

Equations

• Sidner1979.instDecidableEqState = Sidner1979.instDecidableEqState.decEq

def Sidner1979.instDecidableEqState.decEq {E✝ : Type u_2} [DecidableEq E✝] (x✝ x✝¹ : State E✝) : Decidable (x✝ = x✝¹)

Equations

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

inductive Sidner1979.Position : Type

The position of a pronoun as the rules for its co-specification consult it: agent position, a subject outside agent position, or another position.

• agent : Position
• subject : Position
• other : Position

@[instance_reducible]

instance Sidner1979.instDecidableEqPosition : DecidableEq Position

Equations

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

def Sidner1979.State.initial {E : Type u_1} : State E

The state before the discourse.

Equations

• Sidner1979.State.initial = { time := 0, discourse := none, actor := none, alternates := [], potentialActors := [], last := none, stack := [], actorStack := [] }

def Sidner1979.State.confirm {E : Type u_1} [DecidableEq E] (st : State E) (t : ℕ) (a : List E) : State E

The confirmation of the current focus at sentence t by the anaphora a of the sentence: the focus is retained when an anaphor co-specifies it (step 4), moved to the first co-specified alternate (step 5) or else to a co-specified stack member (step 6) with the rejected focus stacked, and retained when no anaphor co-specifies any focus (step 10).

Equations

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

def Sidner1979.State.updateActor {E : Type u_1} [DecidableEq E] (st : State E) (t : ℕ) (agent : Option E) : State E

The actor focus at sentence t is the agent of the sentence when it has one, the previous actor focus being stacked when it changes.

Equations

• One or more equations did not get rendered due to their size.
• st.updateActor t none = st

def Sidner1979.State.step {E : Type u_1} [DecidableEq E] (st : State E) (s : Sentence E) : State E

Processing a sentence: the first sentence sets the discourse focus to its expected focus and the alternates to the rest of the default expected focus list; a later sentence confirms or rejects the discourse focus by its anaphora and sets the alternates to its potential foci. Both update the actor focus, the potential actors, and the last constituent.

Equations

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

def Sidner1979.State.run {E : Type u_1} [DecidableEq E] (st : State E) (d : List (Sentence E)) : State E

Processing a discourse sentence by sentence.

Equations

• st.run d = List.foldl Sidner1979.State.step st d

def Sidner1979.State.recency {E : Type u_1} [DecidableEq E] (st : State E) (pos : Position) : List E

The recency rule's candidate: for a pronoun in subject position, the last constituent of the previous sentence when it is an alternate.

Equations

• st.recency Sidner1979.Position.other = []
• st.recency pos✝ = []
• st.recency pos✝ = if e ∈ st.alternates then [e] else []

def Sidner1979.State.precedence {E : Type u_1} (st : State E) : List E

The discourse focus when it takes precedence over the actor focus for a pronoun in agent position, having been established in an earlier sentence.

Equations

• st.precedence = match st.discourse, st.actor with | some d, some a => if d.since < a.since then [d.entity] else [] | some d, none => [d.entity] | none, x => []

def Sidner1979.State.candidates {E : Type u_1} [DecidableEq E] (st : State E) (pos : Position) : List E

The candidates for the co-specification of a third person pronoun in the order the rules test them. After the recency rule, a pronoun in agent position tests the discourse focus when it takes precedence, the actor focus, the potential actors, the stacked actors, and then the discourse focus and its alternates; a pronoun outside agent position tests the discourse focus, its alternates, the actor focus, and the potential actors.

Equations

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

def Sidner1979.State.cospecify {E : Type u_1} [DecidableEq E] (st : State E) (pos : Position) (ok : E → Prop) [DecidablePred ok] : Option E

The co-specification of a pronoun: the first candidate that the syntactic anaphoric filters and the inference mechanism, ok, accept.

Equations

• st.cospecify pos ok = List.find? (fun (e : E) => decide (ok e)) (st.candidates pos)

theorem Sidner1979.State.confirm_of_mem {E : Type u_1} [DecidableEq E] {st : State E} {t : ℕ} {a : List E} {cf : Focus E} (h : st.discourse = some cf) (ha : cf.entity ∈ a) : st.confirm t a = st

Retention: an anaphor co-specifying the current focus leaves the state unchanged.

theorem Sidner1979.State.confirm_of_not_mem {E : Type u_1} [DecidableEq E] {st : State E} {t : ℕ} {a : List E} {cf : Focus E} (h : st.discourse = some cf) (ha : cf.entity ∉ a) (halt : ∃ e ∈ st.alternates, e ∈ a) : ∃ e ∈ st.alternates, e ∈ a ∧ (st.confirm t a).discourse = some { entity := e, since := t } ∧ (st.confirm t a).stack = cf.entity :: st.stack

Movement: when no anaphor co-specifies the current focus and one co-specifies an alternate, the focus moves to an alternate and the rejected focus is stacked.

theorem Sidner1979.State.cospecify_spec {E : Type u_1} [DecidableEq E] {st : State E} {pos : Position} {ok : E → Prop} [DecidablePred ok] {e : E} (h : st.cospecify pos ok = some e) : ok e ∧ e ∈ st.candidates pos

A co-specification is an accepted candidate.

theorem Sidner1979.State.cospecify_agent_of_precedence {E : Type u_1} [DecidableEq E] {st : State E} {ok : E → Prop} [DecidablePred ok] {d af : Focus E} (hd : st.discourse = some d) (haf : st.actor = some af) (hlt : d.since < af.since) (hok : ok d.entity) (hrec : ∀ e ∈ st.recency Position.agent, ¬ok e) : st.cospecify Position.agent ok = some d.entity

The animate discourse focus rule: a pronoun in agent position co-specifies a discourse focus that was established before the actor focus and passes the filters, the recency rule not applying.

The examples

The entities of the sentences illustrating the expected focus algorithm and of the discourses D2, D7, D8, D9 and D14 of chapter 4 and D25 and D35 of chapter 2.

inductive Sidner1979.Entity : Type

The entities of the examples.

• speaker : Entity
• sister : Entity
• zoo : Entity
• today : Entity
• oldMan : Entity
• woods : Entity
• linda : Entity
• dog : Entity
• allDay : Entity
• mary : Entity
• party : Entity
• hildasHouse : Entity
• cherryStreet : Entity
• necklace : Entity
• office : Entity
• yesterday : Entity
• grandmother : Entity
• max : Entity
• bloomingdales : Entity
• ned : Entity
• winston : Entity
• trip : Entity
• sneakers : Entity
• mother : Entity
• jeff : Entity
• days : Entity
• carl : Entity
• exams : Entity
• oscar : Entity
• cape : Entity
• myDog : Entity
• theVet : Entity
• hand : Entity
• medicine : Entity
• lastWeek : Entity
• strawberries : Entity
• refrigerator : Entity
• foodCoop : Entity
• alfredZohar : Entity
• baseball : Entity
• school : Entity
• dinner : Entity
• iceCreamCones : Entity

@[instance_reducible]

instance Sidner1979.instDecidableEqEntity : DecidableEq Entity

Equations

• Sidner1979.instDecidableEqEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Sidner1979.np (e : Entity) (θ : Thematic) (animate : Bool := false) : Phrase Entity

A phrase realized by a name or a description.

Equations

• Sidner1979.np e θ animate = { entity := e, thematic := θ, pronoun := false, animate := animate }

def Sidner1979.pron (e : Entity) (θ : Thematic) (animate : Bool := true) : Phrase Entity

A phrase realized by a pronoun.

Equations

• Sidner1979.pron e θ animate = { entity := e, thematic := θ, pronoun := true, animate := animate }

def Sidner1979.ex22 : Sentence Entity

(22) I took my sister to the zoo today.

Equations

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

def Sidner1979.ex23 : Sentence Entity

(23) There once was an old man who lived in the woods.

Equations

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

def Sidner1979.ex24 : Sentence Entity

(24) Linda talked with her dog all day long, with no theme.

Equations

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

theorem Sidner1979.expectedFocus_examples : ex22.expectedFocus = some Entity.sister ∧ ex23.expectedFocus = some Entity.oldMan ∧ ex24.expectedFocus = some Entity.dog

The expected foci of (22), (23) and (24): the theme, the subject of the there-insertion sentence, and the first non-agent phrase.

def Sidner1979.D2.a : Sentence Entity

(D2-1) Mary is giving a surprise party at Hilda's house.

Equations

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

theorem Sidner1979.D2.it_hildasHouse : ((State.initial.step a).cospecify Position.subject fun (x : Entity) => x ∈ [Entity.party, Entity.hildasHouse]) = some Entity.hildasHouse

The pronoun of (D2-2), It's at 340 Cherry St., in subject position, co-specifies Hilda's house by the recency rule, ahead of the expected focus, the party.

def Sidner1979.D7.a : Sentence Entity

(D7-1) I lost a necklace at the office yesterday.

Equations

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

def Sidner1979.D7.b : Sentence Entity

(D7-2) I inherited it from my grandmother.

Equations

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

theorem Sidner1979.D7.it_necklace : ((State.initial.step a).cospecify Position.other fun (x : Entity) => x ∈ [Entity.necklace, Entity.office]) = some Entity.necklace ∧ ((State.initial.run [a, b]).cospecify Position.subject fun (x : Entity) => x ∈ [Entity.necklace, Entity.office]) = some Entity.necklace

The pronouns of (D7-2) and (D7-3), and it meant a lot to me, co-specify the necklace, the discourse focus, which the second retains; the office is never reached.

def Sidner1979.D8.a : Sentence Entity

(D8-1) Yesterday Max went to Bloomingdales with Ned and Winston on a shopping trip.

Equations

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

theorem Sidner1979.D8.he_max : ((State.initial.step a).cospecify Position.agent fun (x : Entity) => x ∈ [Entity.max, Entity.ned, Entity.winston]) = some Entity.max

The pronoun of (D8-2), While he was there, he bought some sneakers for his mother, in agent position co-specifies the actor focus Max: the discourse focus Bloomingdales was established in the same sentence and takes no precedence.

def Sidner1979.D9.a : Sentence Entity

(D9-1) I haven't seen Jeff for several days.

Equations

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

def Sidner1979.D9.b : Sentence Entity

(D9-2) Carl thinks he's studying for his exams, the pronoun in the agent position of the complement co-specifying Jeff.

Equations

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

def Sidner1979.D9.c : Sentence Entity

(D9-3) Oscar says he is sick.

Equations

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

def Sidner1979.D9.afterB : State Entity

The state after (D9-2).

Equations

• Sidner1979.D9.afterB = Sidner1979.State.initial.run [Sidner1979.D9.a, Sidner1979.D9.b]

def Sidner1979.D9.afterC : State Entity

The state after (D9-3).

Equations

• Sidner1979.D9.afterC = Sidner1979.D9.afterB.step Sidner1979.D9.c

theorem Sidner1979.D9.foci : afterB.discourse = some { entity := Entity.jeff, since := 1 } ∧ afterB.actor = some { entity := Entity.carl, since := 2 } ∧ afterC.discourse = some { entity := Entity.jeff, since := 1 } ∧ afterC.actor = some { entity := Entity.oscar, since := 3 }

The discourse focus is Jeff throughout while the actor focus moves from the speaker to Carl to Oscar.

theorem Sidner1979.D9.he_jeff : ((State.initial.step a).cospecify Position.agent fun (x : Entity) => x ∈ [Entity.jeff, Entity.carl, Entity.oscar]) = some Entity.jeff ∧ (afterB.cospecify Position.agent fun (x : Entity) => x ∈ [Entity.jeff, Entity.carl, Entity.oscar]) = some Entity.jeff ∧ (afterC.cospecify Position.agent fun (x : Entity) => x ∈ [Entity.jeff, Entity.carl, Entity.oscar]) = some Entity.jeff

The pronouns in agent position of (D9-2) and of (D9-4), but I think he went to the Cape with Linda, co-specify Jeff: the discourse focus was established before the actor focus.

def Sidner1979.D14.a : Sentence Entity

(D14-1) I took my dog to the vet yesterday.

Equations

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

def Sidner1979.D14.b : Sentence Entity

(D14-2a) He bit him in the hand, he my dog and him the vet.

Equations

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

def Sidner1979.D14.b' : Sentence Entity

(D14-2b) He injected him with a new medicine, he the vet and him my dog.

Equations

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

def Sidner1979.D14.afterA : State Entity

The state after (D14-1).

Equations

• Sidner1979.D14.afterA = Sidner1979.State.initial.step Sidner1979.D14.a

theorem Sidner1979.D14.he : (afterA.cospecify Position.agent fun (x : Entity) => x ∈ [Entity.myDog, Entity.theVet]) = some Entity.myDog ∧ (afterA.cospecify Position.agent fun (x : Entity) => x ∈ [Entity.theVet]) = some Entity.theVet

In agent position the actor focus, the speaker, fails the filters for he, and the potential actors follow in surface order: my dog, or the vet once dogs are found not to inject.

theorem Sidner1979.D14.him : (afterA.cospecify Position.other fun (x : Entity) => x ∈ [Entity.myDog, Entity.theVet]) = some Entity.myDog ∧ (afterA.cospecify Position.other fun (x : Entity) => x ∈ [Entity.theVet]) = some Entity.theVet

Outside agent position the discourse focus, my dog, comes first for him, and the vet follows once dogs are found to have no hands.

theorem Sidner1979.D14.foci : (afterA.step b).discourse = some { entity := Entity.theVet, since := 2 } ∧ (afterA.step b).stack = [Entity.myDog] ∧ (afterA.step b).actor = some { entity := Entity.myDog, since := 2 } ∧ (afterA.step b).actorStack = [Entity.speaker] ∧ (afterA.step b').discourse = some { entity := Entity.myDog, since := 1 } ∧ (afterA.step b').actor = some { entity := Entity.theVet, since := 2 }

After (D14-2a) both foci have moved, my dog and the speaker stacked; after (D14-2b) the discourse focus is retained and the actor focus is the vet.

def Sidner1979.D25.a : Sentence Entity

(D25-1) Last week there were some nice strawberries in the refrigerator.

Equations

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

def Sidner1979.D25.b : Sentence Entity

(D25-2) They came from our food co-op and were unusually fresh.

Equations

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

theorem Sidner1979.D25.retained : (State.initial.run [a, b]).discourse = some { entity := Entity.strawberries, since := 1 } ∧ (State.initial.run [a, b]).stack = []

The expected focus, the subject of the there-insertion sentence, is confirmed.

def Sidner1979.D35.a : Sentence Entity

(D35-1) Alfred and Zohar liked to play baseball, the theme of the complement.

Equations

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

def Sidner1979.D35.b : Sentence Entity

(D35-2) They played it everyday after school before dinner.

Equations

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

def Sidner1979.D35.c : Sentence Entity

(D35-3) After their game, Alfred and Zohar had ice cream cones, the game the baseball.

Equations

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

def Sidner1979.D35.d : Sentence Entity

(D35-4) They tasted really good.

Equations

• Sidner1979.D35.d = { form := Sidner1979.Form.plain, phrases := [Sidner1979.pron Sidner1979.Entity.iceCreamCones Sidner1979.Thematic.theme false] }

theorem Sidner1979.D35.movement : (State.initial.run [a, b, c]).discourse = some { entity := Entity.baseball, since := 1 } ∧ (State.initial.run [a, b, c]).alternates = [Entity.iceCreamCones] ∧ (State.initial.run [a, b, c, d]).discourse = some { entity := Entity.iceCreamCones, since := 4 } ∧ (State.initial.run [a, b, c, d]).stack = [Entity.baseball]

Baseball is confirmed by it in (D35-2), the pronoun in agent position not consulted, and retained through (D35-3); the pronoun of (D35-4) moves the focus to the ice cream cones and stacks baseball.