Relevance-Parameterized Question Denotations

@cite{van-rooy-2003}

Theory-level constructs from @cite{van-rooy-2003}'s decision-theoretic question semantics. These are general mechanisms, not paper-specific models.

Key Definitions

• RelevanceFunction: Op(P)(w) — relevance-maximal groups per world
• underspecifiedDenotation: ⟦?xPx⟧^R — the unified question denotation
• mentionAllRelevance / mentionSomeRelevance: Standard instantiations of Op
• isDecisionRelevant / decisionRelevantDomain: Domain selection via UV

Design

The RelevanceFunction abstracts over the decision problem: it captures which groups of satisfiers are optimal without exposing the DP's action set or utility function. The DP determines the relevance function; the relevance function determines the question denotation.

This separation matches @cite{van-rooy-2003}'s architecture: §3 defines utility of answers via DPs, §5 defines the question denotation via Op(P), and the connection is that Op(P)(w) collects the groups with maximal relevance/utility.

Op(P): Relevance-Maximal Satisfiers

@cite{van-rooy-2003}, §5 (p. 752–753): Op(P)(w) selects the group(s) of P-satisfiers in world w that are maximally relevant to the agent's decision problem.

structure Theories.Semantics.Questions.Relevance.RelevanceFunction (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A relevance function assigns to each world a set of "optimal groups" of entities — those groups that are maximally relevant to the agent's decision problem.

@cite{van-rooy-2003}, p. 753: ⟦Op(P)⟧^R = {⟨w,g⟩ | P(w)(g) & ¬∃g'[P(w)(g') & P(g') > P(g)]}

• predicate : W → E → Bool

  The predicate (e.g., "sells Italian newspapers")

• optimalGroups : W → List (List E)

  The optimal groups in each world: subsets of satisfiers that are maximally relevant to the decision problem

def Theories.Semantics.Questions.Relevance.mentionAllRelevance {W : Type u_1} {E : Type u_2} [DecidableEq E] (predicate : W → E → Bool) (domain : List E) : RelevanceFunction W E

Standard mention-all: Op(P)(w) = {ext(P)(w)}, the full extension. Only one group per world: all satisfiers together.

Equations

• Theories.Semantics.Questions.Relevance.mentionAllRelevance predicate domain = { predicate := predicate, optimalGroups := fun (w : W) => [List.filter (predicate w) domain] }

def Theories.Semantics.Questions.Relevance.mentionSomeRelevance {W : Type u_1} {E : Type u_2} (predicate : W → E → Bool) (domain : List E) : RelevanceFunction W E

Mention-some relevance: Op(P)(w) = {{a} : P(a)(w)}, each satisfier is its own optimal group. Any single satisfier suffices.

Equations

• One or more equations did not get rendered due to their size.

⟦?xPx⟧^R: The Underspecified Question Denotation

@cite{van-rooy-2003}, §5 (p. 752):

⟦?xPx⟧^R = {λv[g ∈ Op(P)(v)] : w ∈ W & g ∈ Op(P)(w)}

Each "answer" is a proposition saying "group g is among the optimal groups." When Op = mention-all, this reduces to G&S. When Op = mention-some, this produces one answer per satisfier.

def Theories.Semantics.Questions.Relevance.underspecifiedDenotation {W : Type u_1} {E : Type u_2} [BEq E] [BEq (List E)] (rf : RelevanceFunction W E) (worlds : List W) : Core.DecisionTheory.Question W

The relevance-parameterized question denotation ⟦?xPx⟧^R.

@cite{van-rooy-2003}, p. 752.

Equations

• One or more equations did not get rendered due to their size.

Domain Selection

@cite{van-rooy-2003}, §4.2 (p. 745–746): The wh-domain of a question contains exactly those individuals whose P-status is decision-relevant. An individual d is decision-relevant if learning whether P(d) holds has positive utility value.

def Theories.Semantics.Questions.Relevance.isDecisionRelevant {W : Type u_1} [Fintype W] [DecidableEq W] {A : Type u_2} [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem W A) (actions : Finset A) (predicate : W → Bool) : Bool

An individual d is decision-relevant for question ?xP(x) given DP if learning whether P(d) holds has positive utility value.

@cite{van-rooy-2003}, p. 746: d ∈ D_optimal iff knowing P(d) vs ¬P(d) could affect the agent's decision.

Equations

• Theories.Semantics.Questions.Relevance.isDecisionRelevant dp actions predicate = decide (Core.DecisionTheory.utilityValue dp actions {w : W | predicate w = true} > 0)

def Theories.Semantics.Questions.Relevance.decisionRelevantDomain {W : Type u_1} {E : Type u_2} [Fintype W] [DecidableEq W] {A : Type u_3} [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem W A) (actions : Finset A) (predicate : W → E → Bool) (domain : List E) : List E

The decision-relevant domain: entities whose P-status matters for the agent's decision problem.

@cite{van-rooy-2003}, p. 746: D_optimal = {d | UV(P(d)) > 0}.

Equations

• One or more equations did not get rendered due to their size.