Distributional Common Ground

@cite{anderson-2021}

A non-negative real-valued weight function over worlds, refining @cite{stalnaker-2002}'s sharp set-membership context set with graded plausibility. The probabilistic counterpart of Core.CommonGround.CG W.

Substrate role

This file hosts:

• The DistributionalCG W structure with the weight_nonneg invariant.
• The HasContextSet (DistributionalCG W) W instance projecting to the positive-weight subset.
• The HasSupport ℝ instance enabling the polymorphic CommitmentSpace W G substrate to be hosted at G = ℝ.
• The toCommitmentSpace bridge from DistributionalCG W to Dialogue.Krifka.CommitmentSpace W ℝ, plus the support-equivalence theorem.

The Anderson 2021 study (Phenomena/Dialogue/Studies/Anderson2021.lean) imports this substrate and adds the conversation-update + RSA-bridge content on top.

Why no [CommitmentGrade ℝ]

HasSupport ℝ is provided (support g := 0 < g); CommitmentGrade ℝ is NOT, because the involution law support (complement g) ↔ ¬ support g fails on unrestricted reals (e.g., 0 < 1 - 1/2 = 1/2 AND 0 < 1/2). A future CommitmentGrade NNReal or CommitmentGrade Probability instance with proper laws over [0,1] would unlock graded bipolar questions for probabilistic frameworks.

structure Dialogue.DistributionalCG (W : Type u_1) : Type u_1

A distributional common ground: a non-negative weight function over worlds (@cite{anderson-2021}). The probabilistic counterpart of @cite{stalnaker-2002}'s context set — instead of a sharp membership predicate (W → Prop), the CG assigns graded plausibility (W → ℝ).

• weight : W → ℝ
• weight_nonneg (w : W) : 0 ≤ self.weight w

noncomputable def Dialogue.DistributionalCG.uniform {W : Type u_1} : DistributionalCG W

Uniform distributional CG: all worlds equally plausible (empty CG).

Equations

• Dialogue.DistributionalCG.uniform = { weight := fun (x : W) => 1, weight_nonneg := ⋯ }

def Dialogue.DistributionalCG.toContextSet {W : Type u_1} (cg : DistributionalCG W) : Core.CommonGround.ContextSet W

Bridge to classical context set: a world is "in the context" iff its weight is positive. Recovers @cite{stalnaker-2002}'s set-membership view from the distributional representation.

Equations

• cg.toContextSet w = (0 < cg.weight w)

theorem Dialogue.DistributionalCG.uniform_toContextSet {W : Type u_1} : uniform.toContextSet = Core.CommonGround.ContextSet.trivial

Uniform distributional CG maps to the trivial context set.

theorem Dialogue.DistributionalCG.zero_weight_excluded {W : Type u_1} (cg : DistributionalCG W) (w : W) (h : cg.weight w = 0) : ¬cg.toContextSet w

A world with zero weight is excluded from the classical context set.

@[implicit_reducible]

instance Dialogue.instHasContextSetDistributionalCG {W : Type u_1} : Core.CommonGround.HasContextSet (DistributionalCG W) W

A distributional CG projects to a context set: worlds with positive weight.

Equations

• Dialogue.instHasContextSetDistributionalCG = { toContextSet := Dialogue.DistributionalCG.toContextSet }

@[implicit_reducible]

instance Dialogue.instHasSupportReal : Core.Discourse.Commitment.HasSupport ℝ

[HasSupport ℝ] instance for distributional CGs. support g := 0 < g matches Anderson's "world has positive weight iff in CG" projection (cf. DistributionalCG.toContextSet).

Provides ONLY HasSupport ℝ, NOT CommitmentGrade ℝ: the latter would require the involution law on complement, which fails on unrestricted reals. See module docstring.

Equations

• Dialogue.instHasSupportReal = { support := fun (g : ℝ) => 0 < g }

noncomputable def Dialogue.DistributionalCG.toCommitmentSpace {W : Type u_1} (cg : DistributionalCG W) : Krifka.CommitmentSpace W ℝ

Bridge: a distributional CG embeds into a commitment space at G = ℝ. The speaker's distributional weights become a single commit speaker .doxastic weight entry in the root.

Note: the weight_nonneg constraint on DistributionalCG is NOT propagated into CommitmentSpace W ℝ — the substrate doesn't enforce non-negativity. The bridge is sound in the support-projection direction but loses Anderson's structural invariant.

Equations

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

theorem Dialogue.DistributionalCG.toCommitmentSpace_support {W : Type u_1} (cg : DistributionalCG W) (w : W) : cg.toCommitmentSpace.toContextSet w ↔ cg.toContextSet w

Bridge theorem: the support of a distributional CG equals the toContextSet projection of the bridged commitment space. Demonstrates that the polymorphic substrate at G = ℝ faithfully captures Anderson's distributional CG when projected to its support.