Questions under discussion: stack and strategy

[Rob12]

The inquiry coordinate of the conversational scoreboard: the stack of accepted-but-unanswered questions (head is the immediate QUD; subquestions push, answers pop), the rose-tree strategy of inquiry decomposing a question into subquestions whose joint resolution answers the parent, and relevance of a move to the inquiry (moveRelevant, moveRelevantToStrategy).

Fidelity notes

moveRelevant is existential answerhood relevance: the partial-answer clause of [Rob12]'s Relevance (15), weaker than her strategy clause for interrogative moves. It is the proxy [IKW25] use for their relevance assumption (iii), consumed by the discourse only definedness condition in their (16). That the subquestions argument really lists subquestions of the QUD is the caller's obligation.

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

A QUD stack: ordered list of accepted, unanswered questions (Roberts 2012 Def 10g).

• questions : List (Question W)

def Discourse.QUDStack.empty {W : Type u_1} : QUDStack W

Empty QUD stack (discourse initial state).

Equations

• Discourse.QUDStack.empty = { questions := [] }

def Discourse.QUDStack.immediateQUD {W : Type u_1} (s : QUDStack W) : Option (Question W)

The immediate QUD: the most recently accepted, unanswered question.

Equations

• s.immediateQUD = s.questions.head?

def Discourse.QUDStack.push {W : Type u_1} (s : QUDStack W) (q : Question W) : QUDStack W

Accept a new question: push onto the stack.

Equations

• s.push q = { questions := q :: s.questions }

def Discourse.QUDStack.pop {W : Type u_1} (s : QUDStack W) : QUDStack W

Answer the immediate QUD: pop from the stack.

Equations

• s.pop = { questions := s.questions.tail }

def Discourse.QUDStack.depth {W : Type u_1} (s : QUDStack W) : ℕ

Current depth of the QUD stack.

Equations

• s.depth = s.questions.length

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

A strategy of inquiry as a rose tree: each node a question, children subquestions whose joint resolution answers the parent (Roberts Def 12).

• leaf {W : Type u_1} : Question W → Strategy W
• branch {W : Type u_1} : Question W → List (Strategy W) → Strategy W

def Discourse.Strategy.question {W : Type u_1} : Strategy W → Question W

The question at the root of this (sub)strategy.

Equations

• (Discourse.Strategy.leaf q).question = q
• (Discourse.Strategy.branch q a).question = q

def Discourse.Strategy.substrategies {W : Type u_1} : Strategy W → List (Strategy W)

Immediate substrategies (empty for leaves).

Equations

• (Discourse.Strategy.leaf q).substrategies = []
• (Discourse.Strategy.branch q a).substrategies = a

@[irreducible]

def Discourse.Strategy.allQuestions {W : Type u_1} : Strategy W → List (Question W)

All questions in the strategy (root + all descendants).

Equations

• (Discourse.Strategy.leaf q).allQuestions = [q]
• (Discourse.Strategy.branch q a).allQuestions = q :: List.flatMap Discourse.Strategy.allQuestions a

@[irreducible]

def Discourse.Strategy.leaves {W : Type u_1} : Strategy W → List (Question W)

Leaf questions only (terminal nodes of the strategy).

Equations

• (Discourse.Strategy.leaf q).leaves = [q]
• (Discourse.Strategy.branch q a).leaves = List.flatMap Discourse.Strategy.leaves a

def Discourse.Strategy.isComplete {W : Type u_1} : Strategy W → Prop

A strategy is complete at a single level: the meet of children's questions entails the parent. Recurse on substrategies for full-tree verification.

Equations

• (Discourse.Strategy.leaf q).isComplete = True
• (Discourse.Strategy.branch q a).isComplete = (List.foldl (fun (x1 x2 : Question W) => x1 ⊓ x2) ⊤ (List.map (fun (x : Discourse.Strategy W) => x.question) a)).Entails q

def Discourse.moveRelevant {W : Type u_1} (den qud : Question W) (subquestions : List (Question W)) : Prop

A move is relevant if one of its alternatives partially answers the QUD or one of the subquestions.

Equations

• Discourse.moveRelevant den qud subquestions = ∃ a ∈ den.alt, Question.PartiallyAnswers a qud ∨ ∃ q ∈ subquestions, Question.PartiallyAnswers a q

def Discourse.moveRelevantToStrategy {W : Type u_1} (den : Question W) (strat : Strategy W) : Prop

A discourse move is relevant to a strategy if some alternative of den partially answers some question in the strategy.

Equations

• Discourse.moveRelevantToStrategy den strat = ∃ a ∈ den.alt, ∃ q ∈ strat.allQuestions, Question.PartiallyAnswers a q

theorem Discourse.moveRelevant_of_partiallyAnswers {W : Type u_1} {den qud : Question W} {a : Set W} (ha : a ∈ den.alt) (h : Question.PartiallyAnswers a qud) : moveRelevant den qud []

A move is relevant if one of its alternatives partially answers the QUD directly, with no subquestions.

theorem Discourse.moveRelevantToStrategy_iff_moveRelevant {W : Type u_1} (den : Question W) (strat : Strategy W) : moveRelevantToStrategy den strat ↔ moveRelevant den strat.question (List.flatMap Strategy.allQuestions strat.substrategies)

Strategy relevance is moveRelevant against the root question and the descendant questions.

theorem Discourse.moveRelevant_polar_iff {W : Type u_1} {p : Set W} {qud : Question W} {subquestions : List (Question W)} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : moveRelevant (Question.polar p) qud subquestions ↔ (Question.PartiallyAnswers p qud ∨ ∃ Q ∈ subquestions, Question.PartiallyAnswers p Q) ∨ Question.PartiallyAnswers pᶜ qud ∨ ∃ Q ∈ subquestions, Question.PartiallyAnswers pᶜ Q

Polar reduction of moveRelevant to partial answerhood of p and pᶜ.