哥德尔系统T中函数的连续性证明及计算性
68 浏览量
更新于2024-06-18
收藏 787KB PDF 举报
"本文详细探讨了在哥德尔系统T中如何证明定义的函数的连续性和计算一致性。作者MartínEscardó提出了一种新的、相对简短且独立的证明方法，该方法不依赖于传统的强制、Kripke语义或sheaves的元素，而是引入了泛型元素的概念，这个概念与编程中的泛型效果有关。证明过程运用了编程语言语义学的标准技术，如对话、单子和逻辑关系，并使用内涵马丁-勒夫类型理论（MLTT）以及Agda符号进行表述。由于MLTT具有计算解释，Agda是一种编程语言，因此该证明可以直接运行来计算T-可定义函数的连续性模。
文章首先介绍了已知的事实，即在哥德尔系统T中定义的任何函数f：(N→N)→N都是连续的，并且从Baire型空间(N→N)到Cantor型空间(N×N)的限制是一致连续的。新证明的独特之处在于通过对话树来表示函数f，并从树中提取连续性信息。作者构造了一个辅助函数f_∞：(N_∞→N_∞)→N_∞，其中N_∞代表系统T的对话树。通过对N_∞上的类属序列应用f，可以得到关于f的连续性对话。
该证明的思路是，通过构建一个良好的基础对话树来模拟函数f的行为，然后通过在系统T的解释中计算这个对话树，推导出f的连续性。这种方法不仅提供了一种理解函数连续性的新视角，而且也展示了逻辑、计算和构造性数学的交叉点如何能为程序设计语言的语义分析带来洞见。
关键词：哥德尔系统T，连续性证明，泛型元素，对话树，单子，逻辑关系，内涵马丁-勒夫类型理论，Agda，计算一致性。
1571-0661©2013由Elsevier B.V.出版，本篇论文在CC BY-NC-ND许可下开放获取，doi:10.1016/j.entcs.2013.09.010。
120
M.Escardó/理论计算机科学电子笔记298（2013）119
该研究对于理解哥德尔系统T中的函数性质，以及构造性数学和计算理论中的连续性概念有着重要的贡献，同时为编程语言的语义分析提供了新的工具和方法。"
M. Escardó/
理论计算机科学电子笔记
298
（
2013
）
119
123
rec
：
{
X：Set
}
→（X→X）→X→N→X
→
≡
-
-
→
∀
→ → →→
∀
→ →
∀
→→
∀
→
∀
→ ≡ →≡
∀
→
∀
→ ≡ → ≡ →≡
∀
→
∀
→ →
∀
→ ≡ → ≡
集合变量周围的花括号表示这些是隐式参数，当
使用
v
er
K
和
k
时由Agda推断
。
如果
阿
格达不能
唯一
地
推断
出缺失的
字母
，
则
必须
写为例如。
K
<$
{
X
}{
Y
}
xy
而
不是缩写
形式
K
<$
x
y
。
以下
内容
应该
是
不言自明的：
__
：{X Y Z：
Set
}→（Y→Z）→（X→Y）→（X→Z）
gf=x→g（f x）
data
N
：
Setwherezero：
N
rec
succ：
N
→
N
f x
zero
=
x
recf x（succn）
=
f（recf x n）
Agda
有一个终止检查器，可以验证递归是有根据的，因此所有函数都是总数。我们
还需要二进制数字、有限列表和有限二叉树的类型：
dataN
2
：Setwhere
0 1
：
N
2
dataList
（
X
：
Set
）：
Setwhere[] ：ListX
_
：：
_
：
X
→列表
X
→列表
X
dataTree（X：Set）：
Setwhereempty
：
TreeX
分支：
X
→（N
2
→
TreeX
）→
TreeX
和不是内置的，因此需要定义：
数据集
{
X：Set
}
（Y：X→Set）：Setwhere
_
，
_
：（
x
：
X
）（
y
：
Y x
）→{
X
}
Y
定义说，一个
元素的<$
{
X
}
Y
是一对（
x
，
y
）与
x
：
X
和
y
：
Y X
。请注意，逗号
不是一个保留符号：我们将其定义为一个二元运算符来构造依赖对。因为如果
假设
η -
定律，
Y=
（
x
：
X
）
Y x
，并且因为第一个参数是隐式的，我们可以将
X
Y
写成
Y
或
\
（
x
：
X
）
Y x
，其中反斜杠与
lambda
相同。我们将使用反斜杠专门为总
和。
π
0
：
{
X：集合
} {
Y：X 集合
}
（
\
（x：X） Y x） X
π
0
（
x
，
y
）=
x
π
1
： {
X
：集合} {
Y
：
X
集合} （
t
：\（
x
：
X
）
Y x
）
Y
（
π
0
t
）
π
1
（
x
，
y
）=
y
单位类型
Id
X x
y
被写
为
x
y
，其中
X
是隐式的
，并且被归纳地定义为
“
最小相关关
系”：
data
__
{
X：Set
}
：X→X→Setwherere：
{
x：X
}
→xx
对称：
{
X
：集合
} {
x y
：
X
}
x y y x
symre
=
re
反式：
{
X
：集合
} {
x y z
：
X
}
x y y z x z
transre re
=
re
cong
： {
X Y
：集合} （
f
：
X Y
） {
x
0
x
1
：
X
}
x
0
x
1
f x
0
f x
1
cong
f
re
=
re
cong
2
：
{
X Y Z：Set
}
→（f：X→Y→Z）
剩余22页未读，继续阅读
2022-07-01 上传
2010-12-24 上传
2010-05-11 上传
点击了解资源详情
2024-10-24 上传
cpongm
- 粉丝: 5
- 资源: 2万+
我的内容管理
展开
最新资源
- 掌握Jive for Android SDK：示例应用的使用指南
- Python中的贝叶斯建模与概率编程指南
- 自动化NBA球员统计分析与电子邮件报告工具
- 下载安卓购物经理带源代码完整项目
- 图片压缩包中的内容解密
- C++基础教程视频-数据类型与运算符详解
- 探索Java中的曼德布罗图形绘制
- VTK9.3.0 64位SDK包发布，图像处理开发利器
- 自导向运载平台的行业设计方案解读
- 自定义 Datadog 代理检查：Python 实现与应用
- 基于Python实现的商品推荐系统源码与项目说明
- PMing繁体版字体下载，设计师必备素材
- 软件工程餐厅项目存储库：Java语言实践
- 康佳LED55R6000U电视机固件升级指南
- Sublime Text状态栏插件：ShowOpenFiles功能详解
- 一站式部署thinksns社交系统，小白轻松上手
