Information Propagation and Contraction in Functional Interpretations
For researchers in proof theory and functional interpretations, this provides a modular algebraic framework that unifies and extends existing interpretations, though it is an incremental theoretical contribution.
The paper separates affine information propagation and contraction in functional interpretations, introducing information nuclei to capture the affine component and a formula-indexed contraction structure for contraction. This yields a uniform framework for specifying information carried by extracted realizers, enabling systematic enrichment with auxiliary data like continuity information.
This paper separates two components of functional interpretations: affine information propagation and contraction. We introduce information nuclei as an algebraic interface to capture the affine component. An information nucleus specifies what information is associated with finite-type objects, how exact objects are compatible with such information, and how information is propagated through functions. From any information nucleus we obtain a formula translation and a soundness theorem for affine finite-type arithmetic. Extending soundness to finite-type arithmetic with contraction requires one additional ingredient: a formula-indexed contraction structure reducing the challenges generated by duplicated assumptions to a single challenge. Finite collections of candidates with union yield a Herbrand-style interpretation, while exact information with challenge selection yields the usual Dialectica interpretation over an arithmetic system restricted to decidable primitive formulas. The resulting framework provides a uniform method for specifying the information carried by extracted realizers, allowing existing functional interpretations to be systematically enriched with auxiliary data, such as continuity information.