Hale (2001): A Probabilistic Earley Parser as a Psycholinguistic Model

This file formalizes the linking hypothesis of [Hal01]. Cognitive load is the total probability of the structural analyses the input so far has disconfirmed (section 4): for a consistent grammar, the effort spent on a prefix is one minus its prefix probability, disconfirmed, and word-by-word reading time is proportional to the log of the ratio of the prefix probability before the word to the one after it, the word's surprisal (surprisal_nextWord_eq_log_div), where the prefix probability is [Sto95]'s, computed by a probabilistic Earley parser that is strong-competence, frequency-sensitive, and eager (Principles 1 to 3). The parser computes every parse, so the theory is one of total parallelism (section 3): garden-pathing needs no reanalysis and happens exactly at words where the disconfirmed analyses comprise most of the probability mass (log_le_surprisal_nextWord), which is how the paper reads the spike at fell in the horse raced past the barn fell, where grammar (1) puts the prefix probability before the word at more than ten times the one after it (section 6.1), and the subject and object relative asymmetry of grammar (3) (section 6.3). The two levels of the linking hypothesis agree, since prefix-level load only grows along a sentence (disconfirmed_mono) and word-level surprisals telescope to the negative log of the sentence's prefix mass (totalSurprisal_nil_eq).

Implementation notes

The demonstrations' numerics, grammars (1) to (3) and the reading-time figures, require Stolcke's Earley chart over recursive probabilistic context-free grammars and await an Earley substrate; the theorems here are the grammar-independent content of the linking hypothesis, stated for any probability measure over structures with string yields.

The paper defines a word's surprisal as the log ratio of prefix probabilities. Here it is the library's surprisal of the word under the law of the next word, Surprisal.nextWord, the negative log of its conditional probability, and the paper's ratio is a theorem about it.

References

• [Hal01]
• [Sto95]
• [Lev08]

noncomputable def Hale2001.disconfirmed {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) (ws : List W) : ENNReal

Prefix-level cognitive load (section 4): the total probability of the analyses the prefix has disconfirmed.

Equations

• Hale2001.disconfirmed P str ws = 1 - P (Surprisal.consistent str ws)

theorem Hale2001.disconfirmed_mono {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) {ws ws' : List W} (h : ws <+: ws') : disconfirmed P str ws ≤ disconfirmed P str ws'

Disconfirmed mass grows along a sentence: an extension has disconfirmed at least what its prefix has, so prefix-level load never decreases.

noncomputable def Hale2001.totalSurprisal {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) [MeasurableSpace W] : List W → List W → ℝ

The surprisals of the words of rest, read one by one after the prefix acc.

Equations

• Hale2001.totalSurprisal P str x✝ [] = 0
• Hale2001.totalSurprisal P str x✝ (w :: rest) = InformationTheory.surprisal (Surprisal.nextWord P str x✝) (some w) + Hale2001.totalSurprisal P str (x✝ ++ [w]) rest

theorem Hale2001.surprisal_nextWord_eq_log_div {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) (ws : List W) (w : W) [MeasurableSpace W] [DiscreteMeasurableSpace T] [MeasurableSingletonClass W] : InformationTheory.surprisal (Surprisal.nextWord P str ws) (some w) = Real.log (P.real (Surprisal.consistent str ws) / P.real (Surprisal.consistent str (ws ++ [w])))

Word-level cognitive load (section 4): a word's surprisal is the log of the ratio of the prefix probability before the word to the prefix probability after it.

theorem Hale2001.surprisal_nextWord_eq_log_one_add {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) (ws : List W) (w : W) [MeasurableSpace W] [DiscreteMeasurableSpace T] [MeasurableSingletonClass W] (ha : 0 < P.real (Surprisal.consistent str (ws ++ [w]))) : InformationTheory.surprisal (Surprisal.nextWord P str ws) (some w) = Real.log (1 + (P.real (Surprisal.consistent str ws) - P.real (Surprisal.consistent str (ws ++ [w]))) / P.real (Surprisal.consistent str (ws ++ [w])))

Surprisal in disconfirmation form: the log of one plus the ratio of the mass disconfirmed at the word to the mass surviving it.

theorem Hale2001.log_le_surprisal_nextWord {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) (ws : List W) (w : W) [MeasurableSpace W] [DiscreteMeasurableSpace T] [MeasurableSingletonClass W] {k : ℝ} (hk : 0 ≤ k) (ha : 0 < P.real (Surprisal.consistent str (ws ++ [w]))) (hdis : k * P.real (Surprisal.consistent str (ws ++ [w])) ≤ P.real (Surprisal.consistent str ws) - P.real (Surprisal.consistent str (ws ++ [w]))) : Real.log (1 + k) ≤ InformationTheory.surprisal (Surprisal.nextWord P str ws) (some w)

Garden-pathing (section 6.1): if the mass disconfirmed at a word is at least k times the surviving mass, the word's surprisal is at least log (1 + k); difficulty spikes exactly where the disconfirmable analyses comprise a great amount of probability.

Load along a sentence

@[simp]

theorem Hale2001.disconfirmed_nil {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) [MeasureTheory.IsProbabilityMeasure P] : disconfirmed P str [] = 0

No analysis has been disconfirmed before any input is seen.

theorem Hale2001.totalSurprisal_eq {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) [MeasurableSpace W] [DiscreteMeasurableSpace T] [MeasurableSingletonClass W] [MeasureTheory.IsProbabilityMeasure P] {acc rest : List W} (hpos : 0 < P.real (Surprisal.consistent str (acc ++ rest))) : totalSurprisal P str acc rest = Real.log (P.real (Surprisal.consistent str acc)) - Real.log (P.real (Surprisal.consistent str (acc ++ rest)))

Word surprisals telescope: reading rest after acc costs the log of the ratio of the masses before and after, whenever the whole string has positive mass.

theorem Hale2001.totalSurprisal_nil_eq {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) [MeasurableSpace W] [DiscreteMeasurableSpace T] [MeasurableSingletonClass W] [MeasureTheory.IsProbabilityMeasure P] {ws : List W} (hpos : 0 < P.real (Surprisal.consistent str ws)) : totalSurprisal P str [] ws = -Real.log (P.real (Surprisal.consistent str ws))

The linking hypothesis at the sentence level (section 4): the total surprisal of a sentence is the negative log of its prefix mass, the whole disconfirmed mass paid out word by word.