函数解释中的信息传播与收缩
Information Propagation and Contraction in Functional Interpretations
浏览论文内容
中文总结 AI 辅助
研究函数解释中信息传播与收缩，引入信息核，给出仿射有限类型算术的公式翻译和健全性定理，通过公式索引收缩结构扩展健全性，提供统一方法指定提取实现者携带信息，可丰富现有函数解释。
中文摘要 AI 辅助
本文分离了函数解释的两个组成部分：仿射信息传播和收缩。我们引入信息核作为捕获仿射部分的代数接口。信息核指定与有限类型对象相关联的信息、精确对象如何与此类信息兼容以及信息如何通过函数传播。从任何信息核我们都能得到仿射有限类型算术的公式翻译和健全性定理。将健全性扩展到带有收缩的有限类型算术需要一个额外要素：一个公式索引的收缩结构，将重复假设产生的挑战减少到单个挑战。有限候选集与并集产生Herbrand风格的解释，而精确信息与挑战选择在限于可判定原始公式的算术系统上产生通常的Dialectica解释。由此产生的框架提供了一种统一方法来指定提取的实现者携带的信息，允许现有的函数解释系统地用辅助数据（如连续性信息）丰富。
英文摘要
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.
