Heitmeier, Chuang and Baayen (2026): The Discriminative Lexicon

This file formalizes the book's relation between linearity and regularity. Its linear production maps handle inflectional systems with irregular forms: trained on empirical embeddings, the English past-tense model produces 94% of the regular and 74% of the irregular training verbs (§12.9). Meanings can instead be constructed, the meaning of walked as the meaning of walk plus a past-tense vector (Table 12.7; conceptualization is vector addition, (5.3)). Regularizing meanings this way gives "a reasonable approximation of a truly regular system, and for such a system, linear mappings appear to work quite well" (§16.6, Table 16.2), but when held-out verbs' meanings are built from the comprehended base form plus a past-tense vector, "none of the irregular verbs was produced correctly" (§12.9).

The file states why in word-and-paradigm terms. Over imputed semantics, a lexeme vector plus an inflectional-function vector, the form table of a linear map satisfies proportional analogy by construction (Morphology.IsAnalogicallyRegular). So a table violating analogy is the paradigm of no linear lexicon and forces positive training loss, and when the lexeme and function vectors are jointly independent a table is the paradigm of some linear lexicon exactly when it is analogically regular. Over word-specific embeddings, by contrast, any table is the paradigm of some linear lexicon as soon as the embeddings are linearly independent, which fills the irregular-linear cell of Table 16.2. The English past tense at the book's letter-trigram coding (§12.9) is the irregular table, walk, walked against go, went, with the forms taken from the English fragment.

The file also relates the book's three ways of estimating a mapping. Incremental learning updates the mapping at each usage event by the Widrow–Hoff rule, and the mappings of endstate and frequency-informed learning are the matrices at which those updates cancel (§1.3, §6.2).

Main results

• not_exists_paradigm_eq_of_not_regular, pos_weightedLoss_of_not_regular: an irregular table is the paradigm of no linear lexicon over imputed semantics, and training on it leaves positive loss.
• exists_paradigm_imputed_eq_iff: over jointly independent lexeme and function vectors, a table is the paradigm of some linear lexicon iff it is analogically regular.
• exists_paradigm_eq_of_linearIndependent: over linearly independent word-specific embeddings, every table is the paradigm of some linear lexicon.
• pastTense_not_regular: walk, walked, go, went violates proportional analogy.
• isTrained_iff_sum_update_sub_eq_zero: a mapping matrix is trained iff the frequency-weighted Widrow–Hoff updates of the usage events cancel at it.

Implementation notes

• The book describes endstate learning as the state incremental learning reaches after infinitely many epochs. At a fixed learning rate the updates cancel only in their frequency-weighted sum, and single events leave a matrix fixed only when it fits the experience exactly (mul_eq_iff_forall_update_eq_self).

References

• [HCB26]

Imputed semantics

theorem HeitmeierChuangBaayen2026.not_exists_paradigm_eq_of_not_regular {d n : ℕ} {Lexeme : Type u_1} {Cell : Type u_2} (σ : Lexeme → DiscriminativeLexicon.MeaningVec d) (ε : Cell → DiscriminativeLexicon.MeaningVec d) {f : Lexeme → Cell → DiscriminativeLexicon.FormVec n} (hf : ¬Morphology.IsAnalogicallyRegular f) : ¬∃ (D : DiscriminativeLexicon.Linear ℝ (DiscriminativeLexicon.FormVec n) (DiscriminativeLexicon.MeaningVec d)), D.paradigm (DiscriminativeLexicon.imputed σ ε) = f

A table violating proportional analogy is the paradigm of no linear lexicon over imputed semantics, so irregular forms cannot be produced from constructed meanings (§12.9).

Interpolation

theorem HeitmeierChuangBaayen2026.exists_paradigm_eq_of_linearIndependent {d n : ℕ} {Lexeme : Type u_1} {Cell : Type u_2} {s : Lexeme → Cell → DiscriminativeLexicon.MeaningVec d} (hs : LinearIndependent ℝ (Function.uncurry s)) (f : Lexeme → Cell → DiscriminativeLexicon.FormVec n) : ∃ (D : DiscriminativeLexicon.Linear ℝ (DiscriminativeLexicon.FormVec n) (DiscriminativeLexicon.MeaningVec d)), D.paradigm s = f

Over word-specific, linearly independent embeddings any form table is the paradigm of some linear lexicon, irregulars included, which is the irregular-linear cell of Table 16.2 and the English past tense on empirical embeddings (§12.9).

theorem HeitmeierChuangBaayen2026.exists_paradigm_imputed_eq_iff {d n : ℕ} {Lexeme : Type u_1} {Cell : Type u_2} (σ : Lexeme → DiscriminativeLexicon.MeaningVec d) (ε : Cell → DiscriminativeLexicon.MeaningVec d) [Nonempty Lexeme] [Nonempty Cell] (hind : LinearIndependent ℝ (Sum.elim σ ε)) (f : Lexeme → Cell → DiscriminativeLexicon.FormVec n) : (∃ (D : DiscriminativeLexicon.Linear ℝ (DiscriminativeLexicon.FormVec n) (DiscriminativeLexicon.MeaningVec d)), D.paradigm (DiscriminativeLexicon.imputed σ ε) = f) ↔ Morphology.IsAnalogicallyRegular f

When the lexeme and inflectional-function vectors are jointly linearly independent, a table is the paradigm of some linear lexicon over imputed semantics iff it is analogically regular, so for a regularized system linearity and regularity are the same constraint (§16.6).

Training on a paradigm

noncomputable def HeitmeierChuangBaayen2026.paradigmExperience {d n : ℕ} {Lexeme : Type u_1} {Cell : Type u_2} (σ : Lexeme → DiscriminativeLexicon.MeaningVec d) (ε : Cell → DiscriminativeLexicon.MeaningVec d) [Fintype Lexeme] [Fintype Cell] (f : Lexeme → Cell → DiscriminativeLexicon.FormVec n) : DiscriminativeLexicon.TrainingExperience (Fintype.card (Lexeme × Cell)) n d

A paradigm is a training experience whose semantic matrix holds the imputed meanings and whose form matrix holds the form table, one row per lexeme and cell.

Equations

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

theorem HeitmeierChuangBaayen2026.pos_weightedLoss_of_not_regular {d n : ℕ} {Lexeme : Type u_1} {Cell : Type u_2} (σ : Lexeme → DiscriminativeLexicon.MeaningVec d) (ε : Cell → DiscriminativeLexicon.MeaningVec d) [Fintype Lexeme] [Fintype Cell] {f : Lexeme → Cell → DiscriminativeLexicon.FormVec n} (hf : ¬Morphology.IsAnalogicallyRegular f) {q : DiscriminativeLexicon.FrequencyVector (Fintype.card (Lexeme × Cell))} (hq : ∀ (i : Fin (Fintype.card (Lexeme × Cell))), 0 < q i) (G : Matrix (Fin d) (Fin n) ℝ) : 0 < DiscriminativeLexicon.weightedLoss (paradigmExperience σ ε f) q G

Irregularity forces positive training loss, since no mapping matrix fits a suppletive paradigm exactly and so every trained matrix carries residual error.

Incremental learning

Incremental learning updates a mapping one usage event at a time by the Widrow–Hoff rule. The mapping matrices of endstate and frequency-informed learning are its equilibria.

theorem HeitmeierChuangBaayen2026.update_example : ErrorDrivenLearning.update (1e-2 • 1) 1 ![0, 1] ![0.5, 0.5] !![1.2, -0.3; 0.4, 0.45] = !![1.2, -0.3; 0.401, 0.4505]

The worked Widrow–Hoff step of the book's background box on the rule (§6.2). The book prints 0.4001 for the entry that the rule makes 0.401.

theorem HeitmeierChuangBaayen2026.sub_vecMul_update_smul_one {d n : ℕ} (G : Matrix (Fin d) (Fin n) ℝ) {η : ℝ} (x : DiscriminativeLexicon.MeaningVec d) (y : DiscriminativeLexicon.FormVec n) : y - Matrix.vecMul x (ErrorDrivenLearning.update (η • 1) 1 x y G) = (1 - η * x ⬝ᵥ x) • (y - Matrix.vecMul x G)

One step scales the prediction error for its own input by 1 - η * x ⬝ᵥ x.

theorem HeitmeierChuangBaayen2026.abs_sub_vecMul_update_lt_iff {d n : ℕ} (G : Matrix (Fin d) (Fin n) ℝ) {η : ℝ} {x : DiscriminativeLexicon.MeaningVec d} {y : DiscriminativeLexicon.FormVec n} {j : Fin n} (hj : y j ≠ Matrix.vecMul x G j) : |y j - Matrix.vecMul x (ErrorDrivenLearning.update (η • 1) 1 x y G) j| < |y j - Matrix.vecMul x G j| ↔ |1 - η * x ⬝ᵥ x| < 1

"The next predicted outcome from the same input vector is closer to the target than the previous one" (§6.2) exactly when η * x ⬝ᵥ x lies strictly between 0 and 2.

theorem HeitmeierChuangBaayen2026.tendsto_vecMul_iterate_update_smul_one {d n : ℕ} (G : Matrix (Fin d) (Fin n) ℝ) {η : ℝ} {x : DiscriminativeLexicon.MeaningVec d} (y : DiscriminativeLexicon.FormVec n) (h : |1 - η * x ⬝ᵥ x| < 1) : Filter.Tendsto (fun (k : ℕ) => Matrix.vecMul x ((ErrorDrivenLearning.update (η • 1) 1 x y)^[k] G)) Filter.atTop (nhds y)

For such a learning rate, "by redoing this step again and again, the error [...] will get smaller and smaller" (§6.2), and the prediction converges to the target.

theorem HeitmeierChuangBaayen2026.isTrained_iff_sum_update_sub_eq_zero {d n m : ℕ} (data : DiscriminativeLexicon.TrainingExperience m n d) (q : DiscriminativeLexicon.FrequencyVector m) (G : Matrix (Fin d) (Fin n) ℝ) {η : ℝ} (hη : η ≠ 0) : DiscriminativeLexicon.IsTrained data q G ↔ ∑ i : Fin m, ↑(q i) • (ErrorDrivenLearning.update (η • 1) 1 (data.S i) (data.C i) G - G) = 0

A mapping matrix is trained exactly when the frequency-weighted changes that the usage events would each make to it cancel. Endstate learning, the case of uniform weights, is in this sense the "equilibrium state of network weights" of incremental learning (§1.3).

theorem HeitmeierChuangBaayen2026.mul_eq_iff_forall_update_eq_self {d n m : ℕ} (data : DiscriminativeLexicon.TrainingExperience m n d) (G : Matrix (Fin d) (Fin n) ℝ) {η : ℝ} (hη : η ≠ 0) (hS : ∀ (i : Fin m), data.S i ≠ 0) : data.S * G = data.C ↔ ∀ (i : Fin m), ErrorDrivenLearning.update (η • 1) 1 (data.S i) (data.C i) G = G

A mapping matrix fits the experience exactly iff no usage event changes it.

The English past tense

def HeitmeierChuangBaayen2026.verb : Fin 2 → English.Verbs.Verb

The two verbs of the book's contrast, regular walk and suppletive go, are the English fragment's entries.

Equations

• HeitmeierChuangBaayen2026.verb = ![English.Verbs.walk, English.Verbs.go]

@[reducible, inline]

abbrev HeitmeierChuangBaayen2026.walk : Fin 2

walk is the first verb.

Equations

• HeitmeierChuangBaayen2026.walk = 0

@[reducible, inline]

abbrev HeitmeierChuangBaayen2026.go : Fin 2

go is the second verb.

Equations

• HeitmeierChuangBaayen2026.go = 1

def HeitmeierChuangBaayen2026.cell : Fin 2 → English.Verbs.Verb.Cell

The base and past cells of the fragment's verb paradigm are the two cells of the table.

Equations

• HeitmeierChuangBaayen2026.cell = ![English.Verbs.Verb.Cell.base, English.Verbs.Verb.Cell.past]

@[reducible, inline]

abbrev HeitmeierChuangBaayen2026.base : Fin 2

The base cell is the first cell.

Equations

• HeitmeierChuangBaayen2026.base = 0

@[reducible, inline]

abbrev HeitmeierChuangBaayen2026.past : Fin 2

The past cell is the second cell.

Equations

• HeitmeierChuangBaayen2026.past = 1

def HeitmeierChuangBaayen2026.trigram : Fin 13 → Augmented Char

The letter-trigram cue inventory of the four forms; §12.9 codes forms as letter trigrams.

Equations

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

def HeitmeierChuangBaayen2026.pastTense (v c : Fin 2) : DiscriminativeLexicon.FormVec 13

The past-tense form table at the trigram coding takes each verb's form at each cell from the fragment.

Equations

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

theorem HeitmeierChuangBaayen2026.pastTense_not_regular : ¬Morphology.IsAnalogicallyRegular pastTense

The English past tense violates proportional analogy, since walked adds the cue ed# to walk while went adds nothing to go. So no linear lexicon produces it from constructed meanings (not_exists_paradigm_eq_of_not_regular), while independent embeddings realise it (exists_paradigm_eq_of_linearIndependent), as in §12.9.