In this paper, we present a linear and reversible programming language with inductives types and recursion. The semantics of the languages is based on pattern-matching; we show how ensuring syntactical exhaustivity and non-overlapping of clauses is enough to ensure reversibility. The language allows to represent any Primitive Recursive Function. We then give a Curry-Howard correspondence with the logic {\mu}MALL: linear logic extended with least fixed points allowing inductive statements. The critical part of our work is to show how primitive recursion yields circular proofs that satisfy {\mu}MALL validity criterion and how the language simulates the cut-elimination procedure of {\mu}MALL.


翻译:在本文中, 我们展示了一种直线和可逆的编程语言, 带有感应类型和递归。 语言的语义以模式匹配为基础; 我们展示了如何确保条款的综合性耗尽性和非重叠性足以确保可逆性。 语言允许代表任何原始再现功能。 然后我们给出了逻辑 {mu} mall 的咖哩- Howard对应词: 线性逻辑延伸至最不固定的点, 允许感应语句。 我们工作的关键部分是显示原始递归如何产生符合 {mu} malall 有效性标准的循环证明, 以及语言如何模拟 {mule mall 的切除程序 。

0
下载
关闭预览

相关内容

Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
100+篇《自监督学习(Self-Supervised Learning)》论文最新合集
专知会员服务
164+阅读 · 2020年3月18日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
ICLR2019最佳论文出炉
专知
12+阅读 · 2019年5月6日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
无监督元学习表示学习
CreateAMind
27+阅读 · 2019年1月4日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Arxiv
11+阅读 · 2020年12月2日
Adversarial Mutual Information for Text Generation
Arxiv
13+阅读 · 2020年6月30日
Advances and Open Problems in Federated Learning
Arxiv
18+阅读 · 2019年12月10日
Arxiv
13+阅读 · 2019年11月14日
Meta-Learning to Cluster
Arxiv
17+阅读 · 2019年10月30日
Meta-Learning with Implicit Gradients
Arxiv
13+阅读 · 2019年9月10日
Arxiv
11+阅读 · 2019年4月15日
VIP会员
相关资讯
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
ICLR2019最佳论文出炉
专知
12+阅读 · 2019年5月6日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
无监督元学习表示学习
CreateAMind
27+阅读 · 2019年1月4日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
相关论文
Arxiv
11+阅读 · 2020年12月2日
Adversarial Mutual Information for Text Generation
Arxiv
13+阅读 · 2020年6月30日
Advances and Open Problems in Federated Learning
Arxiv
18+阅读 · 2019年12月10日
Arxiv
13+阅读 · 2019年11月14日
Meta-Learning to Cluster
Arxiv
17+阅读 · 2019年10月30日
Meta-Learning with Implicit Gradients
Arxiv
13+阅读 · 2019年9月10日
Arxiv
11+阅读 · 2019年4月15日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Top
微信扫码咨询专知VIP会员