Memory processes

This file defines the memory process of [FGL20]'s lossy-context surprisal. A memory process encodes a context as a distribution over memory representations and predicts the next word from the representation alone, so that the representation mediates all information flow from the context to the prediction. The difficulty of a word in a context is its expected surprisal over the representations the context can produce, and the average difficulty of the process under a language model and a context prior averages it over contexts and the words they predict.

A process whose encoder is deterministic and whose predictor, read through the encoder, is a language model loses no information, and its difficulty is that model's surprisal: surprisal theory is the lossless special case.

Main definitions

• MemoryProcess: an encoder Kernel C R and a predictor Kernel R W.
• MemoryProcess.expectedSurprisal, MemoryProcess.averageDifficulty.
• MemoryProcess.IsLosslessFor: the process realizes a language model through a deterministic summary of the context.

Main results

• MemoryProcess.expectedSurprisal_of_dirac, MemoryProcess.expectedSurprisal_of_bernoulli: expected surprisal under a point-mass and under a two-point encoder.
• MemoryProcess.expectedSurprisal_eq_surprisal_of_lossless.

References

• [FGL20]

structure LossyContext.MemoryProcess (C : Type u_4) (R : Type u_5) (W : Type u_6) [MeasurableSpace C] [MeasurableSpace R] [MeasurableSpace W] : Type (max (max u_4 u_5) u_6)

A memory process: a lossy encoder from contexts to memory representations and a predictor from memory representations to next words. The representation mediates all information flow from the context to the prediction.

• encode : ProbabilityTheory.Kernel C R

  The distribution over memory representations a context produces.

• predict : ProbabilityTheory.Kernel R W

  The next-word distribution a memory representation predicts.

noncomputable def LossyContext.MemoryProcess.perStateSurprisal {C : Type u_1} {R : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace R] [MeasurableSpace W] (mp : MemoryProcess C R W) (r : R) (w : W) : ℝ

The surprisal of the word w at the memory representation r.

Equations

• mp.perStateSurprisal r w = InformationTheory.surprisal (mp.predict r) w

noncomputable def LossyContext.MemoryProcess.expectedSurprisal {C : Type u_1} {R : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace R] [MeasurableSpace W] (mp : MemoryProcess C R W) (c : C) (w : W) : ℝ

The expected surprisal of w in the context c: the difficulty of w under the process.

Equations

• mp.expectedSurprisal c w = ∫ (r : R), mp.perStateSurprisal r w ∂mp.encode c

noncomputable def LossyContext.MemoryProcess.averageDifficulty {C : Type u_1} {R : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace R] [MeasurableSpace W] (mp : MemoryProcess C R W) (L : ProbabilityTheory.Kernel C W) (π : MeasureTheory.Measure C) : ℝ

The average difficulty of the process under the language model L and the context prior π: expected surprisal averaged over contexts and the words they predict.

Equations

• mp.averageDifficulty L π = ∫ (c : C), ∫ (w : W), mp.expectedSurprisal c w ∂L c ∂π

def LossyContext.MemoryProcess.IsLosslessFor {C : Type u_1} {R : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace R] [MeasurableSpace W] (mp : MemoryProcess C R W) (L : ProbabilityTheory.Kernel C W) : Prop

The process realizes the language model L through the summary f: the encoder is deterministic at f, and the predictor pulled back along f is L.

Equations

• mp.IsLosslessFor L = ∃ (f : C → R) (hf : Measurable f), mp.encode = ProbabilityTheory.Kernel.deterministic f hf ∧ mp.predict.comap f hf = L

theorem LossyContext.MemoryProcess.isLosslessFor_comap {C : Type u_1} {R : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace R] [MeasurableSpace W] {mp : MemoryProcess C R W} {f : C → R} {hf : Measurable f} (h : mp.encode = ProbabilityTheory.Kernel.deterministic f hf) : mp.IsLosslessFor (mp.predict.comap f hf)

A deterministic encoder realizes the language model that reads the predictor through it.

theorem LossyContext.MemoryProcess.expectedSurprisal_of_dirac {C : Type u_1} {R : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace R] [MeasurableSpace W] {mp : MemoryProcess C R W} [MeasurableSingletonClass R] {c : C} {r : R} (h : mp.encode c = MeasureTheory.Measure.dirac r) (w : W) : mp.expectedSurprisal c w = mp.perStateSurprisal r w

theorem LossyContext.MemoryProcess.expectedSurprisal_of_bernoulli {C : Type u_1} {R : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace R] [MeasurableSpace W] {mp : MemoryProcess C R W} [MeasurableSingletonClass R] {c : C} {r₁ r₂ : R} {p : ↑unitInterval} (h : mp.encode c = ProbabilityTheory.bernoulliMeasure r₁ r₂ p) (w : W) : mp.expectedSurprisal c w = ↑p * mp.perStateSurprisal r₁ w + (1 - ↑p) * mp.perStateSurprisal r₂ w

Expected surprisal under a Bernoulli encoder, which produces r₁ with probability p and r₂ otherwise.

theorem LossyContext.MemoryProcess.expectedSurprisal_of_deterministic {C : Type u_1} {R : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace R] [MeasurableSpace W] {mp : MemoryProcess C R W} [MeasurableSingletonClass R] {f : C → R} {hf : Measurable f} (h : mp.encode = ProbabilityTheory.Kernel.deterministic f hf) (c : C) (w : W) : mp.expectedSurprisal c w = mp.perStateSurprisal (f c) w

theorem LossyContext.MemoryProcess.expectedSurprisal_eq_surprisal_of_lossless {C : Type u_1} {R : Type u_2} {W : Type u_3} [MeasurableSpace C] [MeasurableSpace R] [MeasurableSpace W] {mp : MemoryProcess C R W} [MeasurableSingletonClass R] {L : ProbabilityTheory.Kernel C W} (h : mp.IsLosslessFor L) (c : C) (w : W) : mp.expectedSurprisal c w = InformationTheory.surprisal (L c) w

A lossless process has the surprisal of the language model it realizes: surprisal theory is the lossless special case of lossy-context surprisal.