Gentzen 风格的单子翻译对 Gödel 系统 T 的再考察
The Gentzen-style monadic translation of Gödel's System T revisited
浏览论文内容
中文总结 AI 辅助
本文重新考察了 Gödel 系统 T 的 Gentzen 风格单子翻译，通过核参数化并利用逻辑关系基本定理统一论证正确性，获得了连续性模量、对话树等实例，并扩展至和与有限列表，同时比较了 Kuroda 风格翻译。
中文摘要 AI 辅助
我们重新考察了 Gödel 系统 T 的 Gentzen 风格的单子翻译。该翻译由一个核（nucleus）参数化，这是一种类似单子的结构，但不必满足单子律。逻辑关系的一个基本定理为其实例提供了统一的正确性论证。通过选择合适的核，我们获得了主项（majorants）、逐点连续性和一致连续性的模量（moduli）、内部对话树（internal dialogue trees）以及一般 bar 递归（general bar recursion）的函数，所有这些都由 T 的项表示。内部对话树的应用给出了一个更简单的构造，其正确性直接使用 Church 编码的项来确立。我们还将该翻译及其基本定理扩展到和（sums）与有限列表（finite lists）。最后，我们发展了 Kuroda 风格的翻译及其连续性实例，并将所获得的模量与 Gentzen 风格翻译的模量进行了比较。
英文摘要
We revisit the Gentzen-style monadic translation of Gödel's System T. The translation is parametrized by a nucleus, a monad-like structure that need not satisfy the monad laws. A fundamental theorem of logical relations provides a uniform correctness argument for its instances. By choosing suitable nuclei, we obtain majorants, moduli of pointwise and uniform continuity, internal dialogue trees, and functionals of general bar recursion, all represented by terms of T. The internal dialogue-tree application gives a simpler construction, with correctness established directly using Church-encoded terms. We also extend the translation and its fundamental theorem to sums and finite lists. Finally, we develop the Kuroda-style translation and its continuity instance, comparing the moduli obtained with those of the Gentzen-style translation.
