Yang (2016): The Price of Linguistic Productivity

This file formalizes the Tolerance Principle of [Yan16]: a rule applicable to N items is productive only if its exceptions number at most N / ln N (threshold, tolerates). The principle is derived from the cost of rule access under the Elsewhere Condition, in the form first given in [Yan05]. The N items are ranked by frequency and searched serially, so under a Zipfian distribution the expected time to reach an item in a list of N is N / H_N, with H_N the harmonic number (listTime). A productive rule lists its M exceptions before the rule, so an exception is found in expected time T(M, M) and a regular item after all M exceptions have been rejected (ruleTime); listing everything costs T(N, N), and the rule is productive when the former does not exceed the latter (Productive). Since the rule's cost never exceeds M (ruleTime_le), any rule with at most N / H_N exceptions is productive (productive_of_le_listTime), hence any rule with at most N / (1 + ln N) exceptions (productive_of_le_div_one_add_log); the threshold of the principle replaces the harmonic number by the logarithm it approximates. The German feminine plural, with some eighty exceptions among at least five hundred nouns, is tolerated (tolerates_500_80).

Implementation notes

Yang's simplification of the rule's cost, that a random subset of a Zipfian list is again Zipfian, is taken as the definition of ruleTime. The threshold is stated with the natural logarithm as in the book, and its relation to the exact harmonic bound is recorded by the sufficiency theorems rather than by the book's approximate solution of T(N, N) = T(N, M). Mathlib's convention that division by zero is zero makes the threshold vanish at N ≤ 1.

References

• [Yan16]
• [Yan05]

The Tolerance Principle

noncomputable def Yang2016.threshold (n : ℕ) : ℝ

The tolerance threshold for a rule applicable to n items.

Equations

• Yang2016.threshold n = ↑n / Real.log ↑n

def Yang2016.tolerates (n e : ℕ) : Prop

A rule with n items in scope and e exceptions is tolerated when the exceptions fit under the threshold.

Equations

• Yang2016.tolerates n e = (↑e ≤ Yang2016.threshold n)

theorem Yang2016.threshold_nonneg (n : ℕ) : 0 ≤ threshold n

The threshold is nonnegative.

theorem Yang2016.tolerates_zero (n : ℕ) : tolerates n 0

A rule with no exceptions is always tolerated.

Serial access under Zipf

noncomputable def Yang2016.listTime (n : ℕ) : ℝ

The expected time to reach an item in a frequency-ranked list of n items whose frequencies are Zipfian: the i-th item has probability 1 / (i H_n) and is reached in i steps.

Equations

• Yang2016.listTime n = ∑ i ∈ Finset.range n, 1 / ((↑i + 1) * ↑(harmonic n)) * (↑i + 1)

theorem Yang2016.listTime_eq (n : ℕ) : listTime n = ↑n / ↑(harmonic n)

The expected access time of a list is n / H_n.

theorem Yang2016.listTime_le_self (n : ℕ) : listTime n ≤ ↑n

Access in a list never takes longer than its length.

noncomputable def Yang2016.ruleTime (n m : ℕ) : ℝ

The expected access time of a productive rule with m exceptions among n items: with probability m / n the item is an exception, found in a list of m; otherwise it is reached after the m exceptions have been rejected.

Equations

• Yang2016.ruleTime n m = ↑m / ↑n * Yang2016.listTime m + (1 - ↑m / ↑n) * ↑m

def Yang2016.Productive (n m : ℕ) : Prop

A rule is productive when it costs no more than listing everything.

Equations

• Yang2016.Productive n m = (Yang2016.ruleTime n m ≤ Yang2016.listTime n)

theorem Yang2016.ruleTime_self (n : ℕ) (hn : 0 < n) : ruleTime n n = listTime n

Listing everything is the rule with every item an exception.

theorem Yang2016.ruleTime_le {n m : ℕ} (hmn : m ≤ n) : ruleTime n m ≤ ↑m

The rule's cost never exceeds the number of exceptions.

theorem Yang2016.productive_of_le_listTime {n m : ℕ} (hmn : m ≤ n) (h : ↑m ≤ listTime n) : Productive n m

A rule whose exceptions fit under the exact harmonic bound n / H_n is productive.

theorem Yang2016.div_one_add_log_le_listTime (n : ℕ) : ↑n / (1 + Real.log ↑n) ≤ listTime n

The harmonic bound is at least n / (1 + ln n).

theorem Yang2016.productive_of_le_div_one_add_log {n m : ℕ} (hmn : m ≤ n) (h : ↑m ≤ ↑n / (1 + Real.log ↑n)) : Productive n m

A rule with at most n / (1 + ln n) exceptions is productive.

theorem Yang2016.div_one_add_log_le_threshold {n : ℕ} (hn : 2 ≤ n) : ↑n / (1 + Real.log ↑n) ≤ threshold n

The book's threshold exceeds the exact sufficient bound: the logarithm undercounts the harmonic number.

The German feminine plural

theorem Yang2016.tolerates_500_80 : tolerates 500 80

Some eighty feminine nouns fail to pluralize in -(e)n, which five hundred feminine nouns suffice to tolerate.