一句话：用 update recursion 直接解释二阶算术的二阶消去，弥合 bar recursion 与多态 λ 演算两条计算解释路径。
二阶算术有两种计算解释路径：Spector 的 bar recursion 解释选择公理的负翻译，结合排中律负翻译后可解释概括公理模式的负翻译，并通过实例化全称量化集合得到二阶消去；Girard 的多态 λ 演算则用多态类型直接解释二阶消去。本文旨在弥合二者差距，提出用 update recursion（bar recursion 的变体）直接解释二阶消去，从而给出二阶算术的直接计算解释，并建立其与既有两条路径的联系。工作以证明论与类型论的理论构造和元定理证明为主，摘要未涉及实验评估。
Second-order arithmetic has two kinds of computational interpretations: via Spector’s bar recursion of via Girard’s polymorphic lambda-calculus. Bar recursion interprets the negative translation of the axiom of choice which, combined with an interpretation of the negative translation of the excluded middle, gives a computational interpretation of the negative translation of the axiom scheme of comprehension. It is then possible to instantiate universally quantified sets with arbitrary formulas (second-order elimination). On the other hand, polymorphic lambda-calculus interprets directly second-order elimination by means of polymorphic types. The present work aims at bridging the gap between these two interpretations by interpreting directly second-order elimination through update recursion, which is a variant of bar recursion.