Documentation

Linglib.Studies.HeitmeierChuangBaayen2026

Heitmeier, Chuang & Baayen (2026): linearity and regularity #

[HCB26]

The relation between morphological regularity and linearity of the form-meaning mapping (§16.6, Table 16.2), for paradigms with imputed additive semantics — word meaning as stem vector plus exponent vector, the book's regularisation of embeddings for "truly regular" systems.

def HeitmeierChuangBaayen2026.IsAnalogicallyRegular {n : } {Stem : Type u_1} {Cell : Type u_2} (f : StemCellProcessing.Lexical.Discriminative.FormVec n) :

A paradigm's form table satisfies proportional analogy if the form contrast between two cells is the same for every stem (cat : cats :: dog : dogs).

Equations
Instances For
    theorem HeitmeierChuangBaayen2026.map_add_sub_map {d n : } {Stem : Type u_1} {Cell : Type u_2} (σ : StemProcessing.Lexical.Discriminative.MeaningVec d) (ε : CellProcessing.Lexical.Discriminative.MeaningVec d) (G : Processing.Lexical.Discriminative.MeaningVec d →ₗ[] Processing.Lexical.Discriminative.FormVec n) (st : Stem) (c : Cell) :
    G (σ st + ε c) - G (σ st) = G (ε c)

    Under additive semantics, the form shift a linear map assigns to an exponent is stem-independent.

    Every linear map's paradigm table over additive semantics is analogically regular.

    theorem HeitmeierChuangBaayen2026.not_exists_linear_of_not_regular {d n : } {Stem : Type u_1} {Cell : Type u_2} (σ : StemProcessing.Lexical.Discriminative.MeaningVec d) (ε : CellProcessing.Lexical.Discriminative.MeaningVec d) {f : StemCellProcessing.Lexical.Discriminative.FormVec n} (hf : ¬IsAnalogicallyRegular f) :
    ¬∃ (G : Processing.Lexical.Discriminative.MeaningVec d →ₗ[] Processing.Lexical.Discriminative.FormVec n), ∀ (st : Stem) (c : Cell), G (σ st + ε c) = f st c

    A table violating proportional analogy has no linear interpolant over additive semantics.

    theorem HeitmeierChuangBaayen2026.exists_linear_iff_isAnalogicallyRegular {d n : } {Stem : Type u_1} {Cell : Type u_2} (σ : StemProcessing.Lexical.Discriminative.MeaningVec d) (ε : CellProcessing.Lexical.Discriminative.MeaningVec d) [Nonempty Stem] [Nonempty Cell] (hind : LinearIndependent (Sum.elim σ ε)) (f : StemCellProcessing.Lexical.Discriminative.FormVec n) :
    (∃ (G : Processing.Lexical.Discriminative.MeaningVec d →ₗ[] Processing.Lexical.Discriminative.FormVec n), ∀ (st : Stem) (c : Cell), G (σ st + ε c) = f st c) IsAnalogicallyRegular f

    When stem and exponent vectors are jointly linearly independent, a paradigm table is linearly realisable iff it is analogically regular — over imputed additive semantics, linearity and regularity are the same constraint.

    theorem HeitmeierChuangBaayen2026.not_isAnalogicallyRegular_of_xor {n : } {f : BoolBoolProcessing.Lexical.Discriminative.FormVec n} (hxor : f true true = f false false f true false = f false true) (hne : f true true f true false) :

    Proportional analogy is the vanishing of second differences — the same equation as the XOR obstruction of linear separability (§16.6's hub-and-neighbour classification example): a table realising XOR on a coordinate, f ⊤ ⊤ = f ⊥ ⊥ ≠ f ⊤ ⊥ = f ⊥ ⊤, violates analogy, so no linear map over additive semantics produces it. Analogy, linear separability, and absence of interaction terms are one constraint.

    The coding interface #

    The stem-exponent setting is the two-primitive case of the DLM coding interface: a paradigm cell's semantic primitives are its stem and cell tags, and conceptualization over Sum.elim σ ε is the imputed additive semantics. The fourth proportional above is conceptualize_analogy at the multiset relation {st, c} + {st', c'} = {st, c'} + {st', c}.

    @[implicit_reducible]
    Equations
    @[simp]
    theorem HeitmeierChuangBaayen2026.primitives_pair {Stem : Type u_1} {Cell : Type u_2} (st : Stem) (c : Cell) :
    Processing.Lexical.Discriminative.primitives (st, c) = {Sum.inl st, Sum.inr c}
    theorem HeitmeierChuangBaayen2026.conceptualize_sumElim {d : } {Stem : Type u_1} {Cell : Type u_2} (σ : StemProcessing.Lexical.Discriminative.MeaningVec d) (ε : CellProcessing.Lexical.Discriminative.MeaningVec d) (st : Stem) (c : Cell) :
    Processing.Lexical.Discriminative.conceptualize (Sum.elim σ ε) (st, c) = σ st + ε c
    noncomputable def HeitmeierChuangBaayen2026.paradigmExperience {d n : } {Stem : Type u_1} {Cell : Type u_2} (σ : StemProcessing.Lexical.Discriminative.MeaningVec d) (ε : CellProcessing.Lexical.Discriminative.MeaningVec d) [Fintype Stem] [Fintype Cell] (f : StemCellProcessing.Lexical.Discriminative.FormVec n) :

    The paradigm as a training experience: imputed additive semantics as the meanings, the form table as the targets.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem HeitmeierChuangBaayen2026.pos_weightedLoss_of_not_regular {d n : } {Stem : Type u_1} {Cell : Type u_2} (σ : StemProcessing.Lexical.Discriminative.MeaningVec d) (ε : CellProcessing.Lexical.Discriminative.MeaningVec d) [Fintype Stem] [Fintype Cell] {f : StemCellProcessing.Lexical.Discriminative.FormVec n} (hf : ¬IsAnalogicallyRegular f) {q : Processing.Lexical.Discriminative.FrequencyVector (Fintype.card (Stem × Cell))} (hq : ∀ (i : Fin (Fintype.card (Stem × Cell))), 0 < q i) (G : Processing.Lexical.Discriminative.MeaningVec d →ₗ[] Processing.Lexical.Discriminative.FormVec n) :

      Irregularity forces positive training loss: no linear map fits a suppletive paradigm exactly, so every ERM solution carries residual error — Table 16.2's irregular-linear cell runs on word-specific semantics, not on additive imputation.