Docs / Processing / DiscriminativeLexicon / Training

Training a discriminative lexicon

import Linglib.Processing.DiscriminativeLexicon.Training · namespace DiscriminativeLexicon

Source

The linear discriminative lexicon relates form and meaning by learned matrices rather than by stored, decomposed entries. Words' forms and meanings are row vectors, stacked into a form matrix C and a semantic matrix S; production predicts Ĉ = SG and comprehension Ŝ = CF. Training solves SG = C in the least-squares sense, G minimising the frequency-weighted loss ∑ᵢ qᵢ ‖(SG − C)ᵢ‖², and comprehension is the same regression with the matrices exchanged. Uniform weights give endstate learning and token counts give frequency-informed learning, which is endstate learning on the repeated tokens and equally on the √Q-premultiplied matrices. Endstate learning is orthogonal projection onto the space of predictions, whence the normal equations SᵀQ(SG − C) = 0, existence, and unique predictions; the matrix itself is unique exactly when the experienced meanings span the meaning space. A trained matrix sends the centre of mass of a linearly decodable set of meanings to that of its forms.

Implementation notes

The mappings are the papers' matrices rather than bundled linear maps, and S, C and q are separate arguments, so statements read as the papers' equations; Matrix.vecMulLinear gives the linear map where linear algebra needs one. The papers' weight matrix Q is Matrix.diagonal of q. Linearly decodable is our term, not the papers': a set of usage events is linearly decodable when membership in it is a linear functional of the meanings.

TODO

The deep mappings that replace or augment the linear ones, DDL and ResLDL, are not formalized.

References

The training problem

L77–81
L83–84
L86–98
L100–102
L104–105
L107–109
L111–120

Frequency-informed learning under q is exactly endstate learning on the √Q-premultiplied matrices (Gahl & Baayen 2024 (A4); Heitmeier et al. 2024 §3.4), which needs no invertibility assumption.

theorem isEndstateTrained_diagonal_sqrt_mul_iffL122–128
{ι : Type u_1} {κ : Type u_2} {δ : Type u_3} [Fintype ι] [Fintype κ] [Fintype δ] (S : Matrix ι δ ℝ) (C : Matrix ι κ ℝ) (q : ι → NNReal) (G : Matrix δ κ ℝ) [DecidableEq ι] :
IsEndstateTrained ((Matrix.diagonal fun (i : ι) => √↑(q i)) * S) ((Matrix.diagonal fun (i : ι) => √↑(q i)) * C) G ↔ IsTrained S C q G

Built from ,

L130–136

Frequency-informed learning under token counts is exactly endstate learning on the repeated tokens: one row per word type weighted by its count trains the same mapping as one row per token, the matrices S_f and C_f of Heitmeier et al. 2024 §3.4 (Gahl & Baayen 2024 appendix).

theorem isEndstateTrained_submatrix_fst_iffL138–145
{ι : Type u_1} {κ : Type u_2} {δ : Type u_3} [Fintype ι] [Fintype κ] [Fintype δ] (S : Matrix ι δ ℝ) (C : Matrix ι κ ℝ) (G : Matrix δ κ ℝ) (f : ι → ℕ) :
IsEndstateTrained (S.submatrix Sigma.fst id) (C.submatrix Sigma.fst id) G ↔ IsTrained S C (fun (i : ι) => ↑(f i)) G

Built from ,

Training as orthogonal projection

Through Matrix.vec the tables with rows ι and columns κ form a Euclidean space, whose inner product is the trace form and in which the loss under uniform weights is the squared distance from the observed forms to the predictions. Mapping matrices need no inner product of their own, and frequency-informed learning reduces to this case by isEndstateTrained_diagonal_sqrt_mul_iff.

L155–159

Endstate learning is orthogonal projection: G is trained exactly when its predictions are the projection of the observed forms onto the space of all predictions.

theorem isEndstateTrained_iff_predicted_eq_starProjectionL181–190
{ι : Type u_1} {κ : Type u_2} {δ : Type u_3} [Fintype ι] [Fintype κ] [Fintype δ] (S : Matrix ι δ ℝ) (C : Matrix ι κ ℝ) (G : Matrix δ κ ℝ) :
IsEndstateTrained S C G ↔ (predicted κ S) G = (predicted κ S).range.starProjection (WithLp.toLp 2 C.vec)

Built from ,

theorem exists_isTrainedL197–200
{ι : Type u_1} {κ : Type u_2} {δ : Type u_3} [Fintype ι] [Fintype κ] [Fintype δ] (S : Matrix ι δ ℝ) (C : Matrix ι κ ℝ) (q : ι → NNReal) :
∃ (G : Matrix δ κ ℝ), IsTrained S C q G

Built from

The normal equations

G is trained iff it satisfies the normal equations SᵀQ(SG − C) = 0 (Gahl & Baayen 2024 (A2), (A4)).

theorem isTrained_iffL217–229
{ι : Type u_1} {κ : Type u_2} {δ : Type u_3} [Fintype ι] [Fintype κ] [Fintype δ] (S : Matrix ι δ ℝ) (C : Matrix ι κ ℝ) (q : ι → NNReal) (G : Matrix δ κ ℝ) [DecidableEq ι] :
IsTrained S C q G ↔ (S.transpose * Matrix.diagonal fun (i : ι) => ↑(q i)) * (S * G - C) = 0

Built from

L231–238
L242–252
L254–259

Predictions

All trained matrices under positive weights produce the same predicted forms SG on the training events, so predictions are unique even when G is not.

theorem IsTrained.mul_eqL269–279
{ι : Type u_1} {κ : Type u_2} {δ : Type u_3} [Fintype ι] [Fintype κ] [Fintype δ] {S : Matrix ι δ ℝ} {C : Matrix ι κ ℝ} {q : ι → NNReal} {G : Matrix δ κ ℝ} (hq : ∀ (i : ι), 0 < q i) {G' : Matrix δ κ ℝ} (hG : IsTrained S C q G) (hG' : IsTrained S C q G') :
S * G = S * G'

Built from

L281–292
L294–298
L300–316

The trained matrix is uniquely determined exactly when the experienced meanings span the meaning space, the coordinate-free form of S having full column rank. The papers assume this silently in writing the closed form (SᵀS)⁻¹SᵀC.

theorem existsUnique_isTrained_iffL318–330
{ι : Type u_1} {κ : Type u_2} {δ : Type u_3} [Fintype ι] [Fintype κ] [Fintype δ] {S : Matrix ι δ ℝ} {C : Matrix ι κ ℝ} {q : ι → NNReal} [Nonempty κ] (hq : ∀ (i : ι), 0 < q i) :
(∃! G : Matrix δ κ ℝ, IsTrained S C q G) ↔ Submodule.span ℝ (Set.range S.row) = ⊤

Built from

L332–343

Centres of mass

Whenever membership in a set P of usage events is a linear functional of the meanings, a mapping matrix trained under q sends the q-weighted centre of mass of P's meanings to the q-weighted centre of mass of P's observed forms.

theorem IsTrained.centerMass_vecMul_eq_of_decodableL347–356
{ι : Type u_1} {κ : Type u_2} {δ : Type u_3} [Fintype ι] [Fintype κ] [Fintype δ] {S : Matrix ι δ ℝ} {C : Matrix ι κ ℝ} {q : ι → NNReal} {G : Matrix δ κ ℝ} [DecidableEq ι] (hG : IsTrained S C q G) {P : Finset ι} {w : (δ → ℝ) →ₗ[ℝ] ℝ} (hw : ∀ (i : ι), w (S i) = if i ∈ P then 1 else 0) :
Matrix.vecMul (P.centerMass (fun (i : ι) => ↑(q i)) S.row) G = P.centerMass (fun (i : ι) => ↑(q i)) C.row

Built from

L358–365