Documentation

Studies.Roberts2012

Roberts (2012): Information structure in discourse #

This file formalizes the paper's worked discourse, two individuals, two foods and seven questions forming a strategy of inquiry, on the substrate's alternative-set questions and questions-under-discussion stacks. A world is the set of eating events that occurred, a polar question is Question.ofSet of its one alternative and a wh-question the join of its polar subquestions (1), so that the complete-answer partition (4), question entailment (8) and the answer-composition facts (11) are derived, completeAnswers_wh_inter. The stack of questions under discussion at a move (10g) is computed from the moves before it, the questions accepted so far whose complete answer the context set fails to entail, qud; on the eleven moves of the discourse it reproduces the paper's table of stacks, qud_D₀, each well formed in its context set. The strategy of inquiry (12) is read off the same function, the subquestions of a question being those accepted while it was the immediate question under discussion, subquestions, and the tree so obtained is complete, strat_complete. Answerhood (3) and relevance (15) are checked on the discourse's assertions.

Implementation notes #

Entailment between questions is inclusion of complete-answer sets; the substrate's lattice order, entailment by resolution, runs the other way on the discourse's Hamblin questions (wh_le_q1), as the paper notes it would off complete answers. The substrate's inquisitive Question.polar, with alternatives a proposition and its complement, is a rival yes/no convention, not the paper's singleton alternative set. The context set of a move is the intersection of the assertions before it from a trivial initial common ground, so contextual entailment is entailment relative to that set; a question determined to be unanswerable, which the paper also retires, does not arise in the discourse.

References #

The world space #

inductive Roberts2012.Person :

The two individuals.

hilary : Person
robin : Person

Instances For

@[instance_reducible]

instance Roberts2012.instDecidableEqPerson :

DecidableEq Person

Equations

Roberts2012.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Roberts2012.instFintypePerson :

Fintype Person

Equations

Roberts2012.instFintypePerson = { elems := { val := ↑Roberts2012.Person.enumList, nodup := Roberts2012.Person.enumList_nodup }, complete := Roberts2012.instFintypePerson._proof_1 }

@[instance_reducible]

instance Roberts2012.instInhabitedPerson :

Inhabited Person

Equations

Roberts2012.instInhabitedPerson = { default := Roberts2012.instInhabitedPerson.default }

inductive Roberts2012.Food :

The two foods.

bagels : Food
tofu : Food

Instances For

@[instance_reducible]

instance Roberts2012.instDecidableEqFood :

DecidableEq Food

Equations

Roberts2012.instDecidableEqFood x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Roberts2012.instFintypeFood :

Fintype Food

Equations

Roberts2012.instFintypeFood = { elems := { val := ↑Roberts2012.Food.enumList, nodup := Roberts2012.Food.enumList_nodup }, complete := Roberts2012.instFintypeFood._proof_1 }

@[instance_reducible]

instance Roberts2012.instInhabitedFood :

Inhabited Food

Equations

Roberts2012.instInhabitedFood = { default := Roberts2012.instInhabitedFood.default }

theorem Roberts2012.Person.forall_person {p : Person → Prop} :

(∀ (u : Person), p u) ↔ p hilary ∧ p robin

theorem Roberts2012.Food.forall_food {p : Food → Prop} :

(∀ (f : Food), p f) ↔ p bagels ∧ p tofu

theorem Roberts2012.iInter_food_eq {α : Type u_1} {X : Food → Set α} :

⋂ (f : Food), X f = X Food.bagels ∩ X Food.tofu

@[reducible, inline]

abbrev Roberts2012.World :

A world: the set of eating events that occurred in it.

Equations

Roberts2012.World = Finset (Roberts2012.Person × Roberts2012.Food)

Instances For

@[reducible, inline]

abbrev Roberts2012.ate (u : Person) (f : Food) :

u ate f: the worlds containing the event, the principal up-set of its minimal world.

Equations

Roberts2012.ate u f = Set.Ici {(u, f)}

Instances For

theorem Roberts2012.ate_subset_ate_iff {u u' : Person} {f f' : Food} :

ate u f ⊆ ate u' f' ↔ u = u' ∧ f = f'

Distinct eating events are incomparable.

The seven questions ((1), (2), (7)) #

@[reducible, inline]

abbrev Roberts2012.hilaryBagels :

Hilary ate the bagels.

Equations

Roberts2012.hilaryBagels = Roberts2012.ate Roberts2012.Person.hilary Roberts2012.Food.bagels

Instances For

@[reducible, inline]

abbrev Roberts2012.hilaryTofu :

Hilary ate the tofu.

Equations

Roberts2012.hilaryTofu = Roberts2012.ate Roberts2012.Person.hilary Roberts2012.Food.tofu

Instances For

@[reducible, inline]

abbrev Roberts2012.robinBagels :

Robin ate the bagels.

Equations

Roberts2012.robinBagels = Roberts2012.ate Roberts2012.Person.robin Roberts2012.Food.bagels

Instances For

@[reducible, inline]

abbrev Roberts2012.robinTofu :

Robin ate the tofu.

Equations

Roberts2012.robinTofu = Roberts2012.ate Roberts2012.Person.robin Roberts2012.Food.tofu

Instances For

@[reducible, inline]

abbrev Roberts2012.polar (u : Person) (f : Food) :

"Did u eat f?": a yes/no question has its one proposition as alternative.

Equations

Roberts2012.polar u f = Question.ofSet (Roberts2012.ate u f)

Instances For

@[reducible, inline]

abbrev Roberts2012.wh (u : Person) :

"What did u eat?": the join of its alternatives.

Equations

Roberts2012.wh u = ⨆ (f : Roberts2012.Food), Roberts2012.polar u f

Instances For

@[reducible, inline]

abbrev Roberts2012.q_1 :

"Who ate what?", the discourse's move 1, joining alternatives over person–food pairs.

Equations

Roberts2012.q_1 = ⨆ (uf : Roberts2012.Person × Roberts2012.Food), Roberts2012.polar uf.1 uf.2

Instances For

inductive Roberts2012.Qn :

The questions of the discourse.

one : Qn
a : Qn
ai : Qn
aii : Qn
b : Qn
bi : Qn
bii : Qn

Instances For

@[instance_reducible]

instance Roberts2012.instDecidableEqQn :

DecidableEq Qn

Equations

Roberts2012.instDecidableEqQn x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Roberts2012.instFintypeQn :

Fintype Qn

Equations

Roberts2012.instFintypeQn = { elems := { val := ↑Roberts2012.Qn.enumList, nodup := Roberts2012.Qn.enumList_nodup }, complete := Roberts2012.instFintypeQn._proof_1 }

Alternative enumerations #

theorem Roberts2012.ate_antichain (uf uf' : Person × Food) (h : ate uf.1 uf.2 ⊆ ate uf'.1 uf'.2) :

ate uf.1 uf.2 = ate uf'.1 uf'.2

theorem Roberts2012.alt_wh (u : Person) :

(wh u).alt = Set.range (ate u)

theorem Roberts2012.alt_q_1 :

q_1.alt = Set.range fun (uf : Person × Food) => ate uf.1 uf.2

theorem Roberts2012.mem_alt_wh (u : Person) (f : Food) :

ate u f ∈ (wh u).alt

theorem Roberts2012.mem_alt_q1 (u : Person) (f : Food) :

ate u f ∈ q_1.alt

Alternative inclusions #

Subquestionhood in the discourse is alternative-set inclusion: each polar alternative is an alternative of its wh-question, and each wh alternative is an alternative of the big question.

theorem Roberts2012.alt_polar_subset_wh (u : Person) (f : Food) :

(polar u f).alt ⊆ (wh u).alt

theorem Roberts2012.alt_wh_subset_q1 (u : Person) :

(wh u).alt ⊆ q_1.alt

theorem Roberts2012.alt_polar_subset_q1 (u : Person) (f : Food) :

(polar u f).alt ⊆ q_1.alt

The complete-answer partition (4) #

theorem Roberts2012.subset_corners_iff {σ A B : Set World} :

(σ ⊆ A ∨ σ ⊆ Aᶜ) ∧ (σ ⊆ B ∨ σ ⊆ Bᶜ) ↔ σ ⊆ A ∩ B ∨ σ ⊆ A ∩ Bᶜ ∨ σ ⊆ Aᶜ ∩ B ∨ σ ⊆ Aᶜ ∩ Bᶜ

Deciding two propositions is lying in one of the four Boolean corners.

theorem Roberts2012.completelyAnsweredBy_wh_iff {σ : Set World} {u : Person} :

(wh u).CompletelyAnsweredBy σ ↔ σ ⊆ ate u Food.bagels ∩ ate u Food.tofu ∨ σ ⊆ ate u Food.bagels ∩ (ate u Food.tofu)ᶜ ∨ σ ⊆ (ate u Food.bagels)ᶜ ∩ ate u Food.tofu ∨ σ ⊆ (ate u Food.bagels)ᶜ ∩ (ate u Food.tofu)ᶜ

A state completely answers "What did u eat?" iff it lies within one cell of the partition the alternatives induce.

@[instance_reducible]

instance Roberts2012.instDecidableLeSetWorldCoeFinsetOfDecidablePredMem (C : Finset World) (S : Set World) [DecidablePred fun (x : World) => x ∈ S] :

Decidable (↑C ⊆ S)

Equations

Roberts2012.instDecidableLeSetWorldCoeFinsetOfDecidablePredMem C S = decidable_of_iff (∀ w ∈ C, w ∈ S) ⋯

@[instance_reducible]

instance Roberts2012.instDecidableCompletelyAnsweredByWorldDenCoeFinset (C : Finset World) (q : Qn) :

Decidable (q.den.CompletelyAnsweredBy ↑C)

Whether a finite state completely answers a question of the discourse is decidable.

Equations

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

Question entailment ((3), (8)) #

A question entails another when answering it yields a complete answer to the other: the inclusion of complete-answer sets, which the paper tabulates for the seven questions. The lattice order of the substrate reverses it (wh_le_q1, not_q1_le_wh).

theorem Roberts2012.q1_entails_wh (u : Person) :

q_1.completeAnswers ⊆ (wh u).completeAnswers

"Who ate what?" entails "What did u eat?".

theorem Roberts2012.wh_entails_polar (u : Person) (f : Food) :

(wh u).completeAnswers ⊆ (polar u f).completeAnswers

"What did u eat?" entails "Did u eat f?".

theorem Roberts2012.q1_entails_polar (u : Person) (f : Food) :

q_1.completeAnswers ⊆ (polar u f).completeAnswers

"Who ate what?" entails every polar subquestion.

theorem Roberts2012.wh_not_entails_q1 :

¬(wh Person.hilary).completeAnswers ⊆ q_1.completeAnswers

Subquestions do not entail their superquestions: "Hilary ate both" completely answers "What did Hilary eat?" but decides nothing about Robin.

theorem Roberts2012.polar_not_entails_wh :

¬(polar Person.hilary Food.bagels).completeAnswers ⊆ (wh Person.hilary).completeAnswers

"Did Hilary eat the bagels?" does not entail "What did Hilary eat?": the positive answer leaves the tofu alternative open.

theorem Roberts2012.wh_le_q1 (u : Person) :

wh u ≤ q_1

Read as the lattice order, entailment runs the other way, as the paper warns it would without complete answers: every state establishing something u ate establishes something someone ate.

theorem Roberts2012.not_q1_le_wh :

¬q_1 ≤ wh Person.hilary

The converse fails: that Robin ate the bagels settles "Who ate what?" but nothing Hilary ate.

Answer composition (11) #

The complete answers to a join are the meet of the complete answers, completeAnswers_iSup_ofSet, so jointly answering the polar subquestions is answering the wh-question and jointly answering the two wh-questions is answering the big question.

theorem Roberts2012.completeAnswers_wh (u : Person) :

(wh u).completeAnswers = ⋂ (f : Food), (polar u f).completeAnswers

The complete answers to "What did u eat?" are the joint complete answers to its polar subquestions.

theorem Roberts2012.completeAnswers_polar_inter (u : Person) :

(polar u Food.bagels).completeAnswers ∩ (polar u Food.tofu).completeAnswers = (wh u).completeAnswers

Jointly answering the polar subquestions is exactly answering "What did u eat?".

theorem Roberts2012.completeAnswers_wh_inter :

(wh Person.hilary).completeAnswers ∩ (wh Person.robin).completeAnswers = q_1.completeAnswers

Jointly answering "What did Hilary eat?" and "What did Robin eat?" is exactly answering "Who ate what?".

The discourse and its stacks (10g) #

inductive Roberts2012.Move :

A move: a setup move, which is a question, or a payoff move, which asserts that u ate f.

ask (q : Qn) : Move
assert (u : Person) (f : Food) : Move

Instances For

def Roberts2012.D₀ :

List Move

The eleven moves of the discourse in order: each question is accepted and each polar question answered yes.

Equations

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

Instances For

def Roberts2012.contextSet :

List Move → Finset World

The context set after a sequence of moves: the worlds in which every asserted event occurred, from a trivial initial common ground.

Equations

Roberts2012.contextSet [] = Finset.univ
Roberts2012.contextSet (Roberts2012.Move.ask q :: ms) = Roberts2012.contextSet ms
Roberts2012.contextSet (Roberts2012.Move.assert u f :: ms) = {w ∈ Roberts2012.contextSet ms | (u, f) ∈ w}

Instances For

def Roberts2012.asked :

List Move → List Qn

The questions accepted in a sequence of moves, most recent first.

Equations

Roberts2012.asked [] = []
Roberts2012.asked (Roberts2012.Move.ask q :: ms) = Roberts2012.asked ms ++ [q]
Roberts2012.asked (Roberts2012.Move.assert u f :: ms) = Roberts2012.asked ms

Instances For

def Roberts2012.qud (ms : List Move) :

List Qn

The questions under discussion after a sequence of moves: the accepted questions whose complete answer the context set fails to entail, most recent first (10g.i).

Equations

Roberts2012.qud ms = List.filter (fun (q : Roberts2012.Qn) => decide ¬q.den.CompletelyAnsweredBy ↑(Roberts2012.contextSet ms)) (Roberts2012.asked ms)

Instances For

def Roberts2012.table :

ℕ → List Qn

The paper's table of stacks: the questions under discussion at each of the eleven moves, the immediate one first, and the empty stack after the last answer.

Equations

Instances For

theorem Roberts2012.qud_D₀ (k : ℕ) :

k < 12 → qud (List.take k D₀) = table k

The stacks computed from the moves are the paper's: a question is retired exactly when the answers so far entail its complete answer, so "What did Hilary eat?" leaves the stack once both its polar subquestions are answered.

theorem Roberts2012.wellFormed_wh (C : Set World) (u : Person) :

List.Pairwise (Question.IsSubquestionOf C) [wh u, q_1]

theorem Roberts2012.wellFormed_polar (C : Set World) (u : Person) (f : Food) :

List.Pairwise (Question.IsSubquestionOf C) [polar u f, wh u, q_1]

theorem Roberts2012.qud_wellFormed (k : ℕ) (hk : k < 12) :

List.Pairwise (Question.IsSubquestionOf ↑(contextSet (List.take k D₀))) (List.map Qn.den (qud (List.take k D₀)))

Every stack of the discourse is well formed in its context set (10g.iii): each question is a contextual subquestion of every question below it.

The strategy of inquiry (12) #

def Roberts2012.subquestions (ms : List Move) (q : Qn) :

List Qn

The subquestions of a question in a sequence of moves: the questions accepted while it was the immediate question under discussion.

Equations

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

Instances For

theorem Roberts2012.subquestions_D₀ :

subquestions D₀ Qn.one = [Qn.a, Qn.b] ∧ subquestions D₀ Qn.a = [Qn.ai, Qn.aii] ∧ subquestions D₀ Qn.b = [Qn.bi, Qn.bii] ∧ ∀ q ∈ [Qn.ai, Qn.aii, Qn.bi, Qn.bii], subquestions D₀ q = []

The discourse answers the big question by answering the two wh-questions and each of those by answering its two polar subquestions.

def Roberts2012.strat :

Discourse.Strategy World

The strategy of inquiry the discourse realizes, read off its stacks.

Equations

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

Instances For

theorem Roberts2012.wh_complete (u : Person) :

Discourse.Strategy.IsComplete (RoseTree.node (wh u) [RoseTree.leaf (polar u Food.bagels), RoseTree.leaf (polar u Food.tofu)])

A wh-question's substrategy is complete: jointly resolving its polar subquestions resolves it, as already resolving one does, since it is one of the wh-question's disjuncts.

theorem Roberts2012.strat_complete :

strat.IsComplete

The strategy is complete: joint resolutions of the wh-questions resolve the big question, whose disjuncts include those of each.

theorem Roberts2012.values_whTree (u : Person) :

(RoseTree.node (wh u) [RoseTree.leaf (polar u Food.bagels), RoseTree.leaf (polar u Food.tofu)]).values = [wh u, polar u Food.bagels, polar u Food.tofu]

theorem Roberts2012.wh_wellFormed (C : Set World) (u : Person) :

Discourse.Strategy.WellFormed C (RoseTree.node (wh u) [RoseTree.leaf (polar u Food.bagels), RoseTree.leaf (polar u Food.tofu)])

A wh-question's substrategy is well formed in every context: each polar question is a subquestion of the wh-question by alternative inclusion.

theorem Roberts2012.strat_wellFormed (C : Set World) :

Discourse.Strategy.WellFormed C strat

The strategy is well formed in every context: every question below the big question is its subquestion by alternative inclusion, and each wh-substrategy is well formed.

Answerhood (3) #

A partial answer evaluates at least one alternative, positively or negatively; the negative direction, ruling an alternative out, is the paper's point against confirm-only answerhood.

theorem Roberts2012.neg_hilaryBagels_partiallyAnsweredBy_polar :

(polar Person.hilary Food.bagels).PartiallyAnsweredBy hilaryBagels ᶜ

"Hilary didn't eat bagels" negatively answers "Did Hilary eat the bagels?": it falsifies its sole alternative.

theorem Roberts2012.neg_hilaryBagels_partiallyAnsweredBy_wh :

(wh Person.hilary).PartiallyAnsweredBy hilaryBagels ᶜ

"Hilary didn't eat bagels" partially answers "What did Hilary eat?": it rules out the bagels alternative.

theorem Roberts2012.hilaryBagels_partiallyAnsweredBy_polar :

(polar Person.hilary Food.bagels).PartiallyAnsweredBy hilaryBagels

"Hilary ate bagels" positively answers "Did Hilary eat the bagels?".

theorem Roberts2012.hilaryBagels_partiallyAnsweredBy_q1 :

q_1.PartiallyAnsweredBy hilaryBagels

"Hilary ate bagels" partially answers "Who ate what?": it confirms one of its four alternatives.

Relevance (15) #

Assertion-clause relevance throughout; the paper's clause for interrogative moves is strategy membership, which wh_relevant_to_q1 proxies by partial answerhood.

def Roberts2012.hilaryBagels_assertion :

The assertion "Hilary ate bagels": a declarative's alternative set is the singleton of its content.

Equations

Roberts2012.hilaryBagels_assertion = Question.ofSet Roberts2012.hilaryBagels

Instances For

theorem Roberts2012.hilaryBagels_relevant_to_q1 :

hilaryBagels_assertion.IsRelevantTo {q_1}

"Hilary ate bagels" is relevant to move 1, "Who ate what?".

theorem Roberts2012.wh_relevant_to_q1 :

(wh Person.hilary).IsRelevantTo {q_1}

"What did Hilary eat?" is relevant to "Who ate what?" under the assertion-clause proxy: its bagels alternative confirms an alternative of the big question.

theorem Roberts2012.hilaryBagels_relevant_to_strat :

hilaryBagels_assertion.IsRelevantTo {q : Question World | q ∈ RoseTree.values strat}

"Hilary ate bagels" is relevant to the whole strategy: it partially answers its root.