We give a new formulation of Turing reducibility in terms of higher modalities, inspired by an embedding of the Turing degrees in the lattice of subtoposes of the effective topos discovered by Hyland. In this definition, higher modalities play a similar role to I/O monads or dialogue trees in allowing a function to receive input from an external oracle. However, in homotopy type theory they have better logical properties than monads: they are compatible with higher types, and each modality corresponds to a reflective subuniverse that under suitable conditions is itself a model of homotopy type theory. We give synthetic proofs of some basic results about Turing reducibility in cubical type theory making use of two axioms of Markov induction and computable choice. Both axioms are variants of axioms already studied in the effective topos. We show they hold in certain reflective subuniverses of cubical assemblies, demonstrate their use in some simple proofs in synthetic computability theory using modalities, and show they are downwards absolute for oracle modalities. These results have been formalised using cubical mode of the Agda proof assistant. We explore some first connections between Turing reducibility and homotopy theory. This includes a synthetic proof that two Turing degrees are equal as soon as they induce isomorphic permutation groups on the natural numbers, making essential use of both Markov induction and the formulation of groups in HoTT as pointed, connected, 1-truncated types. We also give some simple non-topological examples of modalities in cubical assemblies based on these ideas, to illustrate what we expect higher dimensional analogues of the Turing degrees to look like.


翻译:我们基于海兰在有效拓扑斯子拓扑格中发现的图灵度嵌入,利用高阶模态重新表述了图灵可归约性。在此定义中,高阶模态扮演着类似于I/O单子或对话树的角色,允许函数从外部神谕接收输入。然而,在同伦类型论中,模态比单子具有更优越的逻辑性质:它们与高阶类型兼容,且每个模态对应一个反射子宇宙,在适当条件下其自身即可构成同伦类型论的模型。我们在立方类型论中利用马尔可夫归纳与可计算选择两条公理,给出了关于图灵可归约性若干基本结果的综合证明。这两条公理均为有效拓扑斯中已有公理的变体。我们证明它们在立方装配的某些反射子宇宙中成立,展示了它们在使用模态的合成可计算性理论中的简单证明应用,并证明它们对神谕模态具有向下绝对性。这些结果已通过Agda证明助手的立方模式完成形式化。我们初步探索了图灵可归约性与同伦理论之间的联系,包括一个综合证明:两个图灵度在诱导自然数上的同构置换群时即相等,该证明本质性地利用了马尔可夫归纳与HoTT中将群表述为点化、连通、1-截断类型的方法。我们还基于这些思想给出了立方装配中若干简单的非拓扑模态示例,以阐释我们所期待的高维图灵度类比结构。

0
下载
关闭预览

相关内容

【ACL2020】多模态信息抽取,365页ppt
专知会员服务
151+阅读 · 2020年7月6日
FlowQA: Grasping Flow in History for Conversational Machine Comprehension
专知会员服务
34+阅读 · 2019年10月18日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
60+阅读 · 2019年10月17日
《DeepGCNs: Making GCNs Go as Deep as CNNs》
专知会员服务
32+阅读 · 2019年10月17日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
164+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
182+阅读 · 2019年10月11日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
41+阅读 · 2019年10月9日
Hierarchically Structured Meta-learning
CreateAMind
27+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
29+阅读 · 2019年5月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
18+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
44+阅读 · 2019年1月3日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
STRCF for Visual Object Tracking
统计学习与视觉计算组
15+阅读 · 2018年5月29日
Focal Loss for Dense Object Detection
统计学习与视觉计算组
12+阅读 · 2018年3月15日
可解释的CNN
CreateAMind
18+阅读 · 2017年10月5日
IJCAI | Cascade Dynamics Modeling with Attention-based RNN
KingsGarden
13+阅读 · 2017年7月16日
国家自然科学基金
13+阅读 · 2017年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
5+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
国家自然科学基金
6+阅读 · 2014年12月31日
Arxiv
18+阅读 · 2022年11月21日
Arxiv
69+阅读 · 2022年9月7日
Arxiv
16+阅读 · 2022年5月17日
Arxiv
10+阅读 · 2021年11月3日
Arxiv
49+阅读 · 2021年9月11日
Arxiv
27+阅读 · 2019年11月24日
dynnode2vec: Scalable Dynamic Network Embedding
Arxiv
15+阅读 · 2018年12月6日
Arxiv
14+阅读 · 2018年4月18日
VIP会员
最新内容
2026“人工智能+”行业发展蓝皮书(附下载)
专知会员服务
6+阅读 · 今天12:11
《强化学习数学基础》
专知会员服务
4+阅读 · 今天12:07
“Maven计划”的发展演变之“Maven智能系统”应用
《无人机革命:来自俄乌战场的启示》(报告)
专知会员服务
9+阅读 · 今天6:48
《实现联合作战能力所需的技术》58页报告
专知会员服务
5+阅读 · 今天6:30
以色列运用人工智能优化空袭警报系统
专知会员服务
5+阅读 · 今天6:20
以色列在多条战线部署AI智能体
专知会员服务
7+阅读 · 今天6:12
相关VIP内容
【ACL2020】多模态信息抽取,365页ppt
专知会员服务
151+阅读 · 2020年7月6日
FlowQA: Grasping Flow in History for Conversational Machine Comprehension
专知会员服务
34+阅读 · 2019年10月18日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
60+阅读 · 2019年10月17日
《DeepGCNs: Making GCNs Go as Deep as CNNs》
专知会员服务
32+阅读 · 2019年10月17日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
164+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
182+阅读 · 2019年10月11日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
41+阅读 · 2019年10月9日
相关资讯
Hierarchically Structured Meta-learning
CreateAMind
27+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
29+阅读 · 2019年5月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
18+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
44+阅读 · 2019年1月3日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
STRCF for Visual Object Tracking
统计学习与视觉计算组
15+阅读 · 2018年5月29日
Focal Loss for Dense Object Detection
统计学习与视觉计算组
12+阅读 · 2018年3月15日
可解释的CNN
CreateAMind
18+阅读 · 2017年10月5日
IJCAI | Cascade Dynamics Modeling with Attention-based RNN
KingsGarden
13+阅读 · 2017年7月16日
相关论文
Arxiv
18+阅读 · 2022年11月21日
Arxiv
69+阅读 · 2022年9月7日
Arxiv
16+阅读 · 2022年5月17日
Arxiv
10+阅读 · 2021年11月3日
Arxiv
49+阅读 · 2021年9月11日
Arxiv
27+阅读 · 2019年11月24日
dynnode2vec: Scalable Dynamic Network Embedding
Arxiv
15+阅读 · 2018年12月6日
Arxiv
14+阅读 · 2018年4月18日
相关基金
国家自然科学基金
13+阅读 · 2017年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
5+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
国家自然科学基金
6+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员