Waldon et al. (2023): On the Context Dependence of Artifact Noun Interpretation

Waldon, Condoravdi, Levin and Degen ask how a policy goal shapes the boundary of an artifact noun category, as in no electronic devices are allowed in the theater read with the goal of limiting light or of limiting noise. Following Sassoon and Fadlon, an artifact noun denotes an additive, weighted measure over several dimensions. The paper makes the weights contextual: an explicit goal weights the category measure by γ and the goal-relevant feature by 1 − γ, and with no goal stated the goal weight is split by the goals' plausibility. With a uniform threshold and an even prior, the posterior that an object is prohibited is the measure itself. The Goal Insensitive hypothesis is γ = 1; the experiment's Bayesian analysis estimates γ at about 0.76, with 1 outside the credible interval.

Main statements

• prohibitionPosterior_eq: the posterior that an object is prohibited is its measure.
• not_threshold_shift: one goal raising an object and lowering another is not a shift of the standard of comparison.

Implementation notes

Objects and goals are types, and the category, feature and plausibility measures of the norming studies are the fields of Norming, bounded as the slider scales are, in place of values retyped from the paper; every prediction is stated over them and over γ. The posterior is the Bayes ratio with the threshold marginalized by Lebesgue measure on [0, m]. The paper's examples are the rows of Data.Examples.WaldonEtAl2023.

References

• [WCLD23]
• [SF17]
• [Ken07b]
• [LG17]

The norming data and the contextual measure

structure WaldonEtAl2023.Norming (O : Type u_3) (G : Type u_4) [Fintype G] : Type (max u_3 u_4)

The norming studies (§3.1) supply the category-membership measure cat and the goal-relevant feature measures, on the unit interval, and the plausibility of the goals, a distribution.

• cat : O → ℝ
• feature : G → O → ℝ
• plausibility : G → ℝ
• cat_mem (o : O) : self.cat o ∈ Set.Icc 0 1
• feature_mem (g : G) (o : O) : self.feature g o ∈ Set.Icc 0 1
• plausibility_nonneg (g : G) : 0 ≤ self.plausibility g
• plausibility_sum : ∑ g : G, self.plausibility g = 1

inductive WaldonEtAl2023.Condition (G : Type u_3) : Type u_3

An experimental condition states no goal or an explicit policy goal.

• neutral {G : Type u_3} : Condition G
• explicit {G : Type u_3} (g : G) : Condition G

noncomputable def WaldonEtAl2023.measure {O : Type u_1} {G : Type u_2} [Fintype G] (N : Norming O G) (γ : ℝ) : Condition G → O → ℝ

The goal-weighted measure of the artifact noun, (13) under an explicit goal and (14) with the goal weight split by plausibility, is a weighted sum of the category and the goal dimensions.

Equations

• WaldonEtAl2023.measure N γ (WaldonEtAl2023.Condition.explicit g) = fun (o : O) => γ * N.cat o + (1 - γ) * N.feature g o
• WaldonEtAl2023.measure N γ WaldonEtAl2023.Condition.neutral = fun (o : O) => γ * N.cat o + (1 - γ) * ∑ g : G, N.plausibility g * N.feature g o

theorem WaldonEtAl2023.measure_explicit {O : Type u_1} {G : Type u_2} [Fintype G] (N : Norming O G) (γ : ℝ) (g : G) (o : O) : measure N γ (Condition.explicit g) o = γ * N.cat o + (1 - γ) * N.feature g o

theorem WaldonEtAl2023.mix_mem_Icc {O : Type u_1} {G : Type u_2} [Fintype G] (N : Norming O G) (o : O) : ∑ g : G, N.plausibility g * N.feature g o ∈ Set.Icc 0 1

The plausibility-weighted feature lies on the unit interval.

theorem WaldonEtAl2023.measure_mem_Icc {O : Type u_1} {G : Type u_2} [Fintype G] (N : Norming O G) (γ : ℝ) (hγ0 : 0 ≤ γ) (hγ1 : γ ≤ 1) (c : Condition G) (o : O) : measure N γ c o ∈ Set.Icc 0 1

For γ on the unit interval the measure lies on the unit interval, as the threshold reads it.

The interpretive model (12)

noncomputable def WaldonEtAl2023.meetsProb (m : ℝ) : ENNReal

The probability that a measure meets a standard uniform on the unit interval is the Lebesgue mass of [0, m].

Equations

• WaldonEtAl2023.meetsProb m = MeasureTheory.volume (Set.Icc 0 m)

theorem WaldonEtAl2023.meetsProb_eq (m : ℝ) : meetsProb m = ENNReal.ofReal m

noncomputable def WaldonEtAl2023.prohibitionPosterior (m : ℝ) : ENNReal

The posterior that an object of measure m is prohibited is the Bayes ratio of (12) with an even prior and the threshold marginalized.

Equations

• WaldonEtAl2023.prohibitionPosterior m = 2⁻¹ * WaldonEtAl2023.meetsProb m / (2⁻¹ * WaldonEtAl2023.meetsProb m + 2⁻¹ * (1 - WaldonEtAl2023.meetsProb m))

theorem WaldonEtAl2023.prohibitionPosterior_eq {m : ℝ} (hm1 : m ≤ 1) : prohibitionPosterior m = ENNReal.ofReal m

The posterior is the measure.

theorem WaldonEtAl2023.prohibitionPosterior_lt_iff {m m' : ℝ} (hm0 : 0 ≤ m) (hm1 : m ≤ 1) (hm1' : m' ≤ 1) : prohibitionPosterior m < prohibitionPosterior m' ↔ m < m'

Every prediction is a comparison of measures.

Goal sensitivity (§4.3)

theorem WaldonEtAl2023.measure_one {O : Type u_1} {G : Type u_2} [Fintype G] (N : Norming O G) (c c' : Condition G) (o : O) : measure N 1 c o = measure N 1 c' o

Under the Goal Insensitive hypothesis, γ = 1, no condition moves any object.

theorem WaldonEtAl2023.measure_explicit_lt {O : Type u_1} {G : Type u_2} [Fintype G] (N : Norming O G) (γ : ℝ) (hγ : γ < 1) {g g' : G} {o : O} (h : N.feature g o < N.feature g' o) : measure N γ (Condition.explicit g) o < measure N γ (Condition.explicit g') o

Under Goal Sensitivity, an object's measure across explicit goals orders by its goal-relevant features.

theorem WaldonEtAl2023.measure_explicit_sub_neutral {O : Type u_1} {G : Type u_2} [Fintype G] (N : Norming O G) (γ : ℝ) (g : G) (o : O) : measure N γ (Condition.explicit g) o - measure N γ Condition.neutral o = (1 - γ) * (N.feature g o - ∑ g' : G, N.plausibility g' * N.feature g' o)

An explicit goal moves an object away from the neutral baseline by the goal weight times the excess of the goal's feature over the plausibility-weighted mix.

theorem WaldonEtAl2023.measure_bidirectional {O : Type u_1} {G : Type u_2} [Fintype G] (N : Norming O G) (γ : ℝ) (hγ : γ < 1) {g : G} {o o' : O} (ho : ∑ g' : G, N.plausibility g' * N.feature g' o < N.feature g o) (ho' : N.feature g o' < ∑ g' : G, N.plausibility g' * N.feature g' o') : measure N γ Condition.neutral o < measure N γ (Condition.explicit g) o ∧ measure N γ (Condition.explicit g) o' < measure N γ Condition.neutral o'

Under Goal Sensitivity one goal raises an object whose feature exceeds the mix and lowers one whose feature falls short of it, the flashlight and the boombox under the goal of limiting light.

theorem WaldonEtAl2023.not_threshold_shift {O : Type u_1} (m : O → ℝ) (θ θ' : ℝ) (o o' : O) : ¬((m o < θ ∧ θ' ≤ m o) ∧ θ ≤ m o' ∧ m o' < θ')

No single shift of the standard of comparison is bidirectional. With one measure and two thresholds, an object included under the second but not the first and another included under the first but not the second cannot both exist.