Gahl and Baayen (2024): Time and Thyme Again

Gahl had found that the more frequent of two homophones, such as time against thyme, tends to be shorter in speech. Gahl and Baayen recast this with a discriminative lexicon, linear maps between semantic vectors and triphone vectors with no stored words, so frequency cannot be a property of a word. It splits instead into practice, frequency-informed learning of the production map, and contextual independence, the share of a word's predictability in an utterance that it owes to itself. The duration models are not formalized; the paper's two worked examples are.

Main statements

• semanticSupportForForm_endstate_time_lt_thyme, semanticSupportForFormFIL_thyme_lt_time: practice reverses which homophone's form its meaning supports more.
• time_sub_thyme_notMem_ker: the homophones time and thyme get distinct predicted forms.
• not_existsUnique_isELTrained: regression does not determine the word-to-word map.
• diag_W_mem_Icc: the self-prediction shares of the toy words lie in [0, 1].

Implementation notes

• The paper fits only production, so both toy lexicons have the zero comprehension map.
• The paper estimates the corpus-scale word-to-word map with the Rescorla–Wagner rule, which is not formalized; W is the pseudoinverse solution it uses for the toy corpus.

References

• [GB24]
• [Gah08]
• [BCSBB19]
• [HCAB24]

The toy lexicon

inductive GahlBaayen2024.Phone : Type

The toy lexicon uses five phones, with i standing for the paper's ɪ and the diphthong written as the two phones a ɪ.

• t : Phone
• l : Phone
• a : Phone
• i : Phone
• m : Phone

@[instance_reducible]

instance GahlBaayen2024.instDecidableEqPhone : DecidableEq Phone

Equations

• GahlBaayen2024.instDecidableEqPhone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def GahlBaayen2024.word : Fin 3 → List Phone

The toy words time, lime and thyme are spelled as phone strings, the two homophones sharing a string.

Equations

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

def GahlBaayen2024.triphone : Fin 6 → Augmented Phone

The six triphones of (2) are listed in the paper's column order #ta taɪ aɪm ɪm# #la laɪ.

Equations

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

def GahlBaayen2024.toyForms (i : Fin 3) : DiscriminativeLexicon.FormVec 6

Each row of the form matrix C of (2) is the word's triphone indicator, the DLM's cue coding at width 3.

Equations

• GahlBaayen2024.toyForms i = DiscriminativeLexicon.cueVector 3 GahlBaayen2024.triphone (GahlBaayen2024.word i)

theorem GahlBaayen2024.toyForms_eq : toyForms = ![![1, 1, 1, 1, 0, 0], ![0, 0, 1, 1, 1, 1], ![1, 1, 1, 1, 0, 0]]

The DLM's cue coding reproduces the form matrix (2).

def GahlBaayen2024.semanticVectors : Matrix (Fin 3) (Fin 2) ℚ

The semantic vectors of (1) give time, lime and thyme two arbitrary dimensions.

Equations

• GahlBaayen2024.semanticVectors = !![1 / 10, 3 / 10; 6 / 10, 2 / 10; 11 / 10, 6 / 10]

noncomputable def GahlBaayen2024.toy : DiscriminativeLexicon.TrainingExperience 3 6 2

The toy lexicon pairs the semantic matrix S of (1) with the triphone matrix C of (2).

Equations

• GahlBaayen2024.toy = { S := GahlBaayen2024.semanticVectors.map ⇑(Rat.castHom ℝ), C := Matrix.of GahlBaayen2024.toyForms }

@[reducible, inline]

abbrev GahlBaayen2024.time : Fin 3

time is the first row of the toy lexicon.

Equations

• GahlBaayen2024.time = 0

@[reducible, inline]

abbrev GahlBaayen2024.lime : Fin 3

lime is the second row of the toy lexicon.

Equations

• GahlBaayen2024.lime = 1

@[reducible, inline]

abbrev GahlBaayen2024.thyme : Fin 3

thyme is the third row of the toy lexicon.

Equations

• GahlBaayen2024.thyme = 2

def GahlBaayen2024.freq : DiscriminativeLexicon.FrequencyVector 3

time, lime and thyme have token frequencies 100, 10 and 1 (A3).

Equations

• GahlBaayen2024.freq = ![100, 10, 1]

The arithmetic of the toy lexicon is decided over ℚ and cast into ℝ.

Endstate and frequency-informed learning

The paper fits only the production side of the model. Mapping matrices act on row vectors, ĉ = sG, so a production map is toLin' Gᵀ.

noncomputable def GahlBaayen2024.endstateG : Matrix (Fin 2) (Fin 6) ℝ

The endstate mapping G of (4) is the closed form (SᵀS)⁻¹SᵀC of (A2).

Equations

• GahlBaayen2024.endstateG = (GahlBaayen2024.toy.S.transpose * GahlBaayen2024.toy.S)⁻¹ * (GahlBaayen2024.toy.S.transpose * GahlBaayen2024.toy.C)

noncomputable def GahlBaayen2024.endstate : DiscriminativeLexicon.Linear ℝ (DiscriminativeLexicon.FormVec 6) (DiscriminativeLexicon.MeaningVec 2)

The lexicon at the endstate of learning has the endstate mapping as its production map.

Equations

• GahlBaayen2024.endstate = { comprehension := 0, production := Matrix.toLin' GahlBaayen2024.endstateG.transpose }

noncomputable def GahlBaayen2024.frequencyInformedG : Matrix (Fin 2) (Fin 6) ℝ

The frequency-informed mapping is the closed form (SᵀQS)⁻¹SᵀQC of the normal equations of (A4) at the frequencies freq.

Equations

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

noncomputable def GahlBaayen2024.frequencyInformed : DiscriminativeLexicon.Linear ℝ (DiscriminativeLexicon.FormVec 6) (DiscriminativeLexicon.MeaningVec 2)

The lexicon after frequency-informed learning has the frequency-informed mapping as its production map.

Equations

• GahlBaayen2024.frequencyInformed = { comprehension := 0, production := Matrix.toLin' GahlBaayen2024.frequencyInformedG.transpose }

theorem GahlBaayen2024.endstate_isELTrainedOn : DiscriminativeLexicon.Linear.IsELTrainedOn toy endstate

theorem GahlBaayen2024.frequencyInformed_isTrainedOn : DiscriminativeLexicon.Linear.IsTrainedOn toy freq frequencyInformed

Semantic support for form

def GahlBaayen2024.supportMatrix {m n d : ℕ} (D : DiscriminativeLexicon.Linear ℝ (DiscriminativeLexicon.FormVec n) (DiscriminativeLexicon.MeaningVec d)) (data : DiscriminativeLexicon.TrainingExperience m n d) : Matrix (Fin m) (Fin m) ℝ

The support matrix T = ĈCᵀ of (A5), with Ĉ = SG, tabulates the support each word's form (column) receives from each word's meaning (row).

Equations

• GahlBaayen2024.supportMatrix D data = data.S * D.productionMatrix * data.C.transpose

theorem GahlBaayen2024.supportMatrix_apply {m n d : ℕ} (D : DiscriminativeLexicon.Linear ℝ (DiscriminativeLexicon.FormVec n) (DiscriminativeLexicon.MeaningVec d)) (data : DiscriminativeLexicon.TrainingExperience m n d) (i k : Fin m) : supportMatrix D data i k = (D.semanticSupport (data.S i)) (data.C k)

def GahlBaayen2024.semanticSupportForForm {m n d : ℕ} (D : DiscriminativeLexicon.Linear ℝ (DiscriminativeLexicon.FormVec n) (DiscriminativeLexicon.MeaningVec d)) (data : DiscriminativeLexicon.TrainingExperience m n d) : Fin m → ℝ

Semantic support for form is the diagonal of T, the support a word's form receives from its own meaning.

Equations

• GahlBaayen2024.semanticSupportForForm D data = (GahlBaayen2024.supportMatrix D data).diag

theorem GahlBaayen2024.semanticSupportForForm_endstate_time_lt_thyme : semanticSupportForForm endstate toy time < semanticSupportForForm endstate toy thyme

At the endstate thyme's meaning supports its form more than time's does, 4.623 against 3.455 (Table 1).

noncomputable def GahlBaayen2024.semanticSupportForFormFIL (i : Fin 3) : ℝ

Under frequency-informed learning the paper reads support for form off the fitted values √Q S G of the √Q-scaled regression, paired with the words' own triphone vectors (A7).

Equations

• GahlBaayen2024.semanticSupportForFormFIL i = (GahlBaayen2024.frequencyInformed.semanticSupport ((GahlBaayen2024.toy.sqrtScale GahlBaayen2024.freq).S i)) (GahlBaayen2024.toy.C i)

theorem GahlBaayen2024.semanticSupportForFormFIL_eq_sqrt_mul (i : Fin 3) : semanticSupportForFormFIL i = √↑(freq i) * semanticSupportForForm frequencyInformed toy i

theorem GahlBaayen2024.semanticSupportForFormFIL_thyme_lt_time : semanticSupportForFormFIL thyme < semanticSupportForFormFIL time

Under practice time overtakes thyme, 39.805 against 6.225 (Table 1), reversing the endstate order.

theorem GahlBaayen2024.time_sub_thyme_notMem_ker : toy.S time - toy.S thyme ∉ endstate.production.ker

time and thyme share a form row, but their meaning difference lies outside the kernel of the production map, so identical triphones receive distinct predicted forms (appendix A3, Fig. A2).

Contextual independence

A word-to-word map W with UW = U predicts every word of an utterance from all the words in it, and the diagonal of W is the share of that prediction a word owes to itself.

inductive GahlBaayen2024.Word : Type

The toy corpus has nine words.

• my : Word
• time : Word
• is : Word
• short : Word
• good : Word
• fragrant : Word
• thyme : Word
• lime : Word
• bad : Word

@[instance_reducible]

instance GahlBaayen2024.instDecidableEqWord : DecidableEq Word

Equations

• GahlBaayen2024.instDecidableEqWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def GahlBaayen2024.utterance : Fin 5 → List Word

The five toy utterances of (5).

Equations

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

def GahlBaayen2024.vocabulary : Fin 9 → Word

The columns of U and W list the words in the paper's order.

Equations

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

def GahlBaayen2024.U : Matrix (Fin 5) (Fin 9) ℝ

The utterance-by-word matrix U multiple-hot encodes each utterance over the vocabulary.

Equations

• GahlBaayen2024.U = Matrix.of fun (i : Fin 5) => DiscriminativeLexicon.multiHot GahlBaayen2024.vocabulary fun (x : GahlBaayen2024.Word) => x ∈ GahlBaayen2024.utterance i

The arithmetic of the toy corpus is decided over ℤ and cast into ℝ.

noncomputable def GahlBaayen2024.W : Matrix (Fin 9) (Fin 9) ℝ

The word-to-word map W of (6) is U⁺U = Uᵀ(UUᵀ)⁻¹U, the pseudoinverse solution of UW = U (A8).

Equations

• GahlBaayen2024.W = GahlBaayen2024.U.transpose * (GahlBaayen2024.U * GahlBaayen2024.U.transpose)⁻¹ * GahlBaayen2024.U

theorem GahlBaayen2024.U_mul_W : U * W = U

W solves UW = U, so each word's prediction strength in an utterance containing it is 1 ((7), (8)).

theorem GahlBaayen2024.isStarProjection_W : IsStarProjection W

W is symmetric and idempotent, the orthogonal projection onto the row space of U.

theorem GahlBaayen2024.not_existsUnique_isELTrained : ¬∃! G : Matrix (Fin 9) (Fin 9) ℝ, DiscriminativeLexicon.IsELTrained { S := U, C := U } G

Regressing the words of each utterance on themselves, as the paper does for the toy corpus, does not determine W, since the identity, the "ideal solution" of (A9), is trained as well.

theorem GahlBaayen2024.le_diag_W (i j : Fin 9) : W j i ≤ W i i

The diagonal entry of each column of W is its largest, as the paper observes of (6).

theorem GahlBaayen2024.diag_W_mem_Icc (i : Fin 9) : W i i ∈ Set.Icc 0 1

The diagonal of W lies in [0, 1], the "proportions" of §3.2, because W is an orthogonal projection.

noncomputable def GahlBaayen2024.cind (d : ℝ) : ℝ

The contextual-independence measure of (9) is Cind = (log(1/d))^{1/4}, a log against the right skew of the diagonal values and a power to finish it.

Equations

• GahlBaayen2024.cind d = Real.log (1 / d) ^ (1 / 4)

theorem GahlBaayen2024.strictAntiOn_cind : StrictAntiOn cind (Set.Ioo 0 1)

Cind reverses the order of the diagonal values on (0, 1), so the more a word predicts itself the lower its Cind, which is the sign of its correlation with frequency in Fig. 2.