In a small-step semantics with a deterministic reduction strategy, refocusing is a transformation that connects a reduction-based normalization function (i.e., a normalization function that enumerates the successive terms in a reduction sequence -- the successive reducts) and a reduction-free normalization function (i.e., a normalization function that does not construct any reduct because all the reducts are deforested). This transformation was introduced by Nielsen and the author in the early 2000's with an informal correctness proof. Since then, it has been used in a variety of settings, starting with Biernacka and the author's syntactic correspondence between calculi and abstract machines, and several formal proofs of it have been put forward. This article presents a simple, if overdue, formal proof of refocusing that uses the Coq Proof Assistant and is aligned with the simplicity of the original idea.


翻译:在一个带有决定性的减少战略的小步语义学中,重新定位是一种转变,将基于减少的正常化功能(即一种正常化功能,在削减序列中逐个列举顺序中的顺序 -- -- 连续的删减)和无削减的正常化功能(即一种由于所有重新降水都被砍伐而没有造成任何再降的正常化功能)联系起来。这种转变是Nielsen和作者在2000年初以非正式的正确性证明引入的。从那时起,这种转变就被用于各种环境,从Biernacka和作者的计算器和抽象机器之间的合成通信开始,并提出了若干这方面的正式证据。如果逾期,这篇文章提供了使用 Coq 校准助理并符合原始概念的简单化的简单化的正式证据。

0
下载
关闭预览

相关内容

Artificial Intelligence: Ready to Ride the Wave? BCG 28页PPT
专知会员服务
26+阅读 · 2022年2月20日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
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日
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日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
LibRec 精选:推荐的可解释性[综述]
LibRec智能推荐
10+阅读 · 2018年5月4日
Capsule Networks解析
机器学习研究会
11+阅读 · 2017年11月12日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Arxiv
57+阅读 · 2022年1月5日
Arxiv
11+阅读 · 2021年3月25日
Arxiv
15+阅读 · 2021年2月19日
VIP会员
相关资讯
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
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日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
LibRec 精选:推荐的可解释性[综述]
LibRec智能推荐
10+阅读 · 2018年5月4日
Capsule Networks解析
机器学习研究会
11+阅读 · 2017年11月12日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
相关基金
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Top
微信扫码咨询专知VIP会员