Kiegeland, Snæbjarnarson, Vieira and Cotterell (2026): On the Proper Treatment of Units in Surprisal Theory

[KSVC26] separate the unit of analysis from the alphabet of the language model. A unit parser maps each symbol string to a string of units, and the language model over units is the pushforward of the one over symbols: the prefix probability of a unit string is the probability of the symbol strings whose parse extends it (Surprisal.consistent). To compute it with a language model over symbols, each unit is spelled as its underlying string followed by a separator and the parse is transduced into spellings. The spelling of a unit string is a prefix of the spelling of a parse exactly when the unit string is a prefix of the parse (encode_isPrefix_encode_iff, the paper's prefix identity), so the unit model's conditional prefix probabilities are the transduced model's conditional prefix probabilities of spellings (cond_consistent_encode).

The identity depends on the separator closing each unit. Placed at the onset instead, a unit's spelling is a prefix of the spelling of a longer unit sharing its underlying prefix, and the prefix identity fails (not_forall_encodeOnset_isPrefix_iff). In the paper's two-unit example the unit model and the completion spelling give the shorter unit prefix probability one half, the onset spelling one (prob_consistent_unit, prob_consistent_encode, prob_consistent_encodeOnset). The separator also carries probability of its own: a unit's conditional probability is that of its underlying string times that of the separator after it (cond_consistent_encode_singleton), so summing symbol surprisals over a unit's spelling omits the boundary.

Implementation notes

• The separator is none in Option Ξ, and a unit's underlying string is given by an injective spelling function; the paper takes units to be strings over Ξ.
• The paper computes the pushforward with finite-state transducers under a regularity assumption on the unit inventory; the identities here hold for any deterministic unit parser and any injective spelling.
• The paper's aggregation over regions of interest and its reading-time analyses are not formalized.

References

• [KSVC26]

def KiegelandEtAl2026.encode {U : Type u_1} {Ξ : Type u_2} (ξ : U → List Ξ) (us : List U) : List (Option Ξ)

The spelling of a unit string: each unit's underlying string followed by the separator none.

Equations

• KiegelandEtAl2026.encode ξ us = List.flatMap (fun (u : U) => List.map some (ξ u) ++ [none]) us

def KiegelandEtAl2026.encodeOnset {U : Type u_1} {Ξ : Type u_2} (ξ : U → List Ξ) (us : List U) : List (Option Ξ)

The onset spelling: the separator before each unit's underlying string.

Equations

• KiegelandEtAl2026.encodeOnset ξ us = List.flatMap (fun (u : U) => none :: List.map some (ξ u)) us

@[simp]

theorem KiegelandEtAl2026.encode_nil {U : Type u_1} {Ξ : Type u_2} (ξ : U → List Ξ) : encode ξ [] = []

theorem KiegelandEtAl2026.encode_cons {U : Type u_1} {Ξ : Type u_2} (ξ : U → List Ξ) (u : U) (us : List U) : encode ξ (u :: us) = List.map some (ξ u) ++ none :: encode ξ us

theorem KiegelandEtAl2026.encode_append {U : Type u_1} {Ξ : Type u_2} (ξ : U → List Ξ) (us vs : List U) : encode ξ (us ++ vs) = encode ξ us ++ encode ξ vs

theorem KiegelandEtAl2026.encode_isPrefix_encode_iff {U : Type u_1} {Ξ : Type u_2} {ξ : U → List Ξ} (hξ : Function.Injective ξ) {us vs : List U} : encode ξ us <+: encode ξ vs ↔ us <+: vs

The prefix identity: under the completion convention, the spelling of a unit string is a prefix of the spelling of another exactly when the unit string is a prefix of it.

theorem KiegelandEtAl2026.consistent_encode_comp {U : Type u_1} {Ξ : Type u_2} {ξ : U → List Ξ} {T : Type u_3} (hξ : Function.Injective ξ) (ρ : T → List U) (us : List U) : Surprisal.consistent (encode ξ ∘ ρ) (encode ξ us) = Surprisal.consistent ρ us

The symbol strings whose parse extends a unit string are those whose transduced parse extends its spelling.

theorem KiegelandEtAl2026.cond_consistent_encode {U : Type u_1} {Ξ : Type u_2} {ξ : U → List Ξ} {T : Type u_3} [MeasurableSpace T] (P : MeasureTheory.Measure T) (hξ : Function.Injective ξ) (ρ : T → List U) (cs us : List U) : P[Surprisal.consistent ρ (cs ++ us) | Surprisal.consistent ρ cs] = P[Surprisal.consistent (encode ξ ∘ ρ) (encode ξ cs ++ encode ξ us) | Surprisal.consistent (encode ξ ∘ ρ) (encode ξ cs)]

The unit model's conditional prefix probability of a continuation is the transduced model's conditional prefix probability of its spelling.

theorem KiegelandEtAl2026.cond_consistent_encode_singleton {U : Type u_1} {Ξ : Type u_2} {ξ : U → List Ξ} {T : Type u_3} [MeasurableSpace T] (P : MeasureTheory.Measure T) [DiscreteMeasurableSpace T] [MeasureTheory.IsFiniteMeasure P] (hξ : Function.Injective ξ) (ρ : T → List U) (cs : List U) (u : U) : P[Surprisal.consistent ρ (cs ++ [u]) | Surprisal.consistent ρ cs] = P[Surprisal.consistent (encode ξ ∘ ρ) (encode ξ cs ++ List.map some (ξ u)) | Surprisal.consistent (encode ξ ∘ ρ) (encode ξ cs)] * P[Surprisal.consistent (encode ξ ∘ ρ) (encode ξ cs ++ List.map some (ξ u) ++ [none]) | Surprisal.consistent (encode ξ ∘ ρ) (encode ξ cs ++ List.map some (ξ u))]

A unit's conditional probability is the conditional probability of its underlying string times that of the separator after it.

The two-unit example

def KiegelandEtAl2026.spell : Bool → List Char

The paper's two units: false is spelled a and true is spelled ab.

Equations

• KiegelandEtAl2026.spell false = ['a']
• KiegelandEtAl2026.spell true = ['a', 'b']

def KiegelandEtAl2026.parse (s : List Char) : List Bool

The parse of the source strings a and ab into the two units.

Equations

• KiegelandEtAl2026.parse s = if s = ['a'] then [false] else if s = ['a', 'b'] then [true] else []

noncomputable def KiegelandEtAl2026.source : MeasureTheory.Measure (List Char)

The source model: a and ab with probability one half each.

Equations

• KiegelandEtAl2026.source = 2⁻¹ • MeasureTheory.Measure.dirac ['a'] + 2⁻¹ • MeasureTheory.Measure.dirac ['a', 'b']

theorem KiegelandEtAl2026.not_forall_encodeOnset_isPrefix_iff : ¬∀ (us vs : List Bool), encodeOnset spell us <+: encodeOnset spell vs ↔ us <+: vs

Under the onset convention the prefix identity fails, although the spelling is injective: the onset spelling of a is a prefix of that of ab.

theorem KiegelandEtAl2026.prob_consistent_unit : source (Surprisal.consistent parse [false]) = 2⁻¹

theorem KiegelandEtAl2026.prob_consistent_encode : source (Surprisal.consistent (encode spell ∘ parse) (encode spell [false])) = 2⁻¹

theorem KiegelandEtAl2026.prob_consistent_encodeOnset : source (Surprisal.consistent (encodeOnset spell ∘ parse) (encodeOnset spell [false])) = 1