Discriminative Lexicon Model — linear substrate

[BCSBB19] [HCB26] [CBTB26] [LCB26]

The Discriminative Lexicon Model (DLM) is a theory of lexical processing in which form ↔ meaning relations are learned mappings between vector spaces rather than an inventory of stored, decomposed form-meaning entries ([BCSBB19]). At the endstate of learning the model is a pair of linear maps — a comprehension map (the papers' F, with Ŝ = CF) and a production map (G, with Ĉ = SG) — fitted by linear discriminative learning (LDL), the least-squares estimation method of [HCB26].

Main declarations

• LinearDiscriminativeLexicon R F M: a pair of LinearMaps between form and meaning carriers.
• LinearDiscriminativeLexicon.sub_mem_ker_iff: the kernel of the production map is the DLM's neutralization locus.
• FormVec, MeaningVec: Fin n → ℝ carriers for the Studies specialisations.
• broadcast: the coordinate-broadcast linear map, a witness for non-degenerate example DLMs.

Not formalized here: the deep replacements for the linear maps — ResLDL ([CBTB26]: LDL plus a network fitted to its residuals) and DDL ([HSLB25], who find deep mappings do not reliably beat linear ones for Taiwan Mandarin).

The Linear Discriminative Lexicon

structure Processing.Lexical.Discriminative.LinearDiscriminativeLexicon (R : Type u_1) (F : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid F] [AddCommMonoid M] [Module R F] [Module R M] : Type (max u_2 u_3)

The endstate of a Discriminative Lexicon Model with linear mappings: a comprehension map and a production map between form and meaning carriers, fitted by linear discriminative learning ([HCB26]). The two maps are the model's entire "lexicon" — there is no stored inventory.

• comprehension : F →ₗ[R] M

  The form → meaning map — the papers' comprehension matrix F (Ŝ = CF).

• production : M →ₗ[R] F

  The meaning → form map — the papers' production matrix G (Ĉ = SG).

Kernel = neutralization locus

theorem Processing.Lexical.Discriminative.LinearDiscriminativeLexicon.sub_mem_ker_iff {R : Type u_1} {F : Type u_2} {M : Type u_3} [Ring R] [AddCommGroup F] [AddCommGroup M] [Module R F] [Module R M] (D : LinearDiscriminativeLexicon R F M) {e₁ e₂ : M} : e₁ - e₂ ∈ D.production.ker ↔ D.production e₁ = D.production e₂

Two meanings surface as identical forms iff their difference lies in ker production — the DLM's neutralization locus.

ℝ-typed Fin-indexed carriers

@[reducible, inline]

abbrev Processing.Lexical.Discriminative.FormVec (formDim : ℕ) : Type

A formDim-dimensional form vector over ℝ.

Equations

• Processing.Lexical.Discriminative.FormVec formDim = (Fin formDim → ℝ)

@[reducible, inline]

abbrev Processing.Lexical.Discriminative.MeaningVec (meaningDim : ℕ) : Type

A meaningDim-dimensional meaning vector over ℝ.

Equations

• Processing.Lexical.Discriminative.MeaningVec meaningDim = (Fin meaningDim → ℝ)

The broadcast witness

def Processing.Lexical.Discriminative.broadcast {n d : ℕ} (i : Fin d) : MeaningVec d →ₗ[ℝ] FormVec n

The "broadcast coordinate i" linear map e ↦ fun _ => e i.

Equations

• Processing.Lexical.Discriminative.broadcast i = LinearMap.pi fun (x : Fin n) => LinearMap.proj i

@[simp]

theorem Processing.Lexical.Discriminative.broadcast_apply {n d : ℕ} (i : Fin d) (e : MeaningVec d) (j : Fin n) : (broadcast i) e j = e i