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) and the rose-tree strategy of inquiry decomposing a question into subquestions whose joint resolution answers the parent.

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)).questionEntails 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, q.partiallyAnswers a