QUD Stack: Ordered Accepted-Unanswered Questions

@cite{roberts-2012}

A QUDStack W models the discourse-state component of @cite{roberts-2012} §2: the ordered list of questions that have been accepted as worth answering but have not yet been resolved. Subquestions are pushed on top; answers pop the immediate QUD. Strategies of inquiry (Core/Discourse/Strategy.lean) are the rose-tree counterpart.

Parameterized by Core.Question W — the Set-based inquisitive-content lattice.

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

A QUD stack: ordered list of accepted, unanswered questions. The head is the immediate QUD (most recently accepted question).

@cite{roberts-2012} Def. 10g: "QUD_m = the set of all questions which have been accepted as questions (i.e., accepted as being worth answering) at m, but which have not yet been answered." The stack ordering reflects discourse subordination — subquestions pushed on top.

• questions : List (Core.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 (Core.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 : Core.Question W) : QUDStack W

Accept a new question: push onto the stack. @cite{roberts-2012}: "a subquestion of QUD is pushed onto QUD."

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. @cite{roberts-2012}: "an answer to QUD pops QUD off 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