Form-Frequency Correspondence @cite{haspelmath-2021} #

@cite{haspelmath-2021}'s deeper explanation of argument-coding splits: the Role-Reference Association Universal (Universal 1) itself reduces to a general cognitive tendency for frequent expressions to be short.

The key chain of explanation:

Frequency asymmetry: Some role-reference combinations are more frequent than others (e.g., "I saw him" is more frequent than "He saw me"; animate agents are more frequent than inanimate agents).
Form-frequency correspondence: More frequent expressions tend to get shorter forms. This is a diachronic process — frequent forms erode phonologically and resist analogical extension of explicit markers.
Coding asymmetry: The "usual" role-reference associations (which ARE the frequent ones) therefore get shorter (often zero) coding, while the "unusual" associations get longer (overt) coding.

This explains WHY the monotonicity patterns in DOM/DSM/differential indexing exist: they track frequency gradients on the prominence scales.

source

inductive Core.FormFrequency.CodingLength :

Type

Relative coding length of an argument expression.

Haspelmath's claim is about relative length, not absolute morpheme counts. Zero marking is shorter than overt marking; shorter overt markers are shorter than longer ones.

zero : CodingLength
Zero coding (no overt marker)
short : CodingLength
Short overt coding (e.g., clitic, monosyllabic affix)
long : CodingLength
Long overt coding (e.g., full adposition, bisyllabic affix)

Instances For

source

instance Core.FormFrequency.instDecidableEqCodingLength :

DecidableEq CodingLength

Equations

Core.FormFrequency.instDecidableEqCodingLength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Core.FormFrequency.instBEqCodingLength.beq :

CodingLength → CodingLength → Bool

Equations

Core.FormFrequency.instBEqCodingLength.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Core.FormFrequency.instBEqCodingLength :

BEq CodingLength

Equations

Core.FormFrequency.instBEqCodingLength = { beq := Core.FormFrequency.instBEqCodingLength.beq }

source

instance Core.FormFrequency.instReprCodingLength :

Repr CodingLength

Equations

Core.FormFrequency.instReprCodingLength = { reprPrec := Core.FormFrequency.instReprCodingLength.repr }

source

def Core.FormFrequency.instReprCodingLength.repr :

CodingLength → Nat → Std.Format

Equations

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

Instances For

source

def Core.FormFrequency.CodingLength.rank :

CodingLength → Nat

Numeric rank: zero (0) < short (1) < long (2).

Equations

Instances For

source

def Core.FormFrequency.respectsFormFrequency {α : Type} [DecidableEq α] (domain : List α) (freq : α → Nat) (coding : α → CodingLength) :

Bool

The form-frequency correspondence predicate: a coding system respects the form-frequency correspondence if more frequent role-reference combinations receive shorter (or equal) coding.

freq returns relative frequency (higher = more frequent). coding returns the coding length for that combination.

The predicate holds when: freq(x) > freq(y) → coding(x) ≤ coding(y).

Equations

Core.FormFrequency.respectsFormFrequency domain freq coding = domain.all fun (x : α) => domain.all fun (y : α) => if freq x > freq y then decide ((coding x).rank ≤ (coding y).rank) else true

Instances For

source

def Core.FormFrequency.argumentCodingRespectsFrequency (_role : Prominence.ArgumentRole) (freq : Prominence.AnimacyLevel → Prominence.DefinitenessLevel → Nat) (coding : Prominence.AnimacyLevel → Prominence.DefinitenessLevel → CodingLength) :

Bool

The form-frequency correspondence applied to argument coding: usual role-reference associations (high frequency) should get shorter coding than unusual ones (low frequency).

This is the core claim of @cite{haspelmath-2021}: differential marking patterns are explained by frequency asymmetries, not by grammatical function per se.

Equations

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

Instances For

source

def Core.FormFrequency.frequencyProxy (role : Prominence.ArgumentRole) (a : Prominence.AnimacyLevel) (d : Prominence.DefinitenessLevel) :

Nat

Haspelmath's bridge claim: for P/T arguments, prominence correlates positively with unusualness (and thus with coding length). That is, the frequency of a P with a given prominence is inversely related to prominence rank.

For A/R arguments, the relationship is reversed: frequency is directly related to prominence rank.

This function returns a frequency proxy based on prominence rank and role. It captures the claim that A-prominence is positively correlated with frequency while P-prominence is negatively correlated.

Equations

Instances For

source

theorem Core.FormFrequency.frequency_proxy_matches_default (role : Prominence.ArgumentRole) (a : Prominence.AnimacyLevel) (d : Prominence.DefinitenessLevel) :

Prominence.isDefaultZone role a d = true → frequencyProxy role a d ≥ 3

The frequency proxy predicts that usual associations are more frequent.

source

inductive Core.FormFrequency.VoiceDirection :

Type

Verb voice direction for direct/inverse systems. Direct forms mark downstream (usual) scenarios; inverse forms mark upstream (unusual) scenarios with morphologically more complex marking.