Strategy of Inquiry: Rose-Tree Decomposition of a QUD

@cite{roberts-2012}

A Strategy W is @cite{roberts-2012} Def. 12: a plan to answer a question by pursuing subquestions. Modeled as a rose tree where each node is a question and children are subquestions whose collective answers resolve the parent. The companion stack representation (QUDStack) captures the current unanswered slice; a strategy captures the full plan.

The strategy is parameterized by Core.Question W — the Set-based inquisitive-content lattice. The completeness predicate uses lattice meet ⊓ (children's joint answer) and the Prop-valued Core.Question.questionEntails from Core/Question/Relevance.lean.

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

A strategy of inquiry: a plan to answer a question by pursuing subquestions.

@cite{roberts-2012} Def. 12: "A strategy of inquiry Strat(q) is a set of questions {q₁, ..., qₙ} such that ... if all the questions in Strat(q) were answered, q would be answered too."

Modeled as a rose tree: each node is a question, children are subquestions whose collective answers resolve the parent.

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

def Discourse.Strategy.question {W : Type u_1} : Strategy W → Core.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 (Core.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 (Core.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 child questions (their joint resolution) entails the parent question.

@cite{roberts-2012} Def. 12: answering all subquestions answers the parent.

This checks only the root node; recurse on sub-strategies for full-tree verification. The meet ⊓ is taken in the inquisitive-content lattice; ⊤ is the trivial issue (resolved by every state).

Equations

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

def Discourse.moveRelevantToStrategy {W : Type u_1} (den : Core.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.

Derived from Core.Question.moveRelevant by treating every question in the strategy tree as a candidate subquestion.

Equations

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