Documentation

Linglib.Discourse.QUD.Basic

Questions under discussion: stack and strategy #

Roberts (2012) gives the inquiry coordinate of the conversational scoreboard. It is the stack of accepted but unanswered questions, a List (Question W) with the immediate QUD at its head, well formed when each question is a contextual subquestion of every question below it (definition (10g), List.Pairwise (Question.IsSubquestionOf C)). This file also defines strategies of inquiry as rose trees of questions (Strategy, (12); Büring's 2003 d-trees are the explicit tree-shaped ancestor), strategy completeness (IsComplete, a licensing condition on each local tree), and relevance of a move's denotation to a set of questions (Question.IsRelevantTo, built from the assertion clause of Relevance (15)). Ginzburg's (2012) KoS models the same coordinate as a partially ordered set with its own update rules, which lives with the gameboard in Discourse/Gameboard/. Beaver, Roberts, Simons and Tonhauser (2017) survey the framework, and Riester (2019) gives reconstruction rules and well-formedness constraints for QUD trees over corpus data.

Main definitions #

Implementation notes #

Definition (10g) makes QUD a function from moves to ordered sets of accepted, unanswered questions; a List (Question W) 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 List.Pairwise (Question.IsSubquestionOf C), relative to a context set because entailment in (9) is contextual throughout. The paper warns against strengthening (iii) to question entailment (the bridging-question discourse (13) violates it). Questions are retired when answered or determined practically unanswerable, and the paper 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.

Definition (12) gives 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 Büring (2003). A strategy read off well-formed stacks has every question of a subtree a contextual subquestion of that subtree's root, and since the relation is not transitive WellFormed states this for every ancestor, not only the parent. IsComplete is the success criterion the 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 Ippolito, Kiss and Williams (2025) 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.

References #

source
@[reducible, inline]
abbrev Discourse.Strategy (W : Type u_1) :
Type u_1

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

Equations
Instances For
    source
    inductive Discourse.Strategy.WellFormed {W : Type u_1} (C : Set W) :
    Strategy W → Prop

    A strategy is well formed in the context C when every question in a subtree is a contextual subquestion of that subtree's root ([Rob12] definition (12), the strategies read off the stacks of (10g)).

    Instances For
      source
      theorem Discourse.Strategy.WellFormed.leaf {W : Type u_1} (C : Set W) (q : Question W) :
      WellFormed C (RoseTree.leaf q)
      source
      @[simp]
      theorem Discourse.Strategy.wellFormed_node_iff {W : Type u_1} {C : Set W} {q : Question W} {cs : List (Strategy W)} :
      WellFormed C (RoseTree.node q cs) ↔ (∀ c ∈ cs, ∀ r ∈ RoseTree.values c, Question.IsSubquestionOf C r q) ∧ ∀ c ∈ cs, WellFormed C c
      source
      theorem Discourse.Strategy.WellFormed.isSubquestionOf_root {W : Type u_1} {C : Set W} {t : Strategy W} :
      WellFormed C t → ∀ r ∈ RoseTree.values t, Question.IsSubquestionOf C r (RoseTree.value t)

      Every question of a well-formed strategy is a contextual subquestion of its root.

      source
      def Discourse.Strategy.IsComplete {W : Type u_1} (t : Strategy W) :
      Prop

      A strategy is complete when at every branching node the meet of the children's questions entails the parent's question, so that jointly resolving the subquestions resolves the parent. Each local tree is licensed by entailment, and terminal nodes are trivially complete.

      Equations
      Instances For
        source
        @[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 ≤ q) ∧ ∀ c ∈ cs, c.IsComplete
        source
        theorem Discourse.Strategy.IsComplete.node {W : Type u_1} {q : Question W} {cs : List (Strategy W)} (complete : cs ≠ [] → (↑(List.map RoseTree.value cs)).inf ≤ q) (children : ∀ c ∈ cs, c.IsComplete) :
        IsComplete (RoseTree.node q cs)
        source
        theorem Discourse.Strategy.IsComplete.leaf {W : Type u_1} (q : Question W) :
        IsComplete (RoseTree.leaf q)
        source
        theorem Discourse.Strategy.IsComplete.node_pair {W : Type u_1} {q : Question W} {s t : Strategy W} (h : RoseTree.value s ⊓ RoseTree.value t ≤ q) (hs : s.IsComplete) (ht : t.IsComplete) :
        IsComplete (RoseTree.node q [s, t])

        Under 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.