Erk and Herbelot (2024): How to Marry a Star: Probabilistic Constraints for Meaning in Context

This file formalizes [EH24]'s situation description systems, which model utterance understanding as Bayesian inference over the concepts underlying the words of a sentence, constrained locally by selectional preferences and globally by scenarios. In the graphical model (§5.1, Figure 5; the sampling process in Appendix A) a scenario mix is drawn from a symmetric Dirichlet with concentration α, one scenario per concept node is drawn from the mix, one concept per node is drawn from its scenario's concept distribution, for a role filler from the Product of Experts of that distribution with the role's selectional constraint (p. 570), and each node emits its condition label deterministically. SDS.nodePosterior is the posterior over the concept at one node given the labels of all nodes, mathlib's posterior kernel κ†μ of the deterministic label kernel against the joint, pushed forward to the node, and SDS.nodePosterior_apply is the closed form the paper estimates by WebPPL sampling, a ratio of sums over scenario assignments of per-node fibre masses. The paper's two sentences follow with their posteriors as functions of α. In a player was holding a bat (§5.1, Table 1) the stick sense of bat has posterior (α + 1) / (2α + 1), which strengthens as α decreases (p. 571); in an astronomer married a star (§5.2, Table 2) the person sense has posterior 105α / (115α + 8), so the sun sense strengthens as α decreases (p. 572); and on the star node the selectional constraint prefers STAR-PERSON while the STARGAZING scenario prefers STAR-SUN, the conflict of Figure 6.

Implementation notes

• The Dirichlet prior on the scenario mix is integrated out into the Pólya-urn law of the per-node scenario draws, polyaUrn.
• Ingredients the paper leaves unspecified are set as follows: HOLD-AGENT and MARRY-AGENT get the same constraint as the corresponding theme role, and both cancel since the agent concept is observed; MARRY-THEME gives MARRY itself weight 0, the three stated values already summing to 1.

TODO

• The exact posteriors against the paper's WebPPL estimates from 2000 samples: the astronomer rows, 105/131 ≈ 0.80 and 7/13 ≈ 0.54 against 0.82 and 0.57, are within sampling error; the bat rows, 3/4 and 11/12 against 0.82 and 0.96, are not, and the paper does not describe its WebPPL model in enough detail to locate the difference.

References

• [EH24]

structure ErkHerbelot2024.SDS (S : Type u_1) (C : Type u_2) (R : Type u_3) [MeasurableSpace C] : Type (max (max u_1 u_2) u_3)

A situation description system: the Dirichlet prior on the scenario mix (as a Pólya urn over scenarios), the per-scenario concept distributions, and the per-role selectional constraints.

• prior : S → ℝ

  The parameters of the scenario-mix prior Dirichlet(α, …, α), the weights of the Pólya urn it integrates out to.

• prior_pos (s : S) : 0 < self.prior s

  The Dirichlet parameters are positive.

• scenario : S → MeasureTheory.Measure C

  P(c | s): the concepts a scenario makes available.

• selectional : R → MeasureTheory.Measure C

  P(c | r): the selectional constraint of a semantic role.

noncomputable def ErkHerbelot2024.SDS.poe {S : Type u_1} {C : Type u_2} {R : Type u_3} [MeasurableSpace S] [MeasurableSpace C] [MeasurableSpace R] [Countable S] [MeasurableSingletonClass S] [Countable R] [MeasurableSingletonClass R] [Fintype C] (m : SDS S C R) : ProbabilityTheory.Kernel (S × R) C

Product of Experts (p. 570): the role-filler distribution for scenario s and role r is the normalized pointwise product of scenario s and selectional r. When the two share no concept (fn 10) the row is the zero measure.

Equations

• m.poe = ProbabilityTheory.Kernel.ofWeights fun (p : S × R) (c : C) => (m.scenario p.1) {c} * (m.selectional p.2) {c}

instance ErkHerbelot2024.SDS.instIsFiniteKernelProdPoe {S : Type u_1} {C : Type u_2} {R : Type u_3} [MeasurableSpace S] [MeasurableSpace C] [MeasurableSpace R] [Countable S] [MeasurableSingletonClass S] [Countable R] [MeasurableSingletonClass R] [Fintype C] (m : SDS S C R) : ProbabilityTheory.IsFiniteKernel m.poe

noncomputable def ErkHerbelot2024.SDS.emission {S : Type u_1} {C : Type u_2} {R : Type u_3} [MeasurableSpace S] [MeasurableSpace C] [MeasurableSpace R] [Countable S] [MeasurableSingletonClass S] [Countable R] [MeasurableSingletonClass R] [Fintype C] (m : SDS S C R) (s : S) : Option R → MeasureTheory.Measure C

The concept distribution at one node: a top-level concept (no role) draws from its scenario alone; a role filler draws from the Product of Experts (Appendix A).

Equations

• m.emission s none = m.scenario s
• m.emission s (some r) = m.poe (s, r)

instance ErkHerbelot2024.SDS.instIsFiniteMeasureEmissionOfIsProbabilityMeasureScenario {S : Type u_1} {C : Type u_2} {R : Type u_3} [MeasurableSpace S] [MeasurableSpace C] [MeasurableSpace R] [Countable S] [MeasurableSingletonClass S] [Countable R] [MeasurableSingletonClass R] [Fintype C] (m : SDS S C R) [∀ (s : S), MeasureTheory.IsProbabilityMeasure (m.scenario s)] (s : S) (o : Option R) : MeasureTheory.IsFiniteMeasure (m.emission s o)

theorem ErkHerbelot2024.SDS.emission_univ_le_one {S : Type u_1} {C : Type u_2} {R : Type u_3} [MeasurableSpace S] [MeasurableSpace C] [MeasurableSpace R] [Countable S] [MeasurableSingletonClass S] [Countable R] [MeasurableSingletonClass R] [Fintype C] (m : SDS S C R) [∀ (s : S), MeasureTheory.IsProbabilityMeasure (m.scenario s)] (s : S) (o : Option R) : (m.emission s o) Set.univ ≤ 1

instance ErkHerbelot2024.SDS.instIsProbabilityMeasureForallFinPolyaUrnPrior {S : Type u_1} {C : Type u_2} {R : Type u_3} [Fintype S] [DecidableEq S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [MeasurableSpace C] (m : SDS S C R) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.polyaUrn m.prior n)

noncomputable def ErkHerbelot2024.SDS.emissions {S : Type u_1} {C : Type u_2} {R : Type u_3} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype C] [MeasurableSpace C] [MeasurableSpace R] [Countable R] [MeasurableSingletonClass R] (m : SDS S C R) {n : ℕ} (ρ : Fin n → Option R) : ProbabilityTheory.Kernel (Fin n → S) (Fin n → C)

The concept nodes of an n-node sentence with roles ρ, conditionally independent given their scenarios.

Equations

• m.emissions ρ = ProbabilityTheory.Kernel.ofFunOfCountable fun (s : Fin n → S) => MeasureTheory.Measure.pi fun (i : Fin n) => m.emission (s i) (ρ i)

theorem ErkHerbelot2024.SDS.emissions_apply {S : Type u_1} {C : Type u_2} {R : Type u_3} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype C] [MeasurableSpace C] [MeasurableSpace R] [Countable R] [MeasurableSingletonClass R] (m : SDS S C R) {n : ℕ} (ρ : Fin n → Option R) (s : Fin n → S) : (m.emissions ρ) s = MeasureTheory.Measure.pi fun (i : Fin n) => m.emission (s i) (ρ i)

instance ErkHerbelot2024.SDS.instIsFiniteKernelForallFinEmissions {S : Type u_1} {C : Type u_2} {R : Type u_3} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype C] [MeasurableSpace C] [MeasurableSpace R] [Countable R] [MeasurableSingletonClass R] (m : SDS S C R) [∀ (s : S), MeasureTheory.IsProbabilityMeasure (m.scenario s)] {n : ℕ} (ρ : Fin n → Option R) : ProbabilityTheory.IsFiniteKernel (m.emissions ρ)

noncomputable def ErkHerbelot2024.SDS.joint {S : Type u_1} {C : Type u_2} {R : Type u_3} [Fintype S] [DecidableEq S] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype C] [MeasurableSpace C] [MeasurableSpace R] [Countable R] [MeasurableSingletonClass R] (m : SDS S C R) {n : ℕ} (ρ : Fin n → Option R) : MeasureTheory.Measure ((Fin n → S) × (Fin n → C))

The joint law of scenario and concept assignments (Figure 5, nodes 1–9).

Equations

• m.joint ρ = (ProbabilityTheory.polyaUrn m.prior n).compProd (m.emissions ρ)

instance ErkHerbelot2024.SDS.instIsFiniteMeasureProdForallFinJoint {S : Type u_1} {C : Type u_2} {R : Type u_3} [Fintype S] [DecidableEq S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype C] [MeasurableSpace C] [MeasurableSpace R] [Countable R] [MeasurableSingletonClass R] (m : SDS S C R) [∀ (s : S), MeasureTheory.IsProbabilityMeasure (m.scenario s)] {n : ℕ} (ρ : Fin n → Option R) : MeasureTheory.IsFiniteMeasure (m.joint ρ)

noncomputable def ErkHerbelot2024.SDS.observe {C : Type u_2} {L : Type u_4} [Fintype C] [MeasurableSpace C] [MeasurableSingletonClass C] [MeasurableSpace L] (S : Type u_5) [MeasurableSpace S] [Countable S] [MeasurableSingletonClass S] (label : C → L) (n : ℕ) : ProbabilityTheory.Kernel ((Fin n → S) × (Fin n → C)) (Fin n → L)

Each node emits its condition label deterministically (Figure 5, nodes 10–14).

Equations

• ErkHerbelot2024.SDS.observe S label n = ProbabilityTheory.Kernel.deterministic (fun (ω : (Fin n → S) × (Fin n → C)) (i : Fin n) => label (ω.2 i)) ⋯

instance ErkHerbelot2024.SDS.instIsFiniteKernelProdForallFinObserve {S : Type u_1} {C : Type u_2} {L : Type u_4} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype C] [MeasurableSpace C] [MeasurableSingletonClass C] [MeasurableSpace L] (label : C → L) (n : ℕ) : ProbabilityTheory.IsFiniteKernel (observe S label n)

noncomputable def ErkHerbelot2024.SDS.nodePosterior {S : Type u_1} {C : Type u_2} {R : Type u_3} {L : Type u_4} [Fintype S] [DecidableEq S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype C] [Nonempty C] [MeasurableSpace C] [MeasurableSingletonClass C] [MeasurableSpace R] [Countable R] [MeasurableSingletonClass R] [MeasurableSpace L] (m : SDS S C R) [∀ (s : S), MeasureTheory.IsProbabilityMeasure (m.scenario s)] {n : ℕ} (label : C → L) (ρ : Fin n → Option R) (x : Fin n → L) (t : Fin n) : MeasureTheory.Measure C

The posterior over the concept at node t, given the labels x of all nodes.

Equations

• m.nodePosterior label ρ x t = MeasureTheory.Measure.map (fun (ω : (Fin n → S) × (Fin n → C)) => ω.2 t) ((ProbabilityTheory.posterior (ErkHerbelot2024.SDS.observe S label n) (m.joint ρ)) x)

theorem ErkHerbelot2024.SDS.joint_apply_univ_prod_pi {S : Type u_1} {C : Type u_2} {R : Type u_3} [Fintype S] [DecidableEq S] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype C] [MeasurableSpace C] [MeasurableSingletonClass C] [MeasurableSpace R] [Countable R] [MeasurableSingletonClass R] (m : SDS S C R) [∀ (s : S), MeasureTheory.IsProbabilityMeasure (m.scenario s)] {n : ℕ} (ρ : Fin n → Option R) (T : Fin n → Set C) : (m.joint ρ) (Set.univ ×ˢ Set.univ.pi T) = ∑ s : Fin n → S, (ProbabilityTheory.polyaUrn m.prior n) {s} * ∏ i : Fin n, (m.emission (s i) (ρ i)) (T i)

The joint mass of a box of per-node concept events: a sum over scenario assignments of the urn likelihood times the per-node masses.

theorem ErkHerbelot2024.SDS.nodePosterior_apply {S : Type u_1} {C : Type u_2} {R : Type u_3} {L : Type u_4} [Fintype S] [DecidableEq S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype C] [Nonempty C] [MeasurableSpace C] [MeasurableSingletonClass C] [MeasurableSpace R] [Countable R] [MeasurableSingletonClass R] [MeasurableSpace L] [MeasurableSingletonClass L] (m : SDS S C R) [∀ (s : S), MeasureTheory.IsProbabilityMeasure (m.scenario s)] {n : ℕ} (label : C → L) (ρ : Fin n → Option R) (x : Fin n → L) (t : Fin n) (c : C) (hx : ∑ s : Fin n → S, (ProbabilityTheory.polyaUrn m.prior n) {s} * ∏ i : Fin n, (m.emission (s i) (ρ i)) (label ⁻¹' {x i}) ≠ 0) : (m.nodePosterior label ρ x t) {c} = (∑ s : Fin n → S, (ProbabilityTheory.polyaUrn m.prior n) {s} * ∏ i : Fin n, (m.emission (s i) (ρ i)) {c' : C | label c' = x i ∧ (i = t → c' = c)}) / ∑ s : Fin n → S, (ProbabilityTheory.polyaUrn m.prior n) {s} * ∏ i : Fin n, (m.emission (s i) (ρ i)) (label ⁻¹' {x i})

The node posterior in closed form: the ratio of two scenario-assignment sums of per-node fibre masses — the quantity the paper estimates by sampling.

theorem ErkHerbelot2024.SDS.sum_toReal {S : Type u_1} {C : Type u_2} {R : Type u_3} [Fintype S] [DecidableEq S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype C] [MeasurableSpace C] [MeasurableSpace R] [Countable R] [MeasurableSingletonClass R] (m : SDS S C R) [∀ (s : S), MeasureTheory.IsProbabilityMeasure (m.scenario s)] {n : ℕ} (ρ : Fin n → Option R) (T : Fin n → Set C) : (∑ s : Fin n → S, (ProbabilityTheory.polyaUrn m.prior n) {s} * ∏ i : Fin n, (m.emission (s i) (ρ i)) (T i)).toReal = ∑ s : Fin n → S, ProbabilityTheory.polyaUrnProb m.prior (ProbabilityTheory.countVec s) * ∏ i : Fin n, (m.emission (s i) (ρ i)).real (T i)

The scenario-assignment sums on reals: urn likelihoods times per-node real masses.

Evaluation helpers

A player was holding a bat (§5.1, Figure 5, Table 1)

inductive ErkHerbelot2024.BatConcept : Type

The concept inventory (p. 569).

• BALL : BatConcept
• BAT_ANIMAL : BatConcept
• HOLD : BatConcept
• BAT_STICK : BatConcept
• CANDLE : BatConcept
• CAT : BatConcept
• PLAYER : BatConcept
• STONE : BatConcept
• VAMPIRE : BatConcept

@[instance_reducible]

instance ErkHerbelot2024.instFintypeBatConcept : Fintype BatConcept

Equations

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

@[instance_reducible]

instance ErkHerbelot2024.instDecidableEqBatConcept : DecidableEq BatConcept

Equations

• ErkHerbelot2024.instDecidableEqBatConcept x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive ErkHerbelot2024.BatScenario : Type

The two scenarios (p. 569).

• BASEBALL : BatScenario
• GOTHIC : BatScenario

@[instance_reducible]

instance ErkHerbelot2024.instFintypeBatScenario : Fintype BatScenario

Equations

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

@[instance_reducible]

instance ErkHerbelot2024.instDecidableEqBatScenario : DecidableEq BatScenario

Equations

• ErkHerbelot2024.instDecidableEqBatScenario x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive ErkHerbelot2024.BatRole : Type

The semantic roles of HOLD (p. 569).

• holdAgent : BatRole
• holdTheme : BatRole

@[instance_reducible]

instance ErkHerbelot2024.instFintypeBatRole : Fintype BatRole

Equations

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

@[instance_reducible]

instance ErkHerbelot2024.instDecidableEqBatRole : DecidableEq BatRole

Equations

• ErkHerbelot2024.instDecidableEqBatRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive ErkHerbelot2024.BatLabel : Type

Condition labels: one word form per concept; bat is shared by its two senses.

• ball : BatLabel
• bat : BatLabel
• hold : BatLabel
• candle : BatLabel
• cat : BatLabel
• player : BatLabel
• stone : BatLabel
• vampire : BatLabel

@[instance_reducible]

instance ErkHerbelot2024.instFintypeBatLabel : Fintype BatLabel

Equations

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

@[instance_reducible]

instance ErkHerbelot2024.instDecidableEqBatLabel : DecidableEq BatLabel

Equations

• ErkHerbelot2024.instDecidableEqBatLabel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ErkHerbelot2024.instMeasurableSpaceBatConcept : MeasurableSpace BatConcept

Equations

• ErkHerbelot2024.instMeasurableSpaceBatConcept = ⊤

instance ErkHerbelot2024.instDiscreteMeasurableSpaceBatConcept : DiscreteMeasurableSpace BatConcept

@[instance_reducible]

instance ErkHerbelot2024.instMeasurableSpaceBatScenario : MeasurableSpace BatScenario

Equations

• ErkHerbelot2024.instMeasurableSpaceBatScenario = ⊤

instance ErkHerbelot2024.instDiscreteMeasurableSpaceBatScenario : DiscreteMeasurableSpace BatScenario

@[instance_reducible]

instance ErkHerbelot2024.instMeasurableSpaceBatRole : MeasurableSpace BatRole

Equations

• ErkHerbelot2024.instMeasurableSpaceBatRole = ⊤

instance ErkHerbelot2024.instDiscreteMeasurableSpaceBatRole : DiscreteMeasurableSpace BatRole

@[instance_reducible]

instance ErkHerbelot2024.instMeasurableSpaceBatLabel : MeasurableSpace BatLabel

Equations

• ErkHerbelot2024.instMeasurableSpaceBatLabel = ⊤

instance ErkHerbelot2024.instDiscreteMeasurableSpaceBatLabel : DiscreteMeasurableSpace BatLabel

instance ErkHerbelot2024.instNonemptyBatConcept : Nonempty BatConcept

instance ErkHerbelot2024.instNonemptyBatScenario : Nonempty BatScenario

def ErkHerbelot2024.batLabel : BatConcept → BatLabel

The condition label of each concept (Figure 5, nodes 10–14).

Equations

• ErkHerbelot2024.batLabel ErkHerbelot2024.BatConcept.BALL = ErkHerbelot2024.BatLabel.ball
• ErkHerbelot2024.batLabel ErkHerbelot2024.BatConcept.BAT_ANIMAL = ErkHerbelot2024.BatLabel.bat
• ErkHerbelot2024.batLabel ErkHerbelot2024.BatConcept.HOLD = ErkHerbelot2024.BatLabel.hold
• ErkHerbelot2024.batLabel ErkHerbelot2024.BatConcept.BAT_STICK = ErkHerbelot2024.BatLabel.bat
• ErkHerbelot2024.batLabel ErkHerbelot2024.BatConcept.CANDLE = ErkHerbelot2024.BatLabel.candle
• ErkHerbelot2024.batLabel ErkHerbelot2024.BatConcept.CAT = ErkHerbelot2024.BatLabel.cat
• ErkHerbelot2024.batLabel ErkHerbelot2024.BatConcept.PLAYER = ErkHerbelot2024.BatLabel.player
• ErkHerbelot2024.batLabel ErkHerbelot2024.BatConcept.STONE = ErkHerbelot2024.BatLabel.stone
• ErkHerbelot2024.batLabel ErkHerbelot2024.BatConcept.VAMPIRE = ErkHerbelot2024.BatLabel.vampire

def ErkHerbelot2024.batScenario : BatScenario → Finset BatConcept

The concepts of each scenario: BASEBALL and GOTHIC give equal probability to five concepts each and zero to the rest (p. 569).

Equations

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

def ErkHerbelot2024.holdFiller : Finset BatConcept

HOLD-THEME: 0 for HOLD and 0.125 for each of the eight concrete objects (p. 569). HOLD-AGENT, which the paper leaves unspecified, is set the same way.

Equations

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

noncomputable def ErkHerbelot2024.batSDS (α : ℝ) (hα : 0 < α) : SDS BatScenario BatConcept BatRole

The bat-sentence system with Dirichlet concentration α.

Equations

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

instance ErkHerbelot2024.instIsProbabilityMeasureBatConceptScenarioBatScenarioBatRoleBatSDS (α : ℝ) (hα : 0 < α) (s : BatScenario) : MeasureTheory.IsProbabilityMeasure ((batSDS α hα).scenario s)

def ErkHerbelot2024.batRoles : Fin 3 → Option BatRole

Node roles (Figure 5): the verb node has no role; player fills HOLD-AGENT and bat HOLD-THEME.

Equations

• ErkHerbelot2024.batRoles = ![none, some ErkHerbelot2024.BatRole.holdAgent, some ErkHerbelot2024.BatRole.holdTheme]

def ErkHerbelot2024.batLabels : Fin 3 → BatLabel

The observed labels hold(_), player(_), bat(_) (Figure 5, nodes 12, 10, 14).

Equations

• ErkHerbelot2024.batLabels = ![ErkHerbelot2024.BatLabel.hold, ErkHerbelot2024.BatLabel.player, ErkHerbelot2024.BatLabel.bat]

@[simp]

theorem ErkHerbelot2024.batSDS_prior (α : ℝ) (hα : 0 < α) : (batSDS α hα).prior = fun (x : BatScenario) => α

@[simp]

theorem ErkHerbelot2024.batSDS_scenario (α : ℝ) (hα : 0 < α) (s : BatScenario) : (batSDS α hα).scenario s = ProbabilityTheory.uniformOn ↑(batScenario s)

theorem ErkHerbelot2024.batSDS_poe (α : ℝ) (hα : 0 < α) (s : BatScenario) (r : BatRole) : (batSDS α hα).poe (s, r) = ProbabilityTheory.uniformOn ↑(batScenario s ∩ holdFiller)

A role filler's distribution is uniform on the concepts its scenario and role agree on.

theorem ErkHerbelot2024.batStick_real (α : ℝ) (hα : 0 < α) : ((batSDS α hα).nodePosterior batLabel batRoles batLabels 2).real {BatConcept.BAT_STICK} = (α + 1) / (2 * α + 1)

Table 1 in closed form: the posterior probability of the stick sense of bat in a player was holding a bat is (α + 1) / (2α + 1).

theorem ErkHerbelot2024.batStick_half : ((batSDS (1 / 2) batStick_half._proof_1).nodePosterior batLabel batRoles batLabels 2).real {BatConcept.BAT_STICK} = 3 / 4

Table 1, α = 0.5: P(stick) = 3/4 (paper's simulation: 0.82).

theorem ErkHerbelot2024.batStick_tenth : ((batSDS (1 / 10) batStick_tenth._proof_1).nodePosterior batLabel batRoles batLabels 2).real {BatConcept.BAT_STICK} = 11 / 12

Table 1, α = 0.1: P(stick) = 11/12 (paper's simulation: 0.96).

theorem ErkHerbelot2024.batStick_strictAnti {α β : ℝ} (hα : 0 < α) (hαβ : α < β) : ((batSDS β ⋯).nodePosterior batLabel batRoles batLabels 2).real {BatConcept.BAT_STICK} < ((batSDS α hα).nodePosterior batLabel batRoles batLabels 2).real {BatConcept.BAT_STICK}

The stick preference "grows more pronounced when the concentration parameter α of the Dirichlet distribution is lower" (p. 571): the posterior is strictly decreasing in α.

An astronomer married a star (§5.2, Figure 6, Table 2)

inductive ErkHerbelot2024.StarConcept : Type

The concept inventory (p. 571).

• ASTRONOMER : StarConcept
• STAR_PERSON : StarConcept
• STAR_SUN : StarConcept
• MARRY : StarConcept

@[instance_reducible]

instance ErkHerbelot2024.instFintypeStarConcept : Fintype StarConcept

Equations

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

@[instance_reducible]

instance ErkHerbelot2024.instDecidableEqStarConcept : DecidableEq StarConcept

Equations

• ErkHerbelot2024.instDecidableEqStarConcept x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive ErkHerbelot2024.StarScenario : Type

The two scenarios (p. 571).

• STARGAZING : StarScenario
• STAGE : StarScenario

@[instance_reducible]

instance ErkHerbelot2024.instFintypeStarScenario : Fintype StarScenario

Equations

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

@[instance_reducible]

instance ErkHerbelot2024.instDecidableEqStarScenario : DecidableEq StarScenario

Equations

• ErkHerbelot2024.instDecidableEqStarScenario x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive ErkHerbelot2024.StarRole : Type

The semantic roles of MARRY (p. 571).

• marryAgent : StarRole
• marryTheme : StarRole

@[instance_reducible]

instance ErkHerbelot2024.instFintypeStarRole : Fintype StarRole

Equations

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

@[instance_reducible]

instance ErkHerbelot2024.instDecidableEqStarRole : DecidableEq StarRole

Equations

• ErkHerbelot2024.instDecidableEqStarRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive ErkHerbelot2024.StarLabel : Type

Condition labels; star is shared by its two senses.

• astronomer : StarLabel
• star : StarLabel
• marry : StarLabel

@[instance_reducible]

instance ErkHerbelot2024.instFintypeStarLabel : Fintype StarLabel

Equations

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

@[instance_reducible]

instance ErkHerbelot2024.instDecidableEqStarLabel : DecidableEq StarLabel

Equations

• ErkHerbelot2024.instDecidableEqStarLabel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ErkHerbelot2024.instMeasurableSpaceStarConcept : MeasurableSpace StarConcept

Equations

• ErkHerbelot2024.instMeasurableSpaceStarConcept = ⊤

instance ErkHerbelot2024.instDiscreteMeasurableSpaceStarConcept : DiscreteMeasurableSpace StarConcept

@[instance_reducible]

instance ErkHerbelot2024.instMeasurableSpaceStarScenario : MeasurableSpace StarScenario

Equations

• ErkHerbelot2024.instMeasurableSpaceStarScenario = ⊤

instance ErkHerbelot2024.instDiscreteMeasurableSpaceStarScenario : DiscreteMeasurableSpace StarScenario

@[instance_reducible]

instance ErkHerbelot2024.instMeasurableSpaceStarRole : MeasurableSpace StarRole

Equations

• ErkHerbelot2024.instMeasurableSpaceStarRole = ⊤

instance ErkHerbelot2024.instDiscreteMeasurableSpaceStarRole : DiscreteMeasurableSpace StarRole

@[instance_reducible]

instance ErkHerbelot2024.instMeasurableSpaceStarLabel : MeasurableSpace StarLabel

Equations

• ErkHerbelot2024.instMeasurableSpaceStarLabel = ⊤

instance ErkHerbelot2024.instDiscreteMeasurableSpaceStarLabel : DiscreteMeasurableSpace StarLabel

instance ErkHerbelot2024.instNonemptyStarConcept : Nonempty StarConcept

instance ErkHerbelot2024.instNonemptyStarScenario : Nonempty StarScenario

def ErkHerbelot2024.starLabel : StarConcept → StarLabel

The condition label of each concept.

Equations

• ErkHerbelot2024.starLabel ErkHerbelot2024.StarConcept.ASTRONOMER = ErkHerbelot2024.StarLabel.astronomer
• ErkHerbelot2024.starLabel ErkHerbelot2024.StarConcept.STAR_PERSON = ErkHerbelot2024.StarLabel.star
• ErkHerbelot2024.starLabel ErkHerbelot2024.StarConcept.STAR_SUN = ErkHerbelot2024.StarLabel.star
• ErkHerbelot2024.starLabel ErkHerbelot2024.StarConcept.MARRY = ErkHerbelot2024.StarLabel.marry

def ErkHerbelot2024.starScenario : StarScenario → Finset StarConcept

STARGAZING gives equal probability to ASTRONOMER, STAR-SUN and MARRY; STAGE to STAR-PERSON and MARRY (p. 571).

Equations

• ErkHerbelot2024.starScenario ErkHerbelot2024.StarScenario.STARGAZING = {ErkHerbelot2024.StarConcept.ASTRONOMER, ErkHerbelot2024.StarConcept.STAR_SUN, ErkHerbelot2024.StarConcept.MARRY}
• ErkHerbelot2024.starScenario ErkHerbelot2024.StarScenario.STAGE = {ErkHerbelot2024.StarConcept.STAR_PERSON, ErkHerbelot2024.StarConcept.MARRY}

noncomputable def ErkHerbelot2024.marryFiller : StarConcept → ENNReal

MARRY-THEME (p. 571): 0.475 on ASTRONOMER and on STAR-PERSON, 0.05 on STAR-SUN, and 0 on MARRY. MARRY-AGENT, "with a strong preference for human role fillers" but otherwise unspecified, is set the same way.

Equations

• ErkHerbelot2024.marryFiller ErkHerbelot2024.StarConcept.ASTRONOMER = 19 / 40
• ErkHerbelot2024.marryFiller ErkHerbelot2024.StarConcept.STAR_PERSON = 19 / 40
• ErkHerbelot2024.marryFiller ErkHerbelot2024.StarConcept.STAR_SUN = 1 / 20
• ErkHerbelot2024.marryFiller ErkHerbelot2024.StarConcept.MARRY = 0

noncomputable def ErkHerbelot2024.marryTheme : MeasureTheory.Measure StarConcept

The selectional constraint of MARRY's roles as a measure.

Equations

• ErkHerbelot2024.marryTheme = ∑ c : ErkHerbelot2024.StarConcept, ErkHerbelot2024.marryFiller c • MeasureTheory.Measure.dirac c

@[simp]

theorem ErkHerbelot2024.marryTheme_apply_singleton (c : StarConcept) : marryTheme {c} = marryFiller c

noncomputable def ErkHerbelot2024.starSDS (α : ℝ) (hα : 0 < α) : SDS StarScenario StarConcept StarRole

The astronomer-sentence system with Dirichlet concentration α.

Equations

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

instance ErkHerbelot2024.instIsProbabilityMeasureStarConceptScenarioStarScenarioStarRoleStarSDS (α : ℝ) (hα : 0 < α) (s : StarScenario) : MeasureTheory.IsProbabilityMeasure ((starSDS α hα).scenario s)

@[simp]

theorem ErkHerbelot2024.starSDS_prior (α : ℝ) (hα : 0 < α) : (starSDS α hα).prior = fun (x : StarScenario) => α

@[simp]

theorem ErkHerbelot2024.starSDS_scenario (α : ℝ) (hα : 0 < α) (s : StarScenario) : (starSDS α hα).scenario s = ProbabilityTheory.uniformOn ↑(starScenario s)

def ErkHerbelot2024.starRoles : Fin 3 → Option StarRole

Node roles (Figure 6): astronomer fills MARRY-AGENT, the verb node has no role, star fills MARRY-THEME.

Equations

• ErkHerbelot2024.starRoles = ![some ErkHerbelot2024.StarRole.marryAgent, none, some ErkHerbelot2024.StarRole.marryTheme]

def ErkHerbelot2024.starLabels : Fin 3 → StarLabel

The observed labels astronomer(_), marry(_), star(_).

Equations

• ErkHerbelot2024.starLabels = ![ErkHerbelot2024.StarLabel.astronomer, ErkHerbelot2024.StarLabel.marry, ErkHerbelot2024.StarLabel.star]

theorem ErkHerbelot2024.starSDS_poe (α : ℝ) (hα : 0 < α) : (starSDS α hα).poe = ProbabilityTheory.Kernel.ofWeights fun (p : StarScenario × StarRole) (c : StarConcept) => (ProbabilityTheory.uniformOn ↑(starScenario p.1)) {c} * marryFiller c

A role filler's row is the weight kernel of scenario mass times MARRY's constraint.

theorem ErkHerbelot2024.starPerson_real (α : ℝ) (hα : 0 < α) : ((starSDS α hα).nodePosterior starLabel starRoles starLabels 2).real {StarConcept.STAR_PERSON} = 105 * α / (115 * α + 8)

Table 2 in closed form: the posterior probability of the person sense of star in an astronomer married a star is 105α / (115α + 8).

theorem ErkHerbelot2024.starSun_real (α : ℝ) (hα : 0 < α) : ((starSDS α hα).nodePosterior starLabel starRoles starLabels 2).real {StarConcept.STAR_SUN} = (10 * α + 8) / (115 * α + 8)

The posterior probability of the sun sense of star is (10α + 8) / (115α + 8).

theorem ErkHerbelot2024.starPerson_half : ((starSDS (1 / 2) batStick_half._proof_1).nodePosterior starLabel starRoles starLabels 2).real {StarConcept.STAR_PERSON} = 105 / 131

Table 2, α = 0.5: P(person) = 105/131 ≈ 0.80 (paper's simulation: 0.82).

theorem ErkHerbelot2024.starPerson_tenth : ((starSDS (1 / 10) batStick_tenth._proof_1).nodePosterior starLabel starRoles starLabels 2).real {StarConcept.STAR_PERSON} = 7 / 13

Table 2, α = 0.1: P(person) = 7/13 ≈ 0.54 (paper's simulation: 0.57).

theorem ErkHerbelot2024.starSun_strictAnti {α β : ℝ} (hα : 0 < α) (hαβ : α < β) : ((starSDS β ⋯).nodePosterior starLabel starRoles starLabels 2).real {StarConcept.STAR_SUN} < ((starSDS α hα).nodePosterior starLabel starRoles starLabels 2).real {StarConcept.STAR_SUN}

"The more emphasis there is on a coherent scenario (the lower the value of α), the more probability mass is given to the situation where an astronomer marries a giant ball of plasma" (p. 572): the sun posterior is strictly decreasing in α.

Figure 6: the two constraints on star conflict

theorem ErkHerbelot2024.marryTheme_prefers_person (α : ℝ) (hα : 0 < α) : ((starSDS α hα).selectional StarRole.marryTheme).real {StarConcept.STAR_SUN} < ((starSDS α hα).selectional StarRole.marryTheme).real {StarConcept.STAR_PERSON}

Selectional side: MARRY-THEME prefers the person sense of star to the sun sense (p. 571: 0.475 against 0.05).

theorem ErkHerbelot2024.stargazing_prefers_sun (α : ℝ) (hα : 0 < α) : ((starSDS α hα).scenario StarScenario.STARGAZING).real {StarConcept.STAR_PERSON} < ((starSDS α hα).scenario StarScenario.STARGAZING).real {StarConcept.STAR_SUN}

Scenario side: a coherent STARGAZING scenario prefers the sun sense, which STAR-PERSON is excluded from (p. 571).

theorem ErkHerbelot2024.star_constraints_conflict (α : ℝ) (hα : 0 < α) : ((starSDS α hα).selectional StarRole.marryTheme).real {StarConcept.STAR_SUN} < ((starSDS α hα).selectional StarRole.marryTheme).real {StarConcept.STAR_PERSON} ∧ ((starSDS α hα).scenario StarScenario.STARGAZING).real {StarConcept.STAR_PERSON} < ((starSDS α hα).scenario StarScenario.STARGAZING).real {StarConcept.STAR_SUN}

Figure 6: "either the concept for star conflicts with the selectional constraint, or it conflicts with the preference for a coherent scenario": on the star node the selectional constraint prefers STAR-PERSON while the STARGAZING scenario prefers STAR-SUN.