Continuity of Gödel's System T Definable Functionals via Effectful Forcing
Continuity of Gödel's System T Definable Functionals via Effectful Forcing
复制标题
通过有效强制实现哥德尔系统 T 可定义泛函的连续性
DOI：
10.1016/j.entcs.2013.09.010
复制
发表时间：
2013
期刊：
影响因子：
0.7
通讯作者：
M. Escardó
中科院分区：
文献类型：
--
作者：
M. Escardó
众所周知，哥德尔系统T可定义函数（N→ N）→ N是连续的，并且它们从Baire型（N→ N）到Cantor型（N→ 2）的限制是一致连续的。我们提供了一个新的，相对较短的和独立的证明。主要的技术思想是一个具体的泛型元素概念，它不依赖于强制，Kripke语义或sheaves，这似乎与编程中的泛型效果有关。证明使用来自编程语言语义的标准技术，例如对话、单子和逻辑关系。我们从头开始用内涵马丁-勒夫类型理论（MLTT），用Agda符号来写这个证明。由于MLTT具有计算解释，而Agda可以被视为一种编程语言，因此我们可以运行我们的证明来计算T-可定义函数的（一致）连续性模。
It is well-known that the Gödelʼs system T definable functions (N→ N)→ N are continuous, and that their restrictions from the Baire type (N→ N) to the Cantor type (N→ 2) are uniformly continuous. We offer a new, relatively short and self-contained proof. The main technical idea is a concrete notion of generic element that doesnʼt rely on forcing, Kripke semantics or sheaves, which seems to be related to generic effects in programming. The proof uses standard techniques from programming language semantics, such as dialogues, monads, and logical relations. We write this proof in intensional Martin-Löf type theory (MLTT) from scratch, in Agda notation. Because MLTT has a computational interpretation and Agda can be seen as a programming language, we can run our proof to compute moduli of (uniform) continuity of T-definable functions.
影响因子：
0.6
作者：
Ghani N
通讯作者：
Ghani N