Rescorla-Wagner associative learning

[RW72] [Ell06] [CH95a]

Error-driven associative learning: on each trial every present cue's strength is updated by ΔV_c = α_c · β · (λ − ΣV). The shared prediction-error term makes learning competitive across cues.

Main declarations

• RescorlaWagner, RescorlaWagner.update, RescorlaWagner.iterateConst.
• RescorlaWagner.totalStrength_convergence: total strength converges to λ.
• RescorlaWagner.proportional_partition, RescorlaWagner.overshadowing, RescorlaWagner.blocking, RescorlaWagner.blocked_cue_zero: the salience-proportional equilibrium and the blocking/overshadowing predictions ([Ell06] applies both to second-language acquisition).

The real-valued generalization of the rule is Core.Learning.WidrowHoff.

structure Core.RescorlaWagner (C : Type u_1) : Type u_1

The Rescorla-Wagner learning model ([RW72]): on each trial every present cue has its associative strength updated by

ΔV_c = α_c · β · (λ − ΣV)

where α_c is cue salience, β the learning rate (outcome importance), λ the maximum conditioning supported by the outcome, and ΣV the summed strength of the cues present on the trial. The prediction-error term (λ − ΣV) is what makes learning competitive across cues.

• salience : C → ℝ

  Cue salience: how noticeable each cue is. Must be in [0, 1].

• learnRate : ℝ

  Learning rate (outcome importance). Must be in (0, 1].

• maxCond : ℝ

  Maximum conditioning supported by the outcome.

• salience_nonneg (c : C) : 0 ≤ self.salience c

  Salience is non-negative.

• salience_le_one (c : C) : self.salience c ≤ 1

  Salience is at most 1.

• learnRate_pos : 0 < self.learnRate

  Learning rate is strictly positive.

• learnRate_le_one : self.learnRate ≤ 1

  Learning rate is at most 1.

• maxCond_nonneg : 0 ≤ self.maxCond

  Maximum conditioning is non-negative.

def Core.RescorlaWagner.predictionError {C : Type u_1} (rw : RescorlaWagner C) (present : Finset C) (V : C → ℝ) : ℝ

Prediction error on a trial: λ − ΣV for cues present.

When positive, the outcome is under-predicted (surprise → learning). When zero, the outcome is fully predicted (no learning). When negative, the outcome is over-predicted (extinction).

Equations

• rw.predictionError present V = rw.maxCond - ∑ c ∈ present, V c

def Core.RescorlaWagner.update {C : Type u_1} [DecidableEq C] (rw : RescorlaWagner C) (present : Finset C) (V : C → ℝ) (c : C) : ℝ

One trial of Rescorla-Wagner learning ([RW72]).

For each cue c:

• If c is present: V'(c) = V(c) + α_c · β · (λ − ΣV)
• If c is absent: V'(c) = V(c) (no change)

Equations

• rw.update present V c = if c ∈ present then V c + rw.salience c * rw.learnRate * rw.predictionError present V else V c

theorem Core.RescorlaWagner.update_absent {C : Type u_1} [DecidableEq C] (rw : RescorlaWagner C) (present : Finset C) (V : C → ℝ) (c : C) (hc : c ∉ present) : rw.update present V c = V c

Absent cues are not updated.

theorem Core.RescorlaWagner.blocking {C : Type u_1} [DecidableEq C] (rw : RescorlaWagner C) (present : Finset C) (V : C → ℝ) (B : C) (hB : B ∈ present) (h_total : ∑ c ∈ present, V c = rw.maxCond) : rw.update present V B = V B

Blocking theorem ([RW72]; [Ell06]): when cue A already fully predicts the outcome (V(A) = λ) and is the only cue with nonzero strength among those present, adding a novel cue B to the compound produces zero learning for B: V'(B) = V(B).

theorem Core.RescorlaWagner.no_learning_at_equilibrium {C : Type u_1} [DecidableEq C] (rw : RescorlaWagner C) (present : Finset C) (V : C → ℝ) (h_total : ∑ c ∈ present, V c = rw.maxCond) (c : C) : rw.update present V c = V c

When the outcome is fully predicted, no present cue learns anything.

def Core.RescorlaWagner.iterate {C : Type u_1} [DecidableEq C] (rw : RescorlaWagner C) (trials : List (Finset C)) (V₀ : C → ℝ) : C → ℝ

Iterated R-W learning over a sequence of trials. Each trial specifies which cues are present.

Equations

• rw.iterate trials V₀ = List.foldl (fun (V : C → ℝ) (present : Finset C) (c : C) => rw.update present V c) V₀ trials

def Core.RescorlaWagner.iterateConst {C : Type u_1} [DecidableEq C] (rw : RescorlaWagner C) (S : Finset C) (V₀ : C → ℝ) : ℕ → C → ℝ

Constant-trial iteration: the same cue set is presented on every trial.

Equations

• rw.iterateConst S V₀ 0 = V₀
• rw.iterateConst S V₀ n.succ = fun (c : C) => rw.update S (rw.iterateConst S V₀ n) c

Rescorla-Wagner equilibrium, convergence, and overshadowing

theorem Core.RescorlaWagner.totalStrength_recurrence {C : Type u_1} [DecidableEq C] (rw : RescorlaWagner C) (S : Finset C) (V : C → ℝ) : ∑ c ∈ S, rw.update S V c = ∑ c ∈ S, V c + rw.learnRate * rw.predictionError S V * ∑ c ∈ S, rw.salience c

Total strength recurrence: the summed associative strength across present cues follows an affine recurrence after each trial,

ΣV' = ΣV + β · (Σ_{c∈S} α_c) · (λ − ΣV)
    = (1 − β·A) · ΣV + β·A·λ       where A = Σ_{c∈S} α_c

the same shape as the Luce α-model (cf. LinearLearner.iterate_closed_form) with retention rate 1 − β·A, since the prediction error (λ − ΣV) is shared across all present cues.

theorem Core.RescorlaWagner.totalStrength_convergence {C : Type u_1} [DecidableEq C] (rw : RescorlaWagner C) (S : Finset C) (V₀ : C → ℝ) (h_pos : 0 < rw.learnRate * ∑ c ∈ S, rw.salience c) (h_stable : rw.learnRate * ∑ c ∈ S, rw.salience c < 1) : Filter.Tendsto (fun (n : ℕ) => ∑ c ∈ S, rw.iterateConst S V₀ n c) Filter.atTop (nhds rw.maxCond)

Total strength convergence: under repeated identical trials with the same cue set S, the total associative strength converges to λ.

theorem Core.RescorlaWagner.proportional_partition {C : Type u_1} [DecidableEq C] (rw : RescorlaWagner C) (S : Finset C) (n : ℕ) : ∃ (K : ℝ), ∀ c ∈ S, rw.iterateConst S (fun (x : C) => 0) n c = rw.salience c * K

Proportional partition ([RW72]): when all cues start with zero associative strength and the same cue set is presented on every trial, each cue's strength at every step is proportional to its salience — there exists Kₙ with Vₙ(c) = α_c · Kₙ for every present cue c. At convergence each cue's strength is its salience-share of the outcome maximum λ.

theorem Core.RescorlaWagner.overshadowing {C : Type u_1} [DecidableEq C] (rw : RescorlaWagner C) (S : Finset C) (A B : C) (n : ℕ) (hA : A ∈ S) (hB : B ∈ S) (_hne : A ≠ B) (h_salience : rw.salience B < rw.salience A) (h_pos : 0 < ∑ c ∈ S, rw.iterateConst S (fun (x : C) => 0) n c) : rw.iterateConst S (fun (x : C) => 0) n B < rw.iterateConst S (fun (x : C) => 0) n A

Overshadowing ([RW72]; [Ell06]): when two cues are both present on every trial, the more salient cue captures more associative strength at every step (and hence at equilibrium). Immediate from proportional_partition: Vₙ(c) = α_c · K, so Vₙ(A) = α_A · K > α_B · K = Vₙ(B) whenever K > 0.

theorem Core.RescorlaWagner.blocked_cue_zero {C : Type u_1} [DecidableEq C] (rw : RescorlaWagner C) (S : Finset C) (V : C → ℝ) (C' : C) (hC : C' ∈ S) (hV : V C' = 0) (h_total : ∑ c ∈ S, V c = rw.maxCond) : rw.update S V C' = 0

ΔP–R-W correspondence ([Ell06]; [CH95a]): the blocked direction of a blocking experiment. If one cue already captures all the associative strength and the novel cue starts at zero, the novel cue remains at zero after compound trials — matching ΔP = 0 for the blocked cue.