Learning Models

[Luc59] [BM55]

Learning models built on the Luce choice rule (RationalAction): linear (ratio-scale) and probability-space learning, and stochastic gradient ascent. Associative learning rules (Rescorla-Wagner, Widrow-Hoff) live in Core/Learning/.

Main definitions

• LinearLearner, LinearLearner.update, LinearLearner.iterate — the linear (alpha) learning rule on ratio-scale values, vₙ₊₁(a) = α·vₙ(a) + (1-α)·r(a).
• BetaModel, BetaModel.update — probability-space learning, Pₙ₊₁(a) = (1-β)·Pₙ(a) + β·δ(a, chosen).
• sgaUpdate, glaUpdate — stochastic gradient ascent and the Gradual Learning Algorithm ([Boe98]).

Main results

• linear_learning_preserves_axiom1 — the Luce choice rule is preserved under a positive linear update.
• LinearLearner.iterate_closed_form, linear_convergence — the geometric-series solution and convergence of the values to the reinforcement.
• gla_eq_sga, sga_uses_correct_gradient — the GLA is SGA, and SGA follows the MaxEnt log-likelihood gradient.

Implementation notes

Axiom 1 preservation is structural rather than a bridge theorem: LinearLearner.update produces a new RationalAction, and RationalAction.policy is the Luce choice rule, so IIA holds at every trial by construction.

The Luce linear model and Core.RescorlaWagner's total strength obey the same affine recurrence xₙ₊₁ = r·xₙ + (1-r)·c; their closed forms and convergence proofs share one geometric-series argument.

The linear learner (alpha model)

structure Core.LinearLearner (A : Type u_1) : Type u_1

A linear learner for the Luce ratio-scale model ([Luc59]).

The learning rule is a positive linear operator on ratio-scale values: v_{n+1}(a) = α · v_n(a) + (1-α) · r(a) where α ∈ (0,1) is the retention rate and r : A → ℝ is the reinforcement function. The key property is that this is a positive linear transformation — it maps non-negative scores to non-negative scores — which is exactly what Luce's Axiom 1 preservation requires.

• learnRate : ℝ

  Retention rate: weight on prior score. Must be in (0,1).

• reinforcement : A → ℝ

  Reinforcement: the asymptotic target score for each action.

• learnRate_pos : 0 < self.learnRate

  Retention rate is strictly positive.

• learnRate_lt_one : self.learnRate < 1

  Retention rate is strictly less than 1.

• reinforcement_nonneg (a : A) : 0 ≤ self.reinforcement a

  Reinforcement values are non-negative.

def Core.LinearLearner.complementRate {A : Type u_2} (ll : LinearLearner A) : ℝ

The complement 1 - α, which serves as the weight on reinforcement.

Equations

• ll.complementRate = 1 - ll.learnRate

theorem Core.LinearLearner.complementRate_pos {A : Type u_2} (ll : LinearLearner A) : 0 < ll.complementRate

theorem Core.LinearLearner.complementRate_lt_one {A : Type u_2} (ll : LinearLearner A) : ll.complementRate < 1

Linear update and choice-axiom preservation

def Core.LinearLearner.update {S : Type u_1} {A : Type u_2} [Fintype A] (ll : LinearLearner A) (ra : RationalAction S A) : RationalAction S A

One step of linear learning ([Luc59], the Alpha Model): v_{n+1}(s, a) = α · v_n(s, a) + (1 - α) · r(a).

The result is a new RationalAction, so the Luce choice rule (IIA) holds at trial n+1 by construction.

Equations

• ll.update ra = { score := fun (s : S) (a : A) => ll.learnRate * ra.score s a + ll.complementRate * ll.reinforcement a, score_nonneg := ⋯ }

theorem Core.linear_update_nonneg {S : Type u_1} {A : Type u_2} [Fintype A] (ll : LinearLearner A) (ra : RationalAction S A) (s : S) (a : A) : 0 ≤ (ll.update ra).score s a

Updated scores are non-negative — a direct consequence of the positivity of α, (1-α), the original scores, and the reinforcement values. This is what makes the linear learning model a positive linear operator ([Luc59]).

theorem Core.linear_learning_preserves_axiom1 {S : Type u_1} {A : Type u_2} [Fintype A] (ll : LinearLearner A) (ra : RationalAction S A) (s : S) (a : A) : (ll.update ra).policy s a = if (ll.update ra).totalScore s = 0 then 0 else (ll.update ra).score s a / (ll.update ra).totalScore s

Axiom 1 preservation ([Luc59]):

If the Luce choice rule P(a) = v(a)/Σv(b) holds at trial n, then after a positive linear update v' = α·v + (1-α)·r, the updated rule P'(a) = v'(a)/Σv'(b) is again a Luce choice rule. This holds by construction: LinearLearner.update produces a RationalAction, whose policy is the Luce rule.

The beta model

structure Core.BetaModel (A : Type u_3) : Type

The β-model ([Luc59]; [BM55]):

An alternative learning model operating directly on probabilities rather than ratio-scale values: P_{n+1}(a) = (1-β) · P_n(a) + β · δ(a, chosen_n)

where δ(a, chosen_n) = 1 if a was chosen on trial n, 0 otherwise. Unlike the linear model, this operates in probability space, so it does not generally preserve the Luce ratio-scale structure.

• beta : ℝ

  Learning rate in (0,1).

• beta_pos : 0 < self.beta

  β is strictly positive.

• beta_lt_one : self.beta < 1

  β is strictly less than 1.

def Core.BetaModel.update {A : Type u_2} [DecidableEq A] (bm : BetaModel A) (P : A → ℝ) (chosen : A) : A → ℝ

One step of β-model update ([Luc59]): P'(a) = (1-β) · P(a) + β · δ(a, chosen).

Takes a probability function and the chosen action, returns updated probabilities.

Equations

• bm.update P chosen a = (1 - bm.beta) * P a + bm.beta * if a = chosen then 1 else 0

theorem Core.BetaModel.update_nonneg {A : Type u_2} [DecidableEq A] (bm : BetaModel A) (P : A → ℝ) (chosen : A) (hP : ∀ (a : A), 0 ≤ P a) (a : A) : 0 ≤ bm.update P chosen a

β-model update preserves non-negativity of probabilities.

theorem Core.BetaModel.update_sum_one {A : Type u_2} [Fintype A] [DecidableEq A] (bm : BetaModel A) (P : A → ℝ) (chosen : A) (h_chosen : chosen ∈ Finset.univ) (h_sum : ∑ a : A, P a = 1) : ∑ a : A, bm.update P chosen a = 1

β-model update preserves sum-to-one when the input sums to 1.

Iterated linear learning

def Core.LinearLearner.iterate {S : Type u_1} {A : Type u_2} [Fintype A] (ll : LinearLearner A) (ra : RationalAction S A) : ℕ → RationalAction S A

n-step iteration of linear learning ([Luc59]): apply the linear update rule n times starting from an initial RationalAction.

Equations

• ll.iterate ra 0 = ra
• ll.iterate ra n.succ = ll.update (ll.iterate ra n)

theorem Core.LinearLearner.iterate_nonneg {S : Type u_1} {A : Type u_2} [Fintype A] (ll : LinearLearner A) (ra : RationalAction S A) (n : ℕ) (s : S) (a : A) : 0 ≤ (ll.iterate ra n).score s a

After n iterations, scores are still non-negative.

theorem Core.LinearLearner.iterate_closed_form {S : Type u_1} {A : Type u_2} [Fintype A] (ll : LinearLearner A) (ra : RationalAction S A) (n : ℕ) (s : S) (a : A) : (ll.iterate ra n).score s a = ll.learnRate ^ n * ra.score s a + (1 - ll.learnRate ^ n) * ll.reinforcement a

Closed form for iterated linear learning ([Luc59]): after n iterations with retention rate α and reinforcement r, vₙ(s, a) = αⁿ · v₀(s, a) + (1 - αⁿ) · r(a), the geometric-series solution to the linear recurrence.

Asymptotic convergence

theorem Core.linear_convergence {S : Type u_1} {A : Type u_2} [Fintype A] (ll : LinearLearner A) (ra : RationalAction S A) (s : S) (a : A) : Filter.Tendsto (fun (n : ℕ) => (ll.iterate ra n).score s a) Filter.atTop (nhds (ll.reinforcement a))

Convergence of linear learning ([Luc59]): under constant reinforcement, the ratio-scale values converge to the reinforcement values, vₙ(s, a) → r(a) as n → ∞.

Expected choice sequences

structure Core.TrialRecord (A : Type u_3) : Type u_3

A record of a learning trial: what was available, what was chosen, what was the reinforcement. Used for analyzing sequences of choices over trials ([Luc59]).

• chosen : A

  The action chosen on this trial.

• reinforcement : A → ℝ

  The reinforcement received (may differ from the learner's default).

structure Core.ExpectedChoiceSequence (S : Type u_3) (A : Type u_4) [Fintype A] : Type (max u_3 u_4)

An expected choice sequence: the initial agent, a learner, and a history of trials. This structure supports analyzing how choice probabilities evolve over a sequence of reinforced trials ([Luc59]).

• learner : LinearLearner A

  The learning model governing updates.

• initial : RationalAction S A

  The initial rational agent (trial 0).

• history : List (TrialRecord A)

  History of trials (choices and reinforcements).

def Core.ExpectedChoiceSequence.agentAt {S : Type u_1} {A : Type u_2} [Fintype A] (ecs : ExpectedChoiceSequence S A) (n : ℕ) : RationalAction S A

The agent at trial n, after applying n steps of learning.

Equations

• ecs.agentAt n = ecs.learner.iterate ecs.initial n

noncomputable def Core.ExpectedChoiceSequence.choiceProb {S : Type u_1} {A : Type u_2} [Fintype A] (ecs : ExpectedChoiceSequence S A) (n : ℕ) (s : S) (a : A) : ℝ

The probability of choosing action a in state s at trial n.

Equations

• ecs.choiceProb n s a = (ecs.agentAt n).policy s a

theorem Core.ExpectedChoiceSequence.choiceProb_sum_one {S : Type u_1} {A : Type u_2} [Fintype A] (ecs : ExpectedChoiceSequence S A) (n : ℕ) (s : S) (h : (ecs.agentAt n).totalScore s ≠ 0) : ∑ a : A, ecs.choiceProb n s a = 1

Choice probabilities at any trial sum to 1 (when totalScore is nonzero), because each trial's agent is a RationalAction.

Stochastic gradient ascent (log-linear models)

def Core.sgaUpdate (r_j η observed_j expected_j : ℝ) : ℝ

Stochastic Gradient Ascent update for a single weight of a log-linear model.

For MaxEnt phonology, observed_j is the violation count of constraint j on the observed output, and expected_j is the expected violation count under the current model distribution.

The batch gradient is E_emp[c_j] − E_r̄[c_j] (see hasDerivAt_logConditional in RationalAction). The stochastic version replaces both expectations with single-sample estimates.

Equations

• Core.sgaUpdate r_j η observed_j expected_j = r_j + η * (observed_j - expected_j)

def Core.glaUpdate (r_j η : ℝ) (c_j_observed c_j_hypothesis : ℕ) : ℝ

The Gradual Learning Algorithm ([Boe98]) update for a single weight: adjust by the signed difference between the observed violation count and the violation count of a hypothesis sampled from the current grammar.

Equations

• Core.glaUpdate r_j η c_j_observed c_j_hypothesis = r_j + η * (↑c_j_observed - ↑c_j_hypothesis)

theorem Core.gla_eq_sga (r_j η : ℝ) (obs hyp : ℕ) : glaUpdate r_j η obs hyp = sgaUpdate r_j η ↑obs ↑hyp

GLA = SGA: the Gradual Learning Algorithm is Stochastic Gradient Ascent with single-sample estimates of both observed and expected feature values. The update rules are identical by definition.

theorem Core.sga_uses_correct_gradient {ι : Type u_1} [Fintype ι] [Nonempty ι] (s r : ι → ℝ) (y : ι) (wⱼ : ℝ) : HasDerivAt (fun (w : ℝ) => w * s y + r y - logSumExp (w • s + r)) (s y - ∑ i : ι, softmax (wⱼ • s + r) i * s i) wⱼ

SGA converges to the global maximum of a concave objective.

For MaxEnt log-likelihood, the per-weight objective is concave (logConditional_concaveOn in RationalAction), so SGA is guaranteed to converge. This is the key advantage of MaxEnt over Stochastic OT, where convergence of the GLA is not generally proved.