Prototype Theory: Gradient Meaning over a Numerical Domain

Generic Prototype-Theory operator parameterized by per-word prototype and spread: meaning is a non-negative gradient peaking at the prototype and falling off with distance, scaled by spread.

The bump kernel is a rational-arithmetic approximation of a Gaussian exp(-x²) — specifically, a piecewise-linear-in-|x| tent that is genuinely non-negative, monotone-decreasing in |x|, and continuous at the breakpoints. See bumpKernel.

This is the parametric theory consumed by paper-specific PT models (e.g., Studies/VanTielEtAl2021.lean), which provide their own prototype/spread parameter values.

def Semantics.Probabilistic.PrototypeTheory.bumpKernel (x : ℚ) : ℚ

Tent kernel: max 0 (1 - |x|). Non-negative, monotone-decreasing in |x|, continuous, peak 1 at x = 0, vanishes for |x| ≥ 1. Approximates a Gaussian bump in rational arithmetic without the discontinuities and negative excursions of the previous piecewise quadratic.

Equations

• Semantics.Probabilistic.PrototypeTheory.bumpKernel x = if (if x < 0 then -x else x) ≥ 1 then 0 else 1 - if x < 0 then -x else x

theorem Semantics.Probabilistic.PrototypeTheory.bumpKernel_nonneg (x : ℚ) : 0 ≤ bumpKernel x

def Semantics.Probabilistic.PrototypeTheory.ptMeaning (n p : ℕ) (d : ℚ) (t : Fin (n + 1)) : ℚ

PT meaning at intersection-count t for a word with prototype p and spread d > 0 over a domain of size n.

Distance from the prototype is normalized by spread, then passed through the bump kernel.

Equations

• Semantics.Probabilistic.PrototypeTheory.ptMeaning n p d t = Semantics.Probabilistic.PrototypeTheory.bumpKernel ((↑↑t - ↑p) / d)

theorem Semantics.Probabilistic.PrototypeTheory.ptMeaning_nonneg (n p : ℕ) (d : ℚ) (t : Fin (n + 1)) : 0 ≤ ptMeaning n p d t