Bybee (1985): relevance and the dynamic lexicon

[Byb85] (Morphology: A Study of the Relation Between Meaning and Form, Typological Studies in Language 9) tests the relevance hypothesis on a 50-language stratified probability sample ([Per80]): a morpheme category whose meaning is more relevant to the verb stem (a) occurs more often as inflection cross-linguistically, (b) sits closer to the stem in suffixal morphology, and (c) fuses more tightly with it.

This file formalizes the data behind claims (a) and (b) — the Ch 2 §5 frequency surveys and the Ch 2 §6 morpheme-order counts — and grounds the substrate's relevance order (MorphCategory.peripherality, via RelevanceLT / RelevanceLE) in that evidence. Claim (c), fusion, is qualitative in the source and is not formalized. The second half formalizes Ch 5's dynamic network model of the lexicon: lexical strength, lexical connection, and the strong-verb frequency table.

Main definitions

• BybeeCategory — the verbal-inflectional categories of Ch 2, in relevance order.
• inflectionalCount50, derivOrInflCount50 — the Ch 2 §5 frequency surveys (Figs 1+2).
• orderPairs — the Ch 2 §6 morpheme-order counts, one OrderPair per tested category pair.
• toMorphCategory — the embedding of BybeeCategory into the substrate MorphCategory.
• SurveyedCloser — the stem-proximity order derived from orderPairs.
• LexicalEntry, Network — the Ch 5 dynamic network: entries with token frequency (lexical strength) and typed connections (lexical connection).
• Network.HasMorphologicalRelation — the Ch 5 §5 derived relation: parallel semantic and phonological connections.
• strongStillStrong, strongRegularized — the Ch 5 §6 strong-verb frequency table.

Main results

• valence_highest_when_derivOrInfl, valence_lowest_when_inflectional — the relevance and generality frequency predictions.
• predicted_outnumbers_counter, aspect_categorical_against_tense_and_mood — the order predictions.
• survey_order_iso_relevance — on the surveyed categories SurveyedCloser and the substrate RelevanceLT coincide via toMorphCategory: the hierarchy is the order the §6 survey forces, not a stipulated table.
• bybeeSurveyedOrder_respects_hierarchy — closes the loop to RespectsRelevanceHierarchy.
• strong_verbs_higher_frequency_than_regularized — the Ch 5 §6 diachronic claim: still-Strong verbs have a strictly higher mean token frequency than the regularized ones.

Implementation notes

Out of scope: Ch 1 fusion/allomorphy, Ch 3 paradigm organization, Ch 4's lexical-derivational-inflectional continuum (which no discrete status enum expresses — flagged for future work), and Part II tense/aspect/mood detail (Ch 6-9). MorphCategory.RelevanceLT is exercised independently by Studies/HahnDegenFutrell2021Morphology.lean; the BybeeCategory enum and toMorphCategory bridge feed Studies/RathiHahnFutrell2026.lean. Not yet covered from Ch 5: the frequency-connection interaction (high-frequency items form more distant connections — the autonomy half of the model), and §10-§11 schema emergence and productivity from class size.

Verbal categories (Ch 2 §3)

Bybee's six core categories in relevance order: valence, voice, aspect, tense, mood, agreement (number/person/gender are agreement sub-types).

inductive Bybee1985.BybeeCategory : Type

Bybee's Ch 2 verbal-inflectional categories, in her relevance order (stem first). Constructor docstrings quote the coding definitions of Ch 2 §4.

• valence : BybeeCategory

  Differences in the number or role of the arguments the verb stem takes.

• voice : BybeeCategory

  The perspective from which the situation described by the verb stem is viewed.

• aspect : BybeeCategory

  The way the internal temporal constituency of the situation is viewed.

• tense : BybeeCategory

  The situation's placement in time, relative to the moment of speech or some other established point.

• mood : BybeeCategory

  The way the speaker presents the truth of the proposition: probability, possibility, certainty; evidentials are included under mood.

• numberAgr : BybeeCategory

  Concord by number with one or more arguments of the verb.

• personAgr : BybeeCategory

  Concord by person with the subject.

• personAgrObj : BybeeCategory

  Concord by person with the object.

• genderAgr : BybeeCategory

  Concord with arguments by lexical class, assigned arbitrarily or by inherent qualities of the referent.

@[instance_reducible]

instance Bybee1985.instDecidableEqBybeeCategory : DecidableEq BybeeCategory

Equations

• Bybee1985.instDecidableEqBybeeCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bybee1985.instReprBybeeCategory.repr : BybeeCategory → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bybee1985.instReprBybeeCategory : Repr BybeeCategory

Equations

• Bybee1985.instReprBybeeCategory = { reprPrec := Bybee1985.instReprBybeeCategory.repr }

@[instance_reducible]

instance Bybee1985.instFintypeBybeeCategory : Fintype BybeeCategory

Equations

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

Cross-linguistic frequency (Ch 2 §5, Figs 1+2)

Fig 1 counts the 50-sample languages with inflectional expression of a category; Fig 2 counts those with inflectional or derivational expression. Counts are integers because the sample is exactly 50 (count = percentage / 2).

def Bybee1985.inflectionalCount50 : BybeeCategory → ℕ

Languages (of 50) with inflectional expression of c (Fig 1).

Equations

• Bybee1985.inflectionalCount50 Bybee1985.BybeeCategory.valence = 3
• Bybee1985.inflectionalCount50 Bybee1985.BybeeCategory.voice = 13
• Bybee1985.inflectionalCount50 Bybee1985.BybeeCategory.aspect = 26
• Bybee1985.inflectionalCount50 Bybee1985.BybeeCategory.tense = 24
• Bybee1985.inflectionalCount50 Bybee1985.BybeeCategory.mood = 34
• Bybee1985.inflectionalCount50 Bybee1985.BybeeCategory.numberAgr = 27
• Bybee1985.inflectionalCount50 Bybee1985.BybeeCategory.personAgr = 28
• Bybee1985.inflectionalCount50 Bybee1985.BybeeCategory.personAgrObj = 14
• Bybee1985.inflectionalCount50 Bybee1985.BybeeCategory.genderAgr = 8

def Bybee1985.derivOrInflCount50 : BybeeCategory → ℕ

Languages (of 50) with inflectional or derivational expression of c (Fig 2). Valence reaches 90% once valence-changing derivation is counted; only Haitian, Karankawa, Navaho, Serbo-Croatian, and Vietnamese lack it.

Equations

• Bybee1985.derivOrInflCount50 Bybee1985.BybeeCategory.valence = 45
• Bybee1985.derivOrInflCount50 Bybee1985.BybeeCategory.voice = 28
• Bybee1985.derivOrInflCount50 Bybee1985.BybeeCategory.aspect = 37
• Bybee1985.derivOrInflCount50 Bybee1985.BybeeCategory.tense = 25
• Bybee1985.derivOrInflCount50 Bybee1985.BybeeCategory.mood = 34
• Bybee1985.derivOrInflCount50 Bybee1985.BybeeCategory.numberAgr = 33
• Bybee1985.derivOrInflCount50 Bybee1985.BybeeCategory.personAgr = 28
• Bybee1985.derivOrInflCount50 Bybee1985.BybeeCategory.personAgrObj = 14
• Bybee1985.derivOrInflCount50 Bybee1985.BybeeCategory.genderAgr = 8

theorem Bybee1985.valence_highest_when_derivOrInfl (c : BybeeCategory) : derivOrInflCount50 c ≤ derivOrInflCount50 BybeeCategory.valence

Prediction (a), deriv+infl: valence is the most frequent category, reflecting near-universal valence-changing morphology.

theorem Bybee1985.valence_lowest_when_inflectional (c : BybeeCategory) : inflectionalCount50 BybeeCategory.valence ≤ inflectionalCount50 c

The generality prediction: restricted to inflection, valence is the least frequent category (6%, down from 90%) — generality "predicts fewer inflections among the most highly relevant categories", because highly relevant morphology is rarely obligatory across all stems.

theorem Bybee1985.gender_lowest_when_derivOrInfl (c : BybeeCategory) : derivOrInflCount50 BybeeCategory.genderAgr ≤ derivOrInflCount50 c

In the deriv+infl survey (Fig 2), gender agreement is the least frequent category — Bybee's least-relevant verbal category. (Inflection-only, valence drops below gender, so Fig 2 is the relevance-faithful ranking.)

Morpheme order (Ch 2 §6)

Prediction (b): the most relevant categories sit closest to the stem, the least relevant furthest. Bybee tests the four most frequent — aspect, tense, mood, person — counting, per pair, how many languages place one closer than the other. A language with both categories is untestable when the morphemes are portmanteau, on opposite sides of the stem (unless only one is stem-adjacent), or mutually exclusive in one slot; a morpheme expressed by stem modification counts as closer than one expressed by affixation.

structure Bybee1985.OrderPair : Type

A Ch 2 §6 morpheme-order pair.

• closer : BybeeCategory

  The category predicted closer to the stem.

• further : BybeeCategory

  The category predicted further from the stem.

• closerCount : ℕ

  The languages confirming the predicted order.

• furtherCount : ℕ

  The languages showing the opposite order.

• total : ℕ

  The languages having both categories, testable or not.

@[instance_reducible]

instance Bybee1985.instReprOrderPair : Repr OrderPair

Equations

• Bybee1985.instReprOrderPair = { reprPrec := Bybee1985.instReprOrderPair.repr }

def Bybee1985.instReprOrderPair.repr : OrderPair → ℕ → Std.Format

Equations

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

def Bybee1985.orderPairs : List OrderPair

The six pairs Bybee tests in Ch 2 §6; counts verified against the book, each inline comment quoting its source passage.

Equations

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

theorem Bybee1985.aspect_categorical_against_tense_and_mood (p : OrderPair) : p ∈ orderPairs → p.closer = BybeeCategory.aspect → p.further = BybeeCategory.tense ∨ p.further = BybeeCategory.mood → p.furtherCount = 0

Aspect vs. tense and aspect vs. mood are categorical: zero counterexamples in the whole sample, the strongest confirmations Bybee reports.

theorem Bybee1985.mood_person_ordering_is_freest (p : OrderPair) : p ∈ orderPairs → ∀ q ∈ orderPairs, q.closer = BybeeCategory.mood → p.closer ≠ BybeeCategory.mood → p.furtherCount * q.total < q.furtherCount * p.total

Mood vs. person is the freest pair — "the ordering of mood and person is somewhat freer" — cross-multiplied: every other tested pair has a strictly smaller counterexample rate.

theorem Bybee1985.predicted_outnumbers_counter (p : OrderPair) : p ∈ orderPairs → p.furtherCount < p.closerCount

In every one of the six pairs the predicted direction outnumbers the counter-direction (Ch 2 §6 summary).

Connection to substrate MorphCategory.peripherality

MorphCategory.peripherality (in Morphology/RelevanceHierarchy.lean) numerically encodes the hierarchy — lower = closer to stem = more relevant — faithfully to Ch 2 §3 for the six core categories. Its extensions (derivation, degree, negation, nonfinite) are linglib additions, not Bybee's.

def Bybee1985.toMorphCategory : BybeeCategory → Morphology.MorphCategory

Embed BybeeCategory into the substrate MorphCategory. All four agreement subtypes collapse to .agreement: Bybee's verbal-number agreement sits at the low-relevance (rank-8) end with person and gender, not with nominal .number (rank 3). Subject vs object is preserved via the controller role.

Equations

• Bybee1985.toMorphCategory Bybee1985.BybeeCategory.valence = Morphology.MorphCategory.valence
• Bybee1985.toMorphCategory Bybee1985.BybeeCategory.voice = Morphology.MorphCategory.voice
• Bybee1985.toMorphCategory Bybee1985.BybeeCategory.aspect = Morphology.MorphCategory.aspect
• Bybee1985.toMorphCategory Bybee1985.BybeeCategory.tense = Morphology.MorphCategory.tense
• Bybee1985.toMorphCategory Bybee1985.BybeeCategory.mood = Morphology.MorphCategory.mood
• Bybee1985.toMorphCategory Bybee1985.BybeeCategory.numberAgr = Morphology.MorphCategory.agreement Agreement.Controller.subj
• Bybee1985.toMorphCategory Bybee1985.BybeeCategory.personAgr = Morphology.MorphCategory.agreement Agreement.Controller.subj
• Bybee1985.toMorphCategory Bybee1985.BybeeCategory.personAgrObj = Morphology.MorphCategory.agreement Agreement.Controller.obj
• Bybee1985.toMorphCategory Bybee1985.BybeeCategory.genderAgr = Morphology.MorphCategory.agreement Agreement.Controller.subj

theorem Bybee1985.substrate_matches_bybee_hierarchy : List.Pairwise Morphology.MorphCategory.RelevanceLT (List.map toMorphCategory [BybeeCategory.valence, BybeeCategory.voice, BybeeCategory.aspect, BybeeCategory.tense, BybeeCategory.mood, BybeeCategory.personAgr])

The substrate relevance order is strictly increasing along the six Ch 2 §3 categories: it reproduces valence < voice < aspect < tense < mood < agreement.

Grounding the hierarchy in the survey

On the four categories Bybee surveyed (aspect, tense, mood, person), the substrate order is not a free choice: SurveyedCloser, derived from orderPairs, coincides with RelevanceLT via toMorphCategory (survey_order_iso_relevance). So a RespectsRelevanceHierarchy check over these categories rests on an order isomorphism, not a stipulated table.

def Bybee1985.SurveyedCloser (a b : BybeeCategory) : Prop

a is surveyed closer to the stem than b when some tested Ch 2 §6 pair predicts a closer than b and the language counts confirm that direction (predicted majority). Derived from orderPairs, not stipulated.

Equations

• Bybee1985.SurveyedCloser a b = ∃ p ∈ Bybee1985.orderPairs, p.closer = a ∧ p.further = b ∧ p.furtherCount < p.closerCount

@[instance_reducible]

instance Bybee1985.instDecidableRelBybeeCategorySurveyedCloser : DecidableRel SurveyedCloser

Equations

• Bybee1985.instDecidableRelBybeeCategorySurveyedCloser x✝¹ x✝ = Bybee1985.instDecidableRelBybeeCategorySurveyedCloser._aux_1 x✝¹ x✝

def Bybee1985.Surveyed (c : BybeeCategory) : Prop

A category is surveyed if it appears in any tested Ch 2 §6 pair.

Equations

• Bybee1985.Surveyed c = ∃ p ∈ Bybee1985.orderPairs, p.closer = c ∨ p.further = c

@[instance_reducible]

instance Bybee1985.instDecidablePredBybeeCategorySurveyed : DecidablePred Surveyed

Equations

• Bybee1985.instDecidablePredBybeeCategorySurveyed x✝ = Bybee1985.instDecidablePredBybeeCategorySurveyed._aux_1 x✝

theorem Bybee1985.surveyedCloser_irrefl (a : BybeeCategory) : ¬SurveyedCloser a a

SurveyedCloser is irreflexive: no tested pair ranks a category against itself.

theorem Bybee1985.surveyedCloser_trans (a b c : BybeeCategory) : SurveyedCloser a b → SurveyedCloser b c → SurveyedCloser a c

SurveyedCloser is transitive — the §6 survey tested every pair among its categories, so the confirmed dominances compose.

theorem Bybee1985.surveyedCloser_total (a b : BybeeCategory) : Surveyed a → Surveyed b → a ≠ b → SurveyedCloser a b ∨ SurveyedCloser b a

SurveyedCloser is total on the surveyed categories: any two distinct surveyed categories are ordered by the §6 data in exactly one direction. With irreflexivity and transitivity, the survey alone determines a strict total order on its four categories.

theorem Bybee1985.survey_order_iso_relevance (a b : BybeeCategory) : Surveyed a → Surveyed b → (SurveyedCloser a b ↔ (toMorphCategory a).RelevanceLT (toMorphCategory b))

Order isomorphism: on the surveyed categories, SurveyedCloser and the substrate RelevanceLT coincide via toMorphCategory. The hierarchy there is not merely consistent with Bybee's evidence — it is the order the §6 survey determines.

def Bybee1985.bybeeSurveyedOrder : List BybeeCategory

The stem-outward ordering of the surveyed categories — a literal, but validated as fully SurveyedCloser-sorted (bybeeSurveyedOrder_sorted) and exhaustive (bybeeSurveyedOrder_complete).

Equations

• Bybee1985.bybeeSurveyedOrder = [Bybee1985.BybeeCategory.aspect, Bybee1985.BybeeCategory.tense, Bybee1985.BybeeCategory.mood, Bybee1985.BybeeCategory.personAgr]

theorem Bybee1985.bybeeSurveyedOrder_sorted : List.Pairwise SurveyedCloser bybeeSurveyedOrder

theorem Bybee1985.bybeeSurveyedOrder_complete (c : BybeeCategory) : Surveyed c → c ∈ bybeeSurveyedOrder

theorem Bybee1985.bybeeSurveyedOrder_respects_hierarchy : Morphology.RespectsRelevanceHierarchy (List.map toMorphCategory bybeeSurveyedOrder)

The data-derived surveyed order satisfies the substrate predicate, closing the loop between Bybee's §6 evidence and RespectsRelevanceHierarchy.

Ch 5: the dynamic network model

Ch 5 ("Two Principles in a Dynamic Model of Lexical Representation") abandons the generative "is it in the lexicon or not?" binary for two gradient, dynamic notions. Lexical strength (§4): each token of use strengthens an item's representation ("etching it with deeper and darker lines each time"), and strength declines with disuse. Lexical connection (§5): items bear typed connections to other items, and parallel semantic and phonological connections constitute a morphological relation. Bybee's network model is the usage-based competitor to the realisational and generative engines in Morphology/; not to be confused with Network Morphology, the DATR-based default-inheritance framework.

structure Bybee1985.LexicalEntry : Type

A stored item in Bybee's Ch 5 lexicon: a form with its token frequency. Frequency models lexical strength — each token of use strengthens the representation, and strength declines with disuse (§4). Bybee's entries pair the form with a meaning; the semantic side of matching is not modeled here.

• form : String

  The phonological form.

• tokenFreq : ℕ

  The token frequency, modeling lexical strength.

@[instance_reducible]

instance Bybee1985.instReprLexicalEntry : Repr LexicalEntry

Equations

• Bybee1985.instReprLexicalEntry = { reprPrec := Bybee1985.instReprLexicalEntry.repr }

def Bybee1985.instReprLexicalEntry.repr : LexicalEntry → ℕ → Std.Format

Equations

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

inductive Bybee1985.ConnectionKind : Type

The kind of a connection between lexical entries (Ch 5 §5): shared semantic features (tablechair, deepshallow), a shared phonological skeleton without shared meaning (the two senses of crane), the morphological relation (parallel semantic and phonological connections), or identity (§7), the mapping of one word onto an existing representation. Bybee orders their strengths: purely phonological relations "usually go unnoticed", semantic connections are "the strongest and the most important" (go~went supports goed), the morphological relation is the strongest relation between distinct forms, and "the strongest relations are relations of identity".

• semantic : ConnectionKind
• phonological : ConnectionKind
• morphological : ConnectionKind
• identity : ConnectionKind

@[instance_reducible]

instance Bybee1985.instDecidableEqConnectionKind : DecidableEq ConnectionKind

Equations

• Bybee1985.instDecidableEqConnectionKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bybee1985.instReprConnectionKind.repr : ConnectionKind → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bybee1985.instReprConnectionKind : Repr ConnectionKind

Equations

• Bybee1985.instReprConnectionKind = { reprPrec := Bybee1985.instReprConnectionKind.repr }

structure Bybee1985.Connection : Type

A directed typed edge between two forms in the lexical network.

• src : String

  The source form.

• dst : String

  The target form.

• kind : ConnectionKind

  The kind of connection.

def Bybee1985.instReprConnection.repr : Connection → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bybee1985.instReprConnection : Repr Connection

Equations

• Bybee1985.instReprConnection = { reprPrec := Bybee1985.instReprConnection.repr }

structure Bybee1985.Network : Type

A lexical network: entries plus typed connections among them, as in the Ch 5 §8 representation of the Spanish dormir paradigm, whose three stem allomorphs (dwerm, dorm, durm-y) are linked by morphological relations across persons, numbers, and tenses.

• entries : List LexicalEntry

  The stored lexical entries.

• connections : List Connection

  The typed connections among entries.

@[instance_reducible]

instance Bybee1985.instReprNetwork : Repr Network

Equations

• Bybee1985.instReprNetwork = { reprPrec := Bybee1985.instReprNetwork.repr }

def Bybee1985.instReprNetwork.repr : Network → ℕ → Std.Format

Equations

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

def Bybee1985.Network.IsRelatedBy (N : Network) (a b : String) (k : ConnectionKind) : Prop

N.IsRelatedBy a b k asserts that network N has a connection of kind k from form a to form b.

Equations

• N.IsRelatedBy a b k = ∃ c ∈ N.connections, c.src = a ∧ c.dst = b ∧ c.kind = k

def Bybee1985.Network.HasMorphologicalRelation (N : Network) (a b : String) : Prop

N.HasMorphologicalRelation a b asserts that a and b stand in both a semantic and a phonological connection — Ch 5 §5: "if two words are related by both semantic and phonological connections, then a morphological relation exists between them". The relation is derived, not primitive; ConnectionKind.morphological labels edges already so classified.

Equations

• N.HasMorphologicalRelation a b = (N.IsRelatedBy a b Bybee1985.ConnectionKind.semantic ∧ N.IsRelatedBy a b Bybee1985.ConnectionKind.phonological)

Ch 5 §6: strong-verb frequencies

Bybee's central diachronic claim: high-frequency strong verbs maintain their irregularity, low-frequency strong verbs regularize. The table on p. 120 lists the modern descendants of the Strong Verbs of classes I, II, and VII in [Swe82]'s Anglo-Saxon Primer with their all-forms token frequencies from [FK82]. Slit and beat now take the zero allomorph of Past Tense (Bybee's footnote).

def Bybee1985.strongStillStrong : List LexicalEntry

The Strong Verbs that have stayed Strong (p. 120), with all-forms token frequencies.

Equations

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

def Bybee1985.strongRegularized : List LexicalEntry

The Strong Verbs that have regularized or become Weak (p. 120), with all-forms token frequencies.

Equations

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

theorem Bybee1985.strong_verbs_higher_frequency_than_regularized : (List.map (fun (x : LexicalEntry) => x.tokenFreq) strongRegularized).sum * strongStillStrong.length < (List.map (fun (x : LexicalEntry) => x.tokenFreq) strongStillStrong).sum * strongRegularized.length

The mean token frequency of the still-Strong verbs strictly exceeds that of the regularized ones — irregularity survives where lexical strength is high. Stated as the cross-multiplied sum comparison to stay in Nat.