SDS graphical model: multi-node assembly

The directed graphical model of @cite{erk-herbelot-2024} §5.1, Figure 5 (bat-in-player) and Figure 6 (astronomer-married-star). An utterance with multiple concept-nodes is modelled by:

1. A scenario-mix latent at the top (paper Figure 5 node 1) — a distribution over scenarios, sampled from a symmetric Dirichlet(α).
2. Per-concept-node scenario variables (Figure 5 nodes 2, 3, 4) — each independently sampled from the scenario-mix.
3. Per-concept-node concept variables (Figure 5 nodes 5, 8, 9) — each conditional on its scenario node AND its semantic role node, combined via Product of Experts (paper §5.1 p. 569 formula).
4. Observation nodes (Figure 5 nodes 10–14) — observed condition labels (the surface word forms in the DRS) that constrain which concepts are admissible at each node.

This file gives the typed assembly: a GraphicalModel carries the utterance-independent ingredients (per-scenario distributions, selectional preferences, α), and the per-utterance shape (number of concept-nodes, their roles, observed-concept restrictions) is supplied to jointFactor.

Honest scope

We do not represent the simplex-valued scenario-mix node directly (no continuous Dirichlet in mathlib — see SDS/ScenarioMix.lean's "Honest scope"). Instead we use the marginal likelihood of scenario assignments under the symmetric Dirichlet(α) prior, which equals PolyaUrn.symmetric.seqProb (counts of scenarioAssign) by D-M conjugacy. This is enough for paper Tables 1–2 since those tables report posteriors over concept assignments, not over the scenario mixture itself.

Generative story → joint factor

By the paper's generative process (§5.1 p. 567+, formal version p. 579):

P(s_1..s_n, c_1..c_n | roles_1..roles_n)
  ∝ seqProb_α(counts(s_1..s_n))                  -- D-M scenario likelihood
    × ∏_i  perScenario(s_i, c_i)                  -- scenario→concept
    × ∏_i  selectional(roles_i, c_i)              -- role→concept

The unnormalized joint at a specific assignment is jointFactor below. Normalizing over all assignments consistent with observations gives the joint posterior (in SDS/JointPosterior.lean, Phase 2 part B).

structure Semantics.Probabilistic.SDS.GraphicalModel (Scenario Concept Role : Type) : Type

An SDS graphical model: utterance-independent ingredients. The sentence-specific data (n nodes, their roles, observations) is supplied to jointFactor and jointPosterior below.

• perScenario : Scenario → PMF Concept

  Per-scenario concept distribution P(c | s). Same across nodes.

• selectional : Role → PMF Concept

  Per-role selectional preference P(c | role).

• alpha : ℝ

  Dirichlet concentration α governing scenario-mix sparsity.

• alphaPos : 0 < self.alpha

  α must be strictly positive (Dirichlet hyperparameter requirement).

def Semantics.Probabilistic.SDS.GraphicalModel.counts {Scenario : Type} [DecidableEq Scenario] {n : ℕ} (sAssign : Fin n → Scenario) (s : Scenario) : ℕ

Count of how many concept-nodes were assigned scenario s in the assignment sAssign.

Equations

• Semantics.Probabilistic.SDS.GraphicalModel.counts sAssign s = {x : Fin n | sAssign x = s}.card

noncomputable def Semantics.Probabilistic.SDS.GraphicalModel.jointFactor {Scenario Concept Role : Type} [Fintype Scenario] [DecidableEq Scenario] (m : GraphicalModel Scenario Concept Role) {n : ℕ} (roles : Fin n → Role) (sAssign : Fin n → Scenario) (cAssign : Fin n → Concept) : ENNReal

The unnormalized joint factor at a specific (scenarioAssignment, conceptAssignment) configuration given roles. By the SDS generative process (paper §5.1 + appendix p. 579):

factor(s, c | roles) =
  seqProb_α(counts(s)) · ∏_i perScenario(s_i, c_i) · selectional(roles_i, c_i)

The seqProb factor is the marginal likelihood of the scenario assignment under the symmetric Dirichlet(α) prior, by D-M conjugacy (the simplex is integrated out).

Equations

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

@[reducible, inline]

abbrev Semantics.Probabilistic.SDS.GraphicalModel.Observations (Concept : Type) (n : ℕ) : Type

An observation at a concept-node: the finite set of concepts admissible under the observed condition label (e.g., observing the word "bat" admits {bat-animal, bat-stick}; observing "player" admits {player}).

Equations

• Semantics.Probabilistic.SDS.GraphicalModel.Observations Concept n = (Fin n → Finset Concept)

def Semantics.Probabilistic.SDS.GraphicalModel.Consistent {n : ℕ} {Concept : Type} (cAssign : Fin n → Concept) (obs : Observations Concept n) : Prop

A concept assignment is consistent with observations when each node's assigned concept is in the admissible set.

Equations

• Semantics.Probabilistic.SDS.GraphicalModel.Consistent cAssign obs = ∀ (i : Fin n), cAssign i ∈ obs i

@[implicit_reducible]

instance Semantics.Probabilistic.SDS.GraphicalModel.instDecidableConsistentOfMemFinset {n : ℕ} {Concept : Type} (cAssign : Fin n → Concept) (obs : Observations Concept n) [(i : Fin n) → Decidable (cAssign i ∈ obs i)] : Decidable (Consistent cAssign obs)

Equations

• Semantics.Probabilistic.SDS.GraphicalModel.instDecidableConsistentOfMemFinset cAssign obs = Fintype.decidableForallFintype

noncomputable def Semantics.Probabilistic.SDS.GraphicalModel.jointFactorObs {Scenario Concept Role : Type} [Fintype Scenario] [DecidableEq Scenario] (m : GraphicalModel Scenario Concept Role) {n : ℕ} [Fintype Concept] [DecidableEq Concept] (roles : Fin n → Role) (obs : Observations Concept n) (sAssign : Fin n → Scenario) (cAssign : Fin n → Concept) : ENNReal

The unnormalized joint factor restricted to assignments consistent with observations. Zero on inconsistent assignments.

Equations

• m.jointFactorObs roles obs sAssign cAssign = if Semantics.Probabilistic.SDS.GraphicalModel.Consistent cAssign obs then m.jointFactor roles sAssign cAssign else 0

theorem Semantics.Probabilistic.SDS.GraphicalModel.jointFactor_eq_zero_of_perScenario_zero {Scenario Concept Role : Type} [Fintype Scenario] [DecidableEq Scenario] [Nonempty Scenario] (m : GraphicalModel Scenario Concept Role) {n : ℕ} (roles : Fin n → Role) (sAssign : Fin n → Scenario) (cAssign : Fin n → Concept) {i : Fin n} (h : (m.perScenario (sAssign i)) (cAssign i) = 0) : m.jointFactor roles sAssign cAssign = 0

The joint factor is zero if any concept-node has zero per-scenario probability — a single zero in the per-node product zeros the whole. The discharge tool for proving "this configuration contributes nothing to the posterior" inside paper-replication theorems.

theorem Semantics.Probabilistic.SDS.GraphicalModel.jointFactor_eq_zero_of_selectional_zero {Scenario Concept Role : Type} [Fintype Scenario] [DecidableEq Scenario] [Nonempty Scenario] (m : GraphicalModel Scenario Concept Role) {n : ℕ} (roles : Fin n → Role) (sAssign : Fin n → Scenario) (cAssign : Fin n → Concept) {i : Fin n} (h : (m.selectional (roles i)) (cAssign i) = 0) : m.jointFactor roles sAssign cAssign = 0

The joint factor is zero if any concept-node has zero selectional weight at its role. Companion to jointFactor_eq_zero_of_perScenario_zero.

theorem Semantics.Probabilistic.SDS.GraphicalModel.jointFactorObs_eq_zero_of_inconsistent {Scenario Concept Role : Type} [Fintype Scenario] [DecidableEq Scenario] [Nonempty Scenario] (m : GraphicalModel Scenario Concept Role) {n : ℕ} [Fintype Concept] [DecidableEq Concept] (roles : Fin n → Role) (obs : Observations Concept n) (sAssign : Fin n → Scenario) (cAssign : Fin n → Concept) (h : ¬Consistent cAssign obs) : m.jointFactorObs roles obs sAssign cAssign = 0

Companion: jointFactorObs is zero on observation-inconsistent assignments, by definition. Used explicitly (via exact) in h_supp discharge; not @[simp] because the hypothesis-form would over-fire.