Infinite Gray code has been introduced by Tsuiki as a redundancy-free representation of the reals. In applications the signed digit representation is mostly used which has maximal redundancy. Tsuiki presented a functional program converting signed digit code into infinite Gray code. Moreover, he showed that infinite Gray code can effectively be converted into signed digit code, but the program needs to have some non-deterministic features (see also H. Tsuiki, K. Sugihara, "Streams with a bottom in functional languages"). Berger and Tsuiki reproved the result in a system of formal first-order intuitionistic logic extended by inductive and co-inductive definitions, as well as some new logical connectives capturing concurrent behaviour. The programs extracted from the proofs are exactly the ones given by Tsuiki. In order to do so, co-inductive predicates $\bS$ and $\bG$ are defined and the inclusion $\bS \subseteq \bG$ is derived. For the converse inclusion the new logical connectives are used to introduce a concurrent version $\S_{2}$ of $S$ and $\bG \subseteq \bS_{2}$ is shown. What one is looking for, however, is an equivalence proof of the involved concepts. One of the main aims of the present paper is to close the gap. A concurrent version $\bG^{*}$ of $\bG$ and a modification $\bS^{*}$ of $\bS_{2}$ are presented such that $\bS^{*} = \bG^{*}$. A crucial tool in U. Berger, H. Tsuiki, "Intuitionistic fixed point logic" is a formulation of the Archimedean property of the real numbers as an induction principle. We introduce a concurrent version of this principle which allows us to prove that $\bS^{*}$ and $\bG^{*}$ coincide. A further central contribution is the extension of the above results to the hyperspace of non-empty compact subsets of the reals.


翻译:摘要:由辍辺贺介绍的无穷灰码是实数的无冗余表示。在应用中,大多数情况下使用具有最大冗余的有符号数字表示。辍辺贺提出了一种功能程序,将有符号数字代码转换为无穷灰码。此外,他还展示了无穷灰码可以有效地转换为有符号数字代码,但该程序需要一些非确定性特征(也请参阅 H. Tsuiki, K. Sugihara,“Functional Languages ​​中带底部的流”)。Berger 和辍辺贺在归纳和共归纳定义扩展的正直命题逻辑系统中重新证明了该结果,以及一些新的逻辑连词捕捉并发行为。从证明中提取的程序恰好是辍辺贺所给出的程序。为此,定义了共归纳谓词$ \bS $和$ \bG $,并推导出$ \bS \subseteq \bG $的包含关系。对于逆含关系,使用了新的逻辑连接词来引入$ S $的并发版本$ \S_ {2} $,并显示$ \bG \subseteq \bS_ {2} $。然而,人们寻找的是涉及概念的等价证明。本文的主要目标之一是弥补差距。提出了共归纳版本$ \bG ^ *$和$ \bS_ {2} $的修改$ \bS ^ * $,使得$ \bS ^ * = \bG ^ * $。U. Berger,H. Tsuiki,“直观固定点逻辑”的一个关键工具是将实数的阿基米德特性制定为归纳原则。我们介绍了这个原则的并发版本,允许我们证明$ \bS ^ * $和$ \bG ^ * $相同。更进一步地,将上述结果扩展到实数非空紧致子集的超空间中。

0
下载
关闭预览

相关内容

【硬核书】矩阵代数基础,248页pdf
专知会员服务
83+阅读 · 2021年12月9日
【干货书】真实机器学习,264页pdf,Real-World Machine Learning
强化学习最新教程,17页pdf
专知会员服务
171+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
量化金融强化学习论文集合
专知
13+阅读 · 2019年12月18日
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
26+阅读 · 2019年5月18日
深度自进化聚类:Deep Self-Evolution Clustering
我爱读PAMI
15+阅读 · 2019年4月13日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
【推荐】用Python/OpenCV实现增强现实
机器学习研究会
14+阅读 · 2017年11月16日
Capsule Networks解析
机器学习研究会
11+阅读 · 2017年11月12日
MoCoGAN 分解运动和内容的视频生成
CreateAMind
18+阅读 · 2017年10月21日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Arxiv
1+阅读 · 2023年6月6日
Arxiv
0+阅读 · 2023年6月2日
Arxiv
11+阅读 · 2018年4月8日
VIP会员
相关资讯
量化金融强化学习论文集合
专知
13+阅读 · 2019年12月18日
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
26+阅读 · 2019年5月18日
深度自进化聚类:Deep Self-Evolution Clustering
我爱读PAMI
15+阅读 · 2019年4月13日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
【推荐】用Python/OpenCV实现增强现实
机器学习研究会
14+阅读 · 2017年11月16日
Capsule Networks解析
机器学习研究会
11+阅读 · 2017年11月12日
MoCoGAN 分解运动和内容的视频生成
CreateAMind
18+阅读 · 2017年10月21日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Top
微信扫码咨询专知VIP会员