Circular and non-wellfounded proofs have become an increasingly popular tool for metalogical treatments of systems with forms of induction and/or recursion. In this work we investigate the expressivity of a variant CT of G\"odel's system T where programs are circularly typed, rather than including an explicit recursion combinator. In particular, we examine the abstraction complexity (i.e. type level) of C, and show that the G\"odel primitive recursive functionals may be typed more succinctly with circular derivations, using types precisely one level lower than in T. In fact we give a logical correspondence between the two settings, interpreting the quantifier-free type 1 theory of level n+1 T into that of level n C and vice-versa. We also obtain some further results and perspectives on circular 'derivations', namely strong normalisation and confluence, models based on hereditary computable functionals, continuity at type 2, and a translation to terms of $\T$ computing the same functional, at all types.


翻译:圆形和无根据的证明已成为一种日益流行的工具,用于对具有诱导和(或)循环形式的系统进行元学处理。在这项工作中,我们调查了程序循环键入的G\“odel”系统T的变体CT的表达性,而不是包括一个明确的循环组合器。特别是,我们研究了C的抽象复杂性(即类型级别),并表明G\“odel原始循环功能”可以更简洁地以循环衍生方式打字,使用的类型比T低一个层次。事实上,我们给出了两种环境之间的逻辑对应,将n+1 T级的限定性1型理论解释为n C级和反转。我们还获得了关于循环“递归(即强的正常化和连带作用)”的一些进一步的结果和观点,即基于遗传可兼容功能的模型、2型的连续性和所有类型计算相同功能的翻译值为$\T$。

0
下载
关闭预览

相关内容

让 iOS 8 和 OS X Yosemite 无缝切换的一个新特性。 > Apple products have always been designed to work together beautifully. But now they may really surprise you. With iOS 8 and OS X Yosemite, you’ll be able to do more wonderful things than ever before.

Source: Apple - iOS 8
自动化学科面临的挑战
专知会员服务
37+阅读 · 2020年12月19日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
78+阅读 · 2020年7月26日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
计算机 | 国际会议信息5条
Call4Papers
3+阅读 · 2019年7月3日
【2019-26期】This Week in Extracellular Vesicles
外泌体之家
11+阅读 · 2019年6月28日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
已删除
将门创投
5+阅读 · 2018年10月16日
计算机类 | 国际会议信息7条
Call4Papers
3+阅读 · 2017年11月17日
Arxiv
0+阅读 · 2021年3月15日
Arxiv
0+阅读 · 2021年3月12日
Arxiv
0+阅读 · 2021年3月11日
Arxiv
3+阅读 · 2018年8月17日
Arxiv
27+阅读 · 2018年4月12日
VIP会员
相关资讯
计算机 | 国际会议信息5条
Call4Papers
3+阅读 · 2019年7月3日
【2019-26期】This Week in Extracellular Vesicles
外泌体之家
11+阅读 · 2019年6月28日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
已删除
将门创投
5+阅读 · 2018年10月16日
计算机类 | 国际会议信息7条
Call4Papers
3+阅读 · 2017年11月17日
Top
微信扫码咨询专知VIP会员