Cao, White & Lassiter 2025: graded causative verb semantics

This file formalizes the graded-causative analysis of English cause, make, and force from [CWL25]. On that account, acceptability tracks three measures defined in one structural causal model: Pearl's probability of sufficiency ([Pea19], Causation.SEM.probSufficiency), a simplified [HKW18] degree of intention (intentionDegree), and the number of alternative actions available to the causee (altCount). The models are time-indexed (CausalGraph.TimeIndex), and their agents play a soft-optimality policy (softOptimalPolicy). The model apparatus is shared with [CGK+23].

The paper's in-text judgments (its examples (3)–(11)) are stored as rows in Data/Examples/CaoWhiteLassiter2025.json. Regression estimates remain in prose; no single measure reliably determines verb choice, and each verb's per-verb model has a distinct set of reliable interaction terms.

References

• A. Cao, A. S. White, D. Lassiter, Cause, make, and force as graded causatives

Soft-optimality policy

The paper's mechanism for agent moves (§2.1.1): the highest-utility move — minimax over the game tree, with terminal utility Winner × (EmptySpace + 1) — is taken with probability ρ + (1−ρ)/n, every other available move with (1−ρ)/n (softOptimalPolicy_apply_best, softOptimalPolicy_apply_of_ne). The skill parameter ρ interpolates between a uniformly random player ("assume that the players are infants", softOptimalPolicy_zero) — the limiting case under which the paper's worked SUF contrast between contexts collapses — and a deterministic professional (softOptimalPolicy_one).

noncomputable def CaoWhiteLassiter2025.softOptimalPolicy {A : Type u_1} [Fintype A] [Nonempty A] (best : A) (ρ : NNReal) (hρ : ρ ≤ 1) : PMF A

The move distribution of a player of skill ρ: the highest-utility move best with probability ρ, otherwise a uniform random move.

Equations

• CaoWhiteLassiter2025.softOptimalPolicy best ρ hρ = PMF.mix ρ hρ (PMF.uniformOfFintype A) (PMF.pure best)

@[simp]

theorem CaoWhiteLassiter2025.softOptimalPolicy_apply_best {A : Type u_1} [Fintype A] [Nonempty A] (best : A) (ρ : NNReal) (hρ : ρ ≤ 1) : (softOptimalPolicy best ρ hρ) best = ↑ρ + ↑(1 - ρ) / ↑(Fintype.card A)

@[simp]

theorem CaoWhiteLassiter2025.softOptimalPolicy_apply_of_ne {A : Type u_1} [Fintype A] [Nonempty A] (best : A) (ρ : NNReal) (hρ : ρ ≤ 1) {a : A} (h : a ≠ best) : (softOptimalPolicy best ρ hρ) a = ↑(1 - ρ) / ↑(Fintype.card A)

theorem CaoWhiteLassiter2025.softOptimalPolicy_zero {A : Type u_1} [Fintype A] [Nonempty A] (best : A) : softOptimalPolicy best 0 ⋯ = PMF.uniformOfFintype A

theorem CaoWhiteLassiter2025.softOptimalPolicy_one {A : Type u_1} [Fintype A] [Nonempty A] (best : A) : softOptimalPolicy best 1 ⋯ = PMF.pure best

The ALT measure

ALT (§2.2 of [CWL25]) counts the alternative actions available to the causee, excluding the action actually taken — ALT(Y₁) = 5 at the paper's fig. 2a board state. ALT = 0 is the Frankfurt-style could-not-have-done-otherwise configuration (altCount_eq_zero_iff).

noncomputable def CaoWhiteLassiter2025.altCount {A : Type u_1} (p : PMF A) (taken : A) : ℕ

The number of alternative actions available to the causee: the support of the action distribution, less the action taken.

Equations

• CaoWhiteLassiter2025.altCount p taken = (p.support \ {taken}).ncard

theorem CaoWhiteLassiter2025.altCount_eq_zero_iff {A : Type u_1} [Fintype A] (p : PMF A) (taken : A) : altCount p taken = 0 ↔ ∀ (a : A), a ≠ taken → p a = 0

The INT measure

The paper's §2.3 displayed equation, a simplified [HKW18] degree of intention:

INT(a) = Pr(A = a ∧ G) · u′(a) / Σ_{a′} Pr(A = a′ ∧ G) · u′(a′)

"the probability that an action performed in a state will result in the desired outcome, normalized by the probability of all alternative actions that would have resulted in the same outcome", with each term weighted by exponentiated utility u′ = e^u — the exponential serving only to make the weights strictly positive. Here pr a′ is the joint probability that the agent takes a′ and the goal results, and the weight is abstracted to any w : A → ℝ≥0 (the paper's instantiation is w = e^u); modelIntention below instantiates pr over a SEM. INT is the normalized goal-weighted action distribution evaluated at the taken action (intentionDegree_eq_normalize), and an action without alternatives is trivially intentional (intentionDegree_eq_one_of_altCount_eq_zero) — the alternative-possibilities principle of [Fra69], via [HKW18], behind the paper's made/forced contrast in its example (8).

noncomputable def CaoWhiteLassiter2025.intentionDegree {A : Type u_1} [Fintype A] (pr : A → ENNReal) (w : A → NNReal) (a : A) : ENNReal

The goal-weighted share of action a among all goal-conducive alternatives.

Equations

• CaoWhiteLassiter2025.intentionDegree pr w a = pr a * ↑(w a) / ∑ a' : A, pr a' * ↑(w a')

theorem CaoWhiteLassiter2025.intentionDegree_le_one {A : Type u_1} [Fintype A] (pr : A → ENNReal) (w : A → NNReal) (a : A) : intentionDegree pr w a ≤ 1

theorem CaoWhiteLassiter2025.intentionDegree_eq_normalize {A : Type u_1} [Fintype A] (pr : A → ENNReal) (w : A → NNReal) (a : A) (h0 : ∑' (a' : A), pr a' * ↑(w a') ≠ 0) (htop : ∑' (a' : A), pr a' * ↑(w a') ≠ ⊤) : intentionDegree pr w a = (PMF.normalize (fun (a' : A) => pr a' * ↑(w a')) h0 htop) a

With nonzero finite total mass, INT is mathlib's PMF.normalize of the goal-weighted masses, evaluated at the taken action — the PMF.reweight/PMF.posterior family of Core/Probability/Posterior.

theorem CaoWhiteLassiter2025.intentionDegree_eq_one_of_no_alternatives {A : Type u_1} [Fintype A] (taken : A) (pr : A → ENNReal) (w : A → NNReal) (h : ∀ (a : A), a ≠ taken → pr a = 0) (h0 : pr taken ≠ 0) (hw : w taken ≠ 0) (htop : pr taken ≠ ⊤) : intentionDegree pr w taken = 1

theorem CaoWhiteLassiter2025.intentionDegree_eq_one_of_altCount_eq_zero {A : Type u_1} [Fintype A] (p : PMF A) (taken : A) (pr : A → ENNReal) (w : A → NNReal) (hle : pr ≤ ⇑p) (h : altCount p taken = 0) (h0 : pr taken ≠ 0) (hw : w taken ≠ 0) : intentionDegree pr w taken = 1

noncomputable def CaoWhiteLassiter2025.modelIntention {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Causation.DecidableValuation α] (M : Causation.SEM V α) [M.graph.IsDAG] (ctx : Causation.Valuation α) (act : V) [Fintype (α act)] (goal : Set (Causation.Valuation α)) (w : α act → NNReal) (a : α act) : ENNReal

The paper's INT over a SEM instantiates intentionDegree with pr a′ the probability, under the development of the context, that the action vertex takes value a′ and the goal event holds — the paper's Pr((M,u⃗) ⊨ A = a⃗′ ∧ G = g⃗).

Equations

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

Deterministic limit

In the deterministic limit, SUF collapses to a {0,1} indicator (Causation.SEM.probSufficiency_eq_indicator_of_deterministic). At the vacuous (empty) context this is exactly [NL20]'s causal sufficiency (their definition (23)): with nothing observed, Pearl's counterfactual degenerates to the bare interventional development of cause := true, and "interventional = counterfactual at a vacuous context" is a theorem (probSufficiency_empty_eq_deterministicSuf) rather than a conflation.

noncomputable def CaoWhiteLassiter2025.deterministicSuf {V : Type u_1} [DecidableEq V] (M : Causation.BoolSEM V) [M.graph.IsDAG] [Causation.SEM.IsDeterministic M] (background : Causation.Valuation fun (x : V) => Bool) (cause effect : V) : ENNReal

The {0,1} indicator of categorical causal sufficiency (causallySufficient).

Equations

• CaoWhiteLassiter2025.deterministicSuf M background cause effect = if M.causallySufficient background cause effect then 1 else 0

theorem CaoWhiteLassiter2025.probSufficiency_empty_eq_deterministicSuf {V : Type u_1} [Fintype V] [DecidableEq V] (M : Causation.BoolSEM V) [M.graph.IsDAG] [Causation.SEM.IsDeterministic M] (c e : V) : M.probSufficiency Causation.Valuation.empty c e = deterministicSuf M Causation.Valuation.empty c e

theorem CaoWhiteLassiter2025.probSufficiency_empty_eq_one_of_make {V : Type u_1} [Fintype V] [DecidableEq V] (M : Causation.BoolSEM V) [M.graph.IsDAG] [Causation.SEM.IsDeterministic M] (c e : V) (h : Causative.toSemantics M Causative.make Causation.Valuation.empty c true e true) : M.probSufficiency Causation.Valuation.empty c e = 1

The hub denotation for make entails maximal SUF at the vacuous context — whenever Causative.toSemantics M .make holds (both clauses of [NL20]'s definition (23), over the strict development), Pearl's probability of sufficiency is 1. The converse fails, since the eager development fills undetermined exogenous vertices from their mechanisms; the categorical make semantics is strictly stronger than maximal graded SUF.

The paper's judgment data

The paper's in-text acceptability contrasts are typed rows in Data.Examples.CaoWhiteLassiter2025 (examples (3)–(11)): the non-interchangeability triplets, the gym gradability triplets, the could-have-done-otherwise pair, the intent-denial continuations, and the make/let sufficiency pair. Regression results stay in the module docstring: analysis outputs are not Lean content.

theorem CaoWhiteLassiter2025.make_force_same_semantics_different_judgments {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Causation.DecidableValuation α] [(v : V) → Fintype (α v)] (M : Causation.SEM V α) [M.graph.IsDAG] [M.IsDeterministic] : Causative.toSemantics M Causative.make = Causative.toSemantics M Causative.force ∧ Examples.cwl2025_ex8a.judgment = Features.Judgment.acceptable ∧ Examples.cwl2025_ex8b.judgment = Features.Judgment.questionable

The force-dynamic dispatch of [NL20] gives make and force identical truth conditions, but the paper's minimal pair (8) — same frame, a could-have-done-otherwise continuation — pulls them apart; made tolerates the continuation, forced resists it. The ALT/INT measures register the difference (intentionDegree_eq_one_of_altCount_eq_zero).

A probabilistic example

A 2-vertex SEM whose effect mechanism is a p-weighted coin — genuinely probabilistic, not Dirac. Demonstrates that probSufficiency accepts non-deterministic SEMs (no IsDeterministic constraint).

inductive CaoWhiteLassiter2025.ProbabilisticExample.V : Type

A 2-vertex SEM with root cause and child effect.

• cause : V
• effect : V

@[instance_reducible]

instance CaoWhiteLassiter2025.ProbabilisticExample.instDecidableEqV : DecidableEq V

Equations

• CaoWhiteLassiter2025.ProbabilisticExample.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CaoWhiteLassiter2025.ProbabilisticExample.instFintypeV : Fintype V

Equations

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

@[instance_reducible]

instance CaoWhiteLassiter2025.ProbabilisticExample.instReprV : Repr V

Equations

• CaoWhiteLassiter2025.ProbabilisticExample.instReprV = { reprPrec := CaoWhiteLassiter2025.ProbabilisticExample.instReprV.repr }

def CaoWhiteLassiter2025.ProbabilisticExample.instReprV.repr : V → ℕ → Std.Format

Equations

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

def CaoWhiteLassiter2025.ProbabilisticExample.graph : Causation.CausalGraph V

Equations

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

noncomputable def CaoWhiteLassiter2025.ProbabilisticExample.effectMech (p : NNReal) (h : p ≤ 1) : Causation.Mechanism graph (fun (x : V) => Bool) V.effect

The probabilistic mechanism for effect, ignoring its parent and returning true with probability p — genuinely non-Dirac when p ∉ {0, 1}.

Equations

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

noncomputable def CaoWhiteLassiter2025.ProbabilisticExample.model (p : NNReal) (h : p ≤ 1) : Causation.BoolSEM V

A genuinely probabilistic SEM (not IsDeterministic for p ∉ {0,1}).

Equations

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

def CaoWhiteLassiter2025.ProbabilisticExample.timeIndex : graph.TimeIndex

The 2-vertex graph is time-indexed in the sense of the paper's definition 1, with cause at step 0 and effect at step 1.

Equations

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

instance CaoWhiteLassiter2025.ProbabilisticExample.instIsDAGVGraph : graph.IsDAG

instance CaoWhiteLassiter2025.ProbabilisticExample.instIsDAGVGraphBoolModel (p : NNReal) (h : p ≤ 1) : (model p h).graph.IsDAG