Levy (2008): Expectation-Based Syntactic Comprehension

This file formalizes the resource-allocation theory of processing difficulty of [Lev08]. A comprehender maintains a probability distribution over the complete structures consistent with the input so far, the prior conditioned on consistency with the prefix (posterior), and the difficulty of a word is the relative entropy of the updated distribution with respect to the old one. Incremental update equals direct conditioning (posterior_incremental), and the paper's central result is that the difficulty so defined is exactly the word's surprisal (klDiv_posterior_eq_surprisal), [Hal01]'s measure, for any generative process over structures: the surprisal of the word under the law of the next word the process induces. Surprisal is therefore a causal bottleneck: processes agreeing on conditional word probabilities incur identical difficulty whatever their structures (bottleneck).

Implementation notes

Structures live in an arbitrary discrete measurable space, covering the paper's normally infinite structure set; the generative process is a probability measure over them, and the prefix apparatus (consistent, nextProb, nextWord) is Processing/Surprisal/PrefixProbability.lean. The prior is fixed throughout, matching the paper's caveat that the equivalence holds only when extra-sentential context does not change while the word is processed.

References

• [Lev08]
• [Hal01]

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

Pᵢ (eq. (3)): the comprehender's distribution over complete structures given the prefix — the prior conditioned on consistency.

Equations

• Levy2008.posterior P str ws = P[|Surprisal.consistent str ws]

theorem Levy2008.posterior_consistent_append {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) (ws : List W) (w : W) : (posterior P str ws) (Surprisal.consistent str (ws ++ [w])) = Surprisal.nextProb P str ws w

The posterior's mass on the structures consistent with the next word is the induced conditional word probability.

theorem Levy2008.posterior_incremental {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) (ws : List W) (w : W) [DiscreteMeasurableSpace T] [MeasureTheory.IsProbabilityMeasure P] : (posterior P str ws)[|Surprisal.consistent str (ws ++ [w])] = posterior P str (ws ++ [w])

Incremental update equals direct conditioning (eqs. (5)–(8)): conditioning the current posterior on consistency with the extended prefix is conditioning the prior on the extended prefix directly.

theorem Levy2008.klDiv_posterior_eq_surprisal {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) (ws : List W) (w : W) [DiscreteMeasurableSpace T] [MeasureTheory.IsProbabilityMeasure P] [MeasurableSpace W] [MeasurableSingletonClass W] (h : P (Surprisal.consistent str (ws ++ [w])) ≠ 0) : InformationTheory.klDiv (posterior P str (ws ++ [w])) (posterior P str ws) = ENNReal.ofReal (InformationTheory.surprisal (Surprisal.nextWord P str ws) (some w))

The paper's eq. (4): the relative entropy of the updated distribution over structures with respect to the pre-update distribution is the surprisal of the word that triggered the update.

theorem Levy2008.bottleneck {T : Type u_1} {W : Type u_2} [MeasurableSpace T] (P : MeasureTheory.Measure T) (str : T → List W) (ws : List W) (w : W) [DiscreteMeasurableSpace T] [MeasureTheory.IsProbabilityMeasure P] [MeasurableSpace W] [MeasurableSingletonClass W] {T' : Type u_3} [MeasurableSpace T'] [DiscreteMeasurableSpace T'] (P' : MeasureTheory.Measure T') [MeasureTheory.IsProbabilityMeasure P'] (str' : T' → List W) (hagree : Surprisal.nextProb P str ws w = Surprisal.nextProb P' str' ws w) (h : P (Surprisal.consistent str (ws ++ [w])) ≠ 0) (h' : P' (Surprisal.consistent str' (ws ++ [w])) ≠ 0) : InformationTheory.klDiv (posterior P str (ws ++ [w])) (posterior P str ws) = InformationTheory.klDiv (posterior P' str' (ws ++ [w])) (posterior P' str' ws)

The causal bottleneck (§2.3, Fig. 1b): two generative processes assigning the same conditional word probability incur the same update difficulty, regardless of their structural representations.