Documentation

Linglib.Theories.Semantics.Probabilistic.SDS.ConceptNode

Concept node for SDS #

A concept node in the SDS graphical model (@cite{erk-herbelot-2024} Figure 5 nodes (5), (8), (9); paper §5.1). Each unary predicate in the DRS pairs with a concept-node random variable whose value is a concept drawn from a distribution determined by:

  1. Its associated scenario node (provides P(c | s) — paper §5.1 p. 569: scenario nodes "express their preferences through a multinomial distribution over concepts")
  2. Its associated semantic role node (provides selectional preference P(c | role) — paper §5.1 p. 569: the role-conditional is "again a multinomial distribution over concepts")

The two are combined via Product of Experts at the concept node:

P(c | scenario, role) ∝ P(c | s) · P(c | role)

Both factors are PMFs (paper p. 569: "P(c | hold-theme) = 0 for c=hold; 0.125 else" — and 8 × 0.125 = 1.0 over the 8 concrete objects in the inventory). PoE on two PMFs has bounded total mass (≤ 1), so the finiteness hypothesis on PMF.normalize is automatic.

This file provides the typed primitives for those two contributions and their PoE combination at a single concept node. The graphical-model assembly (SDS/GraphicalModel.lean, Phase 2) composes these across all concept nodes in a DRS.

Cross-reference: legacy ℚ-valued selectional substrate #

A parallel substrate (formerly Theories/Semantics/Verb/SelectionalPreferences.lean; deleted as graduation-rule violation 0.231.X) uses Concept → ℚ (Resnik 1996 + Erk 2007 + Erk-Herbelot 2024). Its RoleWithConstraint Concept is the ℚ analogue of SelectionalDist Role Concept here. Full unification (promoting the legacy file to ℝ≥0∞ + PMF) is a separate project. Prefer this PMF version for new SDS work.

Design choice: α → PMF β, not Kernel α β #

We work at the PMF level (not mathlib's measure-theoretic Kernel) because all our spaces are finite, composition via PMF.bind is enough for SDS/GraphicalModel.lean, and avoiding [MeasurableSpace] keeps signatures clean. Lifting to Kernel is only needed if downstream work requires disintegration/Radon-Nikodym lemmas.

source
@[reducible, inline]
abbrev Semantics.Probabilistic.SDS.ConceptNode.PerScenarioDist (Scenario Concept : Type) :
Type

Per-scenario concept distribution: P(c | s). The scenario contribution to the concept node, paper §5.1 p. 569 ("scenario nodes express their preferences through a multinomial distribution over concepts").

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Semantics.Probabilistic.SDS.ConceptNode.SelectionalDist (Role Concept : Type) :
    Type

    Per-role selectional preference: P(c | role). The role contribution to the concept node, paper §5.1 p. 569: the role-conditional "is again associated with a selectional constraint, which is expressed as a multinomial distribution over concepts." Paper-faithful: PMF, not an unnormalized weight (paper's P(c | hold-theme) = 0.125 ×8 = 1.0 over the 8 holdable concrete objects).

    Equations
    Instances For
      source
      noncomputable def Semantics.Probabilistic.SDS.ConceptNode.conditionalAt {Scenario Concept Role : Type} (perScenario : PerScenarioDist Scenario Concept) (sel : SelectionalDist Role Concept) (s : Scenario) (r : Role) (h_pos : ∑' (c : Concept), (perScenario s) c * (sel r) c ≠ 0) :
      PMF Concept

      The conditional concept distribution at a node, given a fixed scenario and a fixed role. Combines the per-scenario distribution with the role's selectional preference via Product of Experts (paper §5.1 p. 569 formula: P(c | s, r) ∝ P(c | s) · P(c | r)).

      Hypothesis: at least one concept must have non-zero mass under both factors (paper @cite{erk-herbelot-2024} fn 10). The finiteness of the sum is automatic: both factors are PMFs, so ∑ p · q ≤ ∑ p = 1.

      Equations
      Instances For
        source
        @[simp]
        theorem Semantics.Probabilistic.SDS.ConceptNode.conditionalAt_apply {Scenario Concept Role : Type} (perScenario : PerScenarioDist Scenario Concept) (sel : SelectionalDist Role Concept) (s : Scenario) (r : Role) (h_pos : ∑' (c : Concept), (perScenario s) c * (sel r) c ≠ 0) (c : Concept) :
        (conditionalAt perScenario sel s r h_pos) c = (perScenario s) c * (sel r) c * (∑' (x : Concept), (perScenario s) x * (sel r) x)⁻¹
        source
        noncomputable def Semantics.Probabilistic.SDS.ConceptNode.conditionalKernel {Scenario Concept Role : Type} (perScenario : PerScenarioDist Scenario Concept) (sel : SelectionalDist Role Concept) (s : Scenario) (r : Role) :
        Option (PMF Concept)

        The conditional kernel produces a PMF only when the per-scenario and selectional distributions agree on at least one concept (paper fn 10). Returns an Option: none is the pathological "no agreement" case.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Semantics.Probabilistic.SDS.ConceptNode.mem_support_conditionalAt_iff {Scenario Concept Role : Type} (perScenario : PerScenarioDist Scenario Concept) (sel : SelectionalDist Role Concept) (s : Scenario) (r : Role) (h_pos : ∑' (c : Concept), (perScenario s) c * (sel r) c ≠ 0) (c : Concept) :
          c ∈ (conditionalAt perScenario sel s r h_pos).support ↔ (perScenario s) c ≠ 0 ∧ (sel r) c ≠ 0

          The PoE support is the intersection of the per-scenario and selectional supports (paper @cite{erk-herbelot-2024} fn 10's caveat made formal).

          source
          theorem Semantics.Probabilistic.SDS.ConceptNode.conditionalAt_self {Scenario Concept Role : Type} (perScenario : PerScenarioDist Scenario Concept) (sel : SelectionalDist Role Concept) (s : Scenario) (r : Role) (h_pos : ∑' (c : Concept), (perScenario s) c * (sel r) c ≠ 0) (h_eq : sel r = perScenario s) (c : Concept) :
          (conditionalAt perScenario sel s r h_pos) c = (perScenario s) c ^ 2 * (∑' (x : Concept), (perScenario s) x ^ 2)⁻¹

          PoE-with-self identity: when the selectional preference equals the per-scenario distribution, the conditional is perScenario s weighted by itself (sq-and-renormalize). A useful sanity check on the PoE combinator behavior.

          source
          theorem Semantics.Probabilistic.SDS.ConceptNode.conditionalAt_perScenario_uniform {Scenario Concept Role : Type} [Fintype Concept] [Nonempty Concept] (perScenario : PerScenarioDist Scenario Concept) (sel : SelectionalDist Role Concept) (s : Scenario) (r : Role) (h_uniform : perScenario s = PMF.uniformOfFintype Concept) (h_pos : ∑' (c : Concept), (perScenario s) c * (sel r) c ≠ 0) (c : Concept) :
          (conditionalAt perScenario sel s r h_pos) c = (sel r) c

          The genuine paper §4 reduction: when the per-scenario distribution is uniform over the concept space — equivalently, when the model has no scenario contribution at the concept node (paper §4 = "selectional constraints only," no scenario-mix node) — the conditional reduces to the selectional PMF unchanged. The PoE with uniform is the identity (up to renormalization, which is also trivial since selectional already sums to 1).