Questions under discussion: stack and strategy

The inquiry coordinate of the conversational scoreboard, after [Rob12]: the stack of accepted-but-unanswered questions (QUDStack, her definition (10g); the head is the immediate QUD), strategies of inquiry as rose trees of questions (Strategy, her (12); [Bur03]'s d-trees are the explicit tree-shaped ancestor), hereditary strategy completeness (IsComplete), and relevance of a move's denotation to a set of questions (Question.IsRelevantTo, built from the assertion clause of her Relevance (15)). [Gin12]'s KoS models the same coordinate as a partially ordered set with its own update rules; that structure lives with the gameboard in Discourse/Gameboard/. [BRST17] is the modern survey statement of the framework; [Rie19] gives explicit reconstruction rules and well-formedness constraints for QUD trees over corpus data.

Main definitions

• Discourse.QUDStack — the stack, as a List (Question W)
• Discourse.QUDStack.WellFormed — Roberts' ordering constraint (10g.iii), relative to a context set
• Discourse.Strategy — strategies of inquiry as RoseTree (Question W)
• Discourse.Strategy.IsComplete — at every branching node, the meet of the children's questions entails the parent's
• Question.IsRelevantTo — some alternative of the move partially answers some question in the set

Fidelity notes

Roberts' (10g) makes QUD a function from moves to ordered sets of accepted, unanswered questions; QUDStack models a single value of that function, and clause (iii) — each question's complete answers contextually entail partial answers to every question below it — is WellFormed, relative to a context set because entailment in her (9) is contextual throughout. She warns against strengthening (iii) to question entailment (her bridging-question discourse (13) violates it). Questions are retired when answered or determined practically unanswerable, and she licenses non-LIFO removal (answering a lower question discharges the higher questions in its strategy); List.tail is the unconditional LIFO special case, and the licensing conditions are the caller's obligation.

Her (12) defines Strat(q) derivatively — its substrategies are those for the questions accepted while q was the immediate QUD — with well-formedness left to "rational considerations", and the second component an unordered set. The ordered RoseTree follows [Bur03]. IsComplete is the success criterion her D₀ discussion illustrates (complete answers to the subquestions jointly yield a complete answer to the parent), not a clause of (12); the converse direction (parent entails children-meet) is exactly what (13) rules out.

IsRelevantTo is existential answerhood relevance: weaker than (15), whose guarantee is universal (every complete answer to the move contextually entails a partial answer to the QUD), and set-valued where (15) targets only last(QUD). The set extension is the proxy [IKW25] use for their relevance assumption, consumed by the discourse only definedness condition in their (16); that the set really holds subquestions of the QUD is the caller's obligation.

@[reducible, inline]

abbrev Discourse.QUDStack (W : Type u_1) : Type u_1

A QUD stack ([Rob12] definition (10g)): the accepted, unanswered questions, most recent first, so the head is the immediate QUD. Accepting a question is List.cons; retiring one from the top is List.tail.

Equations

• Discourse.QUDStack W = List (Question W)

def Discourse.QUDStack.WellFormed {W : Type u_1} (C : Set W) (s : QUDStack W) : Prop

Roberts' ordering constraint (10g.iii) on a QUD stack, relative to context set C: for higher accepted more recently than lower, every complete answer to higher contextually entails a partial answer to lower.

Equations

• Discourse.QUDStack.WellFormed C s = List.Pairwise (fun (higher lower : Question W) => ∀ a ∈ higher.alt, Question.PartiallyAnswers (C ∩ a) lower) s

@[simp]

theorem Discourse.QUDStack.wellFormed_nil {W : Type u_1} (C : Set W) : WellFormed C []

@[simp]

theorem Discourse.QUDStack.wellFormed_singleton {W : Type u_1} (C : Set W) (q : Question W) : WellFormed C [q]

theorem Discourse.QUDStack.wellFormed_cons {W : Type u_1} {C : Set W} {q : Question W} {s : QUDStack W} : WellFormed C (q :: s) ↔ (∀ lower ∈ s, ∀ a ∈ q.alt, Question.PartiallyAnswers (C ∩ a) lower) ∧ WellFormed C s

Accepting q preserves well-formedness iff q's complete answers contextually partially answer every question already on the stack.

theorem Discourse.QUDStack.WellFormed.tail {W : Type u_1} {C : Set W} {s : QUDStack W} (h : WellFormed C s) : WellFormed C (List.tail s)

Retiring the immediate QUD preserves well-formedness.

@[reducible, inline]

abbrev Discourse.Strategy (W : Type u_1) : Type u_1

A strategy of inquiry as a rose tree of questions ([Rob12] definition (12), [Bur03]'s d-trees): each node a question, its children the subquestions pursued to answer it.

Equations

• Discourse.Strategy W = RoseTree (Question W)

inductive Discourse.Strategy.IsComplete {W : Type u_1} : Strategy W → Prop

A strategy is complete when at every branching node the meet of the children's questions entails the parent's question: jointly resolving the subquestions resolves the parent. Terminal nodes are trivially complete.

• node {W : Type u_1} {q : Question W} {cs : List (Strategy W)} (complete : cs ≠ [] → (↑(List.map RoseTree.value cs)).inf.Entails q) (children : ∀ c ∈ cs, c.IsComplete) : IsComplete (RoseTree.node q cs)

theorem Discourse.Strategy.IsComplete.leaf {W : Type u_1} (q : Question W) : IsComplete (RoseTree.leaf q)

theorem Discourse.Strategy.IsComplete.node_pair {W : Type u_1} {q : Question W} {s t : Strategy W} (h : (RoseTree.value s ⊓ RoseTree.value t).Entails q) (hs : s.IsComplete) (ht : t.IsComplete) : IsComplete (RoseTree.node q [s, t])

Binary branching: a two-child node is complete when the meet of the children's questions entails the parent's and both children are complete.

@[simp]

theorem Discourse.Strategy.isComplete_node_iff {W : Type u_1} {q : Question W} {cs : List (Strategy W)} : IsComplete (RoseTree.node q cs) ↔ (cs ≠ [] → (↑(List.map RoseTree.value cs)).inf.Entails q) ∧ ∀ c ∈ cs, c.IsComplete